specification in pdl with recursion

CORC > 软件研究所 > 软件所图书馆 > 会议论文

	specification in pdl with recursion
	Liu Xinxin ; Xue Bingtian
	2012
会议名称	4th NASA Formal Methods Symposium, NFM 2012
会议日期	April 3, 2012 - April 5, 2012
会议地点	Norfolk, VA, United states
关键词	Calculations NASA Specifications
页码	181-194
中文摘要	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.
收录类别	EI
会议录	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
语种	英语
ISSN号	0302-9743
ISBN号	9783642288906
内容类型	会议论文
源URL	[http://ir.iscas.ac.cn/handle/311060/15703]
专题	软件研究所_软件所图书馆_会议论文
推荐引用方式 GB/T 7714	Liu Xinxin,Xue Bingtian. specification in pdl with recursion[C]. 见:4th NASA Formal Methods Symposium, NFM 2012. Norfolk, VA, United states. April 3, 2012 - April 5, 2012.