Login
- Document type:
- Technical Report
- Author(s):
- Richard Mayr
- Title:
- Model Checking PA-Processes
- 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.
- Keywords:
- PA-processes; model checking; process algebras; tableau systems
- Year:
- 1996
- Year / month:
- 1996-11-01 00:00:00
- Pages:
- 27
BibTeX