An automata theoretic decision procedure for the propositional mu-calculus

ISCAS OpenIR

	An automata theoretic decision procedure for the propositional mu-calculus
	Robert S. Streett; E. Allen Emerson
	1989
发表期刊	Information and Computation
卷号	81 期号:3 页码:249 - 264
摘要	The propositional mu-calculus is a propositional logic of programs which incorporates a least fixpoint operator and subsumes the propositional dynamic logic of Fischer and Ladner, the infinite looping construct of Streett, and the game logic of Parikh. We give an elementary time decision procedure, using a reduction to the emptiness problem for automata on infinite trees. A small model theorem is obtained as a corollary.
收录类别	其他
合作性质	其它
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/1353
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Robert S. Streett,E. Allen Emerson. An automata theoretic decision procedure for the propositional mu-calculus[J]. Information and Computation,1989,81(3):249 - 264.
APA	Robert S. Streett,&E. Allen Emerson.(1989).An automata theoretic decision procedure for the propositional mu-calculus.Information and Computation,81(3),249 - 264.
MLA	Robert S. Streett,et al."An automata theoretic decision procedure for the propositional mu-calculus".Information and Computation 81.3(1989):249 - 264.