Yet Another Look at LTL Model Checking

  • Klaus Schneider
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


A subset of LTL is presented that can be translated to ω automata with only a linear number of states. The translation is completely based on closures under temporal and boolean operators. Moreover, it is shown how this enhancement can be combined with traditional translations so that all LTL formulas can be translated. Exponential savings are possible in terms of reachable states, as well as in terms of runtime and memory requirements for model checking.


Model Check Temporal Logic Reachable State Acceptance Condition Propositional Formula 
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.
    K. Schneider and D. Hoffmann. A HOL conversion for translating linear time temporal logic to ω-automata. In Higher Order Logic Theorem Proving and its Applications, LNCS, Nice, France, September 1999. Springer Verlag.Google Scholar
  2. 2.
    E. M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Conference on Computer Aided Verification (CAV), LNCS 818, pp. 415–427, Standford, California, USA, June 1994. Springer-Verlag.Google Scholar
  3. 3.
    G.G de Jong. An automata theoretic approach to temporal logic. In Computer Aided Verification (CAV), LNCS 575, pp. 477–487, Aalborg, July 1991. Springer-Verlag.Google Scholar
  4. 4.
    W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191, Amsterdam, 1990. Elsevier Science Publishers.Google Scholar
  5. 5.
    K. Schneider. CTL and equivalent sublanguages of CTL✻. In C. Delgado Kloos, editor, IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL), pp. 40–59, Toledo, Spain, April 1997. IFIP, Chapman and Hall.Google Scholar
  6. 6.
    K. Schneider. Model checking on product structures. In Formal Methods in Computer-Aided Design, LNCS 1522, pp. 483–500, Palo Alto, CA, November 1998. Springer Verlag.CrossRefGoogle Scholar
  7. 7.
    O. Kupferman and M. Y. Vardi. Freedom, weakness, and determinism: From lineartime to branching-time. In IEEE Symposium on Logic in Computer Science, 1998.Google Scholar
  8. 8.
    K. Wagner. On ✻ regular sets. Information and control, 43:123–177, 1979.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Klaus Schneider
    • 1
  1. 1.Department of Computer Science Institute for Computer Design and Fault ToleranceUniversity of KarlsruheKarlsruheGermany

Personalised recommendations