Login
- Titel:
Model Checking PA-Processes
- Dokumenttyp:
- Technical Report
- Autor(en):
- Richard Mayr
- Abstract:
- PA (Process algebra) is the name that has become common use to denote the algebra with a sequential and parallel operator (without communication), plus recursion. PA-processes are a superset of both Basic Parallel Processes (BPP) and context-free processes (BPA). They are a simple model for infinite state concurrent systems. We show that the model checking problem for the branching time temporal logic EF is decidable for PA-processes.
- Stichworte:
- PA-processes; model checking; process algebras; tableau systems
- Jahr:
- 1996
- Jahr / Monat:
- 1996-11-01 00:00:00
- Seiten/Umfang:
- 27
BibTeX