loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering
PDL over Accelerated Labeled Transition Systems
June 17-June 19
ISBN: 978-0-7695-3249-3
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 Nlogspace-complete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.
Index Terms:
PDL, Accelerated Labeled Transition Systems
Citation:
Taolue Chen, Jaco van de Pol, Yanjing Wang, "PDL over Accelerated Labeled Transition Systems," tase, pp.193-200, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008
Usage of this product signifies your acceptance of the Terms of Use.