Abstract
The difference in the complexity of branching and linear model checking has been viewed as an argument in favor of the branching paradigm. In particular, the computational advantage of CTL model checking over LTL model checking makes CTL a popular choice, leading to efficient model-checking tools for this logic. Can we use these tools in order to verify linear properties? In this paper we relate branching and linear model checking. With each LTL formula ψ, we associate a CTL formula ψ A that is obtained from ψ by preceding each temporal operator by the universal path quantifier A. We first describe a number of attempts to utilize the tight syntactic relation between ψ and ψ A in order to use CTL model-checking tools in the process of checking the formula ψ. Neither attempt, however, suggests a method that is guaranteed to perform better than usual LTL model checkers. We then claim that, in practice, LTL model checkers perform nicely on formulas with equivalences of CTL. In fact, they often proceed essentially as the ones for CTL.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th CAV, LNCS 818, pp. 182–193, 1994.
O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Proc. 6th CAV, LNCS 818, pp. 142-155, 1994.
E. M. Clarke, I. A. Draghicescu, and R. P. Kurshan. A unified approach for showing language containment and equivalence between various types of ce-automata. IPL 46, pp 301–308, 1993.
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pp. 52–71, 1981.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. Transactions on Programming Languages and Systems, 8 (2): 244–263, 1986.
E.M. Clarke, O. Grumberg, and D. Long. Verification tools for finitestate concurrent systems. In Proc. REX School, LNCS 803, pp. 124–175, 1993.
E. Clarke. Private communication, 1997.
E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33 (1): 151–178, 1986.
E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th FOCS, pp. 368–377, 1988.
E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. In Proc. 20th POPL, pp. 84–96, 1985.
E.A. Emerson. Temporal and modal logic. Handbook of theoretical computer science, pp. 997–1072, 1990.
E.A. Emerson and A. P. Sistla. Deciding branching time logic. In Proc. 16th STOC, 1984.
GL94] O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems,16(3):843871, 1994.
R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. A simple on-the-fly automatic verification for linear temporal logic. In Protocol Specification, Testing, and Verification, pp. 3–18. Chapman and Hall, 1995.
G. Holzmann and O. Kupferman. Not checking for closure under stuttering. In Proc. 2nd SPIN, pp 163–169, 1996.
G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23 (5): 279–295, 1997.
N. Immerman. Nondeterministic space is closed under complement. SIAM Journal on Computing, 17: 935–938, 1988.
N.D. Jones. Space-bounded reducibility among combinatorial problems. Journal of Computer and System Sciences, 11: 68–75, 1975.
O. Kupferman and O. Grumberg. Buy one, get one free! Journal of Logic and Computation, 6 (4): 523–539, 1996.
O. Kupferman and M.Y. Vardi. On the complexity of branching mod- ular model checking. In Proc. 6th CONCUR, LNCS 962. pp. 408–422, 1995.
O. Kupferman and M.Y. Vardi. Module checking. In Proc. 8th CAV, LNCS 1102, pp. 75–86, 1996.
O. Kupferman and M.Y. Vardi. Module checking revisited. In Proc. 9th CAV, LNCS 1254, pp. 36–47, 1997.
L. Lamport. Sometimes is sometimes “not never”–on the temporal logic of programs. In Proc. 7th POPL, pp. 174–185, 1980.
D.E. Long. Model checking, abstraction and compositional verification. PhD thesis, Carnegie-Mellon University, Pittsburgh, 1993.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th POPL, pp. 97–107, 1985.
K.L. McMillan. Symbolic model checking. Kluwer Academic Publishers, 1993.
R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd IJCAI, pp. 481–489, 1971.
A. Pnueli. The temporal logic of programs. In Proc. 18th FOCS, pp 46–57, 1977.
A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13: 45–60, 1981.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, LNCS 137, pp. 337–351, 1981.
M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3: 115–125, 1959.
S. Safra. Complexity of automata on infinite objects. PhD thesis, Weiz- mann Institute of Science, Rehovot, Israel, 1989.
A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32: 733–749, 1985.
K. Schneider. CTL and equivalent sublanguages of CTL*. In Proc. IFIP Conference on Computer Hardware Description Languages and Applications, pp. 40–59, 1997.
R. Szelepcsinyi. The method of forced enumeration for nondeterministic automata. Acta Informatica, 26: 279–284, 1988.
M.Y. Vardi. On the complexity of modular model checking. In Proc. 10th LICS, pp. 101–111, 1995.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st LICS, pp. 322–331, 1986.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115 (1): 1–37, November 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Kupferman, O., Vardi, M.Y. (1998). Relating Linear and Branching Model Checking. In: Gries, D., de Roever, WP. (eds) Programming Concepts and Methods PROCOMET ’98. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35358-6_21
Download citation
DOI: https://doi.org/10.1007/978-0-387-35358-6_21
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6299-0
Online ISBN: 978-0-387-35358-6
eBook Packages: Springer Book Archive