Sciweavers

TASE
2008
IEEE

PDL over Accelerated Labeled Transition Systems

14 years 4 months ago
PDL over Accelerated Labeled Transition Systems
We present a thorough study of Propositional Dynamic Logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding ones of PDL in the traditional semantics (w.r.t. LTS). As for the complexity, both of problems are proved to be EXPSPACE-complete. Moreover, the program complexity of model checking problem turns out to be NLOGSPACEcomplete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.
Taolue Chen, Jaco van de Pol, Yanjing Wang
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TASE
Authors Taolue Chen, Jaco van de Pol, Yanjing Wang
Comments (0)