Model checking propositional dynamic logic with all extras |
| |
Authors: | Martin Lange |
| |
Affiliation: | University of Munich, Institut für Informatik, Oettingenstr. 67, D-80538 München, Germany |
| |
Abstract: | This paper presents a model checking algorithm for Propositional Dynamic Logic (PDL) with looping, repeat, test, intersection, converse, program complementation as well as context-free programs. The algorithm shows that the model checking problem for PDL remains PTIME-complete in the presence of all these operators, in contrast to the high increase in complexity that they cause for the satisfiability problem. |
| |
Keywords: | Propositional Dynamic Logic Model checking Complexity |
本文献已被 ScienceDirect 等数据库收录! |
|