Institutional Repository
| An automata theoretic decision procedure for the propositional mu-calculus | |
| Robert S. Streett; E. Allen Emerson | |
| 1989 | |
| Source | Information and Computation
 |
| Volume | 81Issue:3Pages:249 - 264 |
| English Abstract | 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. |
| Indexed Type | 其他 |
| Cooperation Status | 其它 |
| Language | 英语 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/1353 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation 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. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| bj01147735.pdf（898KB） | 开放获取 | License | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment