PDL over Accelerated Labeled Transition Systems

Chen, Taolue and Pol van de, Jaco and Wang, Yanjing (2008) PDL over Accelerated Labeled Transition Systems. In: 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 June 2008, Nanjing, China.

Preview

PDF
276Kb

Abstract:	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.
Item Type:	Conference or Workshop Item
Copyright:	© 2008 IEEE
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/64837
Official URL:	http://dx.doi.org/10.1109/TASE.2008.42
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 251038