Infinite State Model-Checking of Propositional Dynamic Logics

Model-checking problems for PDL (propositional dynamic logic) and its extension PDL (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.

• Type: Journal
• Year: 2006
• Where: CSL
• Authors: Stefan Göller, Markus Lohrey
• Keywords: Automated Reasoning, CSL 2006, Extension Pdl, Infinite State Systems, Propositional Dynamic Logic