摘要: We show how LTL model checking can be reduced to CTL with fairness constraints. Using this reduction, we also describe construct a symbolic checker that appears quite efficient in practice. In particular, the SMV system developed by McMillan [16] extended permit specifications. The results have obtained are surprising. For examples considered, required at most twice as much time and space checker. Although additional still need tried, it is possible when specifications not excessively complicated.
springer.com
core.ac.uk
acm.org 
sci-hub.st 参考文章(19)
E. Allen Emerson, Chin-Laung Lei, Modalities for Model Checking: Branching Time Strikes Back. POPL. pp. 84- 96 ,(1985)
Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness, Verification of the Futurebus+ Cache Coherence Protocol CHDL '93 Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications. pp. 15- 30 ,(1993) , 10.1016/B978-0-444-81641-2.50007-1
Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem Ph. D. Thesis, Carnegie Mellon University. ,(1992)
E. M. Clarke, I. A. Browne, R. P. Kurshan, A unified approach for showing language containment and equivalence between various types of Ω-automata colloquium on trees in algebra and programming. pp. 103- 116 ,(1990) , 10.1007/3-540-52590-4_43
E. Clarke, O. Grumberg, D. Long, Verification Tools for Finite-State Concurrent Systems A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium. pp. 124- 175 ,(1993) , 10.1007/3-540-58043-3_19
Olivier Coudert, Jean Christophe Madre, Christian Berthet, Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams computer aided verification. pp. 23- 32 ,(1990) , 10.1007/BFB0023716
Alain J. Martin, The Design of a Self-timed Circuit for Distributed Mutual Exclusion California Institute of Technology. ,(1983)
E. M. Clarke, I. A. Draghicescu, Expressibility results for linear-time and branching-time logics Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop. pp. 428- 437 ,(1988) , 10.1007/BFB0013029
E.M. Clarke, I.A. Draghicescu, R.P. Kurshan, A unified approach for showing language inclusion and equivalence between various types of Ω-automata Information Processing Letters. ,vol. 46, pp. 301- 308 ,(1993) , 10.1016/0020-0190(93)90069-L
Mordechai Ben-Ari, Amir Pnueli, Zohar Manna, The temporal logic of branching time Acta Informatica. ,vol. 20, pp. 207- 226 ,(1983) , 10.1007/BF01257083