specification in pdl with recursion

ISCAS OpenIR

	specification in pdl with recursion
	Liu Xinxin; Xue Bingtian
	2012
会议名称	4th NASA Formal Methods Symposium, NFM 2012
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	181-194
会议日期	April 3, 2012 - April 5, 2012
会议地点	Norfolk, VA, United states
收录类别	EI
ISSN	0302-9743
ISBN	9783642288906
部门归属	(1) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences P.O. Box 8718 100190 Beijing China; (2) Graduate School Chinese Academy of Sciences P.O. Box 8718 100190 Beijing China
摘要	By extending regular Propositional Dynamic Logic (PDL) with simple recursive propositions, we obtain a language which has enough expressiveness to allow interesting applications while still enjoying a relatively simple decision procedure. More specifically, it is strictly more expressive than the regular PDL and not more expressive than the single alternation fragment of the modal μ-calculus. We present a decision procedure for satisfiability of a large class of so called simple formulas. The decision procedure has a time complexity which is polynomial in the size of the programs and exponential in the number of the sub-formulas. We show a way to solve process equations of weak bisimulation as an application. © 2012 Springer-Verlag.; By extending regular Propositional Dynamic Logic (PDL) with simple recursive propositions, we obtain a language which has enough expressiveness to allow interesting applications while still enjoying a relatively simple decision procedure. More specifically, it is strictly more expressive than the regular PDL and not more expressive than the single alternation fragment of the modal μ-calculus. We present a decision procedure for satisfiability of a large class of so called simple formulas. The decision procedure has a time complexity which is polynomial in the size of the programs and exponential in the number of the sub-formulas. We show a way to solve process equations of weak bisimulation as an application. © 2012 Springer-Verlag.
关键词	Calculations Nasa Specifications
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15703
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Liu Xinxin,Xue Bingtian. specification in pdl with recursion[C],2012:181-194.