On the model checking problem for branching time logics and basic parallel processes

  • Javier Esparza
  • Astrid Kiehn
Session 10: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


We investigate the model checking problem for branching time logics and Basic Parallel Processes. We show that the problem is undecidable for the logic ∀L(O, F, U) (equivalent to CTL*) in the usual interleaving semantics, but decidable in a standard partial order interpretation.


Model Check Transition Rule Label Transition System Input Place Linear Time Temporal Logic 
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.


  1. 1.
    J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Computation 60:109–137, 1984.Google Scholar
  2. 2.
    O. Burkart and B. Steffen. Model checking for context-free processes. In Proceedings of CONCUR '92, LNCS 630:123–137, 1992.Google Scholar
  3. 3.
    S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation Equivalence is Decidable for all Basic Parallel Processes. In Proceedings of CONCUR '93, LNCS 715:143–157, 1993.Google Scholar
  4. 4.
    S. Christensen, H. Hüttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-free Processes. In Proceedings of CONCUR '92, LNCS 630:138–147, 1992.Google Scholar
  5. 5.
    E.M. Clarke and E.A. Emerson. Design and Synthesis of synchronization skeletons using Branching Time Temporal Logic. In Proceedings of Workshop on Logics of Programs, LNCS 131:52–71, 1981.Google Scholar
  6. 6.
    E.A. Emerson. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, Volume B, 995–1072, 1990.Google Scholar
  7. 7.
    E.A. Emerson and J.Y. Halpern. “Sometimes” and “Not Never” revisited: on Branching versus Linear Time Temporal Logic. Journal of the ACM 33(1):151–178, 1986.CrossRefGoogle Scholar
  8. 8.
    E.A. Emerson and C. S. Jutla. Tree Automata, Mu-Calculus and Determinacy. In Proceedings of FOCS '91, 1991.Google Scholar
  9. 9.
    J. Engelfriet. Branching processes of Petri nets. Acta Informatica 28:575–591, 1991.CrossRefGoogle Scholar
  10. 10.
    J. Esparza. On the Decidability of the Model Checking Problem for Several μcalculi and Petri Nets. In Proceedings of CAAP '94, LNCS 787:115–129, 1994.Google Scholar
  11. 11.
    J. Esparza. On the uniform word problem for commutative context-free grammars. Submitted for publication, 1994.Google Scholar
  12. 12.
    R. Gorrieri and U. Montanari. A Simple Calculus of Nets. In Proceedings of CONCUR '90, LNCS 458:2–30, 1990.Google Scholar
  13. 13.
    Y. Hirshfeld. Petri Nets and the Equivalence Problem. In Proceedings of CSL '93, 1994.Google Scholar
  14. 14.
    H. Hungar and B. Steffen. Local Model Checking for Context-Free Processes. In Proceedings of ICALP '93, LNCS 707, 1993.Google Scholar
  15. 15.
    D. Muller and P. Schupp. The Theory of Ends, Pushdown Automata and Second Order Logic, Theoretical Computer Science 37: 51–75, 1985.CrossRefGoogle Scholar
  16. 16.
    M. Minsky: Computation. Finite and Infinite Machines. Prentice-Hall, 1967.Google Scholar
  17. 17.
    D. Peled, S. Katz, and A. Pnueli. Specifying and Proving Serializability in Temporal Logic. In Proceedings of LICS '91, 232–245, 1991.Google Scholar
  18. 18.
    W. Penczek. Temporal Logics for Trace Systems: On Automated Verification. International Journal on Foundations of Computer Science 33:31–67, 1992.Google Scholar
  19. 19.
    M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141:1–35, 1969.Google Scholar
  20. 20.
    C. Stirling. Modal and Temporal Logics. In Handbook of Logic in Computer Science, Oxford University Press, 1991.Google Scholar
  21. 21.
    P.S. Thiagarajan. A Trace Based Extension of PTL. In Proceedings of LICS '94, 1994.Google Scholar
  22. 22.
    P. Wolper. Temporal Logic can be more expressive. Information and Control 56(1,2):72–93, 1983.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Javier Esparza
    • 1
  • Astrid Kiehn
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchen

Personalised recommendations