| Bibliography | Göller, Stefan; Lohrey, Markus: Infinite State Model-Checking of Propositional Dynamic Logics.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Technical Report Computer Science No. 2006/04.
47 pages, english.
|
|---|
| CR-Schema | F.1.3 (Complexity Measures and Classes)
F.4.1 (Mathematical Logic)
|
|---|
| Keywords | infinite state systems; model checking; propositional dynamic logic; basic parallel processes; basic process algebras; pushdown systems; prefix-recognizable sytems |
|---|
| Abstract | Model-checking problems for propositional dynamic logic (PDL) and its extension PDL$^\cap$ (which includes the intersection operator on programs) over various classes of infinite state systems (BPP, BPA, pushdown systems, prefix-recognizable systems) are studied. Precise upper and lower bounds are shown for the data/expression/combined complexity of these model-checking problems.
|
|---|
Full text and
other links | PDF (420573 Bytes)
PostScript (688567 Bytes)
|
|---|
| Contact | goeller@informatik.uni-stuttgart.de lohrey@informatik.uni-stuttgart.de |
|---|
| Department(s) | University of Stuttgart, Institute of Formal Methods in Computer Science, Theoretical Computer Science
|
|---|
| Entry date | February 8, 2006 |
|---|