scholarly journals Infinite State Model-Checking of Propositional Dynamic Logics

2006 ◽  
pp. 349-364 ◽  
Author(s):  
Stefan Göller ◽  
Markus Lohrey
Keyword(s):  
Model Checking ◽  
State Model ◽  
Infinite State ◽  
Dynamic Logics

PDL with intersection and converse: satisfiability and infinite-state model checking

2009 ◽  
Vol 74 (1) ◽  
pp. 279-314 ◽  
Author(s):  
Stefan Göller ◽  
Markus Lohrey ◽  
Carsten Lutz
Keyword(s):  
Lower Bound ◽  
Model Checking ◽  
Dynamic Logic ◽  
State Model ◽  
Propositional Dynamic Logic ◽  
Reasoning Problem ◽  
Infinite Trees ◽  
Emptiness Problem ◽  
Alternating Turing Machines ◽  
Infinite State

AbstractWe study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2ΕΧΡΤΙΜΕ, thus 2ΕΧΡΤΙΜΕ-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2ΕΧΡΤΙΜΕ-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2ΕΧΡΤΙΜΕ. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines.

Sign in / Sign up

Export Citation Format

Share Document