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 NLOGSPACE-complete. 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

作者单位: CWI PO Box 94079 1090 GB Amsterdam, NL University of Twente PO Box 217 7500 AE Enschede, NL

会议类型: 国际会议

会议名称: 第二届IFIP/IEEE软件工程理论基础国际研讨会(TASE 2008)(Second IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering)

会议地点: 南京

会议语种:英文

页码: 193-200

在线出版日期: 2008-06-17（万方平台首次上网日期，不代表论文的发表时间）