Bounded Model Search in Linear Temporal Logic and Its Application to Planning

  • Serenella Cerrito
  • Marta Cialdea Mayer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


In this work a tableau calculus is proposed, that checks whether a finite set of formulae in propositional linear temporal logic (LTL) has a finite model whose cardinality is bounded by a constant given in input, and constructs such a model, if any. From a theoretical standpoint, the method can also be used to check finite satisfiability tout court. The following properties of the proposed calculus are proved: termination, soundness and completeness w.r.t. finite model construction. The motivation behind this work is the design of a logical language to model planning problems and an associated calculus for plan construction, integrating the declarativity, expressiveness and flexibility typical of the logical languages with the capability of embedding search-based techniques well established in the planning community.


Temporal Logic Linear Temporal Logic Planning Language Linear Temporal Logic Formula Open Branch 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Fahiem Bacchus and Froduald Kabanza. Planning for temporally extended goals. In Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), pages 1215–1222. AAAI Press / The MIT Press, 1996.Google Scholar
  2. 2.
    H. Barringer, M. Fisher, D. Gabbay, G. Gough, and R. Owens. METATEM: a framework for programming in temporal logic. In Proc. of REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS. Springer, 1989.Google Scholar
  3. 3.
    H. Barringer, M. Fisher, D. Gabbay, and A. Hunter. Meta-reasoning in executable temporal logic. In Proc. of the Second Int. Conf. on Principles of Knowledge Representation and Reasoning, 1991.Google Scholar
  4. 4.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    T. Bylander. Complexity results for planning. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI-91), pages 274–279, 1991.Google Scholar
  6. 6.
    S. Cerrito and M. Cialdea Mayer. TabPlan: Planning in linear temporal logic. Technical Report 1141, Université de Paris Sud, Laboratoire de Recherche en Informatique, 1997.Google Scholar
  7. 7.
    T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT press, 1990.Google Scholar
  8. 8.
    K. Currie and A. Tate. O-Plan: the open planning architecture. Journal of Artificial Intelligence, 52:49–86, 1991.CrossRefGoogle Scholar
  9. 9.
    K. Erol, J. Hendler, and D. S. Nau. Complexity results for HTN planning. In Proceedings of AAAI-94, 1994.Google Scholar
  10. 10.
    R. E. Fikes and N.J. Nilsson. STRIPS: a new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2(3–4):189–208, 1971.zbMATHCrossRefGoogle Scholar
  11. 11.
    R. Hähnle and O. Ibens. Improving temporal logic tableaux using integer constraints. In D. M. Gabbay and H. J. Ohlbach, editors, Proceedings of the First International Conference on Temporal Logic (ICTL 94), volume 827 of LNCS, pages 535–539. Springer, 1994.Google Scholar
  12. 12.
    H. Kautz and B. Selman. Planning as satisfiability. In B. Neumann, editor, 10th European Conference on Artificial Intelligence (ECAI), pages 360–363. Wiley & Sons, 1992.Google Scholar
  13. 13.
    J. Koehler and R. Treinen. Constraint deduction in an interval-based temporal logic. In M. Fisher and R. Owens, editors, Executable Modal and Temporal Logics, (Proc. of the IJCAI’93 Workshop), volume 897 of LNAI, pages 103–117. Springer, 1995.Google Scholar
  14. 14.
    M. Masseron. Generating plans in linear logic: II. A geometry of conjunctive actions. Theoretical Computer Science, 113:371–375, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    M. Masseron, C. Tollu, and J. Vauzeilles. Generating plans in linear logic: I. Actions as proofs. Theoretical Computer Science, 113:349–370, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    R. Reiter. The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. In V. Lifschitz, editor, Artificial Intelligence and mathematical theory of computation: Papers in honor of John McCarthy, pages 359–380. Academic Press, 1991.Google Scholar
  17. 17.
    P.H. Schmitt and J. Goubault-Larrecq. A tableau system for full linear temporal logic. Draft.Google Scholar
  18. 18.
    P.H. Schmitt and J. Goubault-Larrecq. A tableau system for linear-time temporal logic. In E. Brinksma, editor, 3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), LNCS. Springer Verlag, 1997.Google Scholar
  19. 19.
    J. Scott Penberthy and D.S Weld. UCPOP: A sound, complete, partial order planner for ADL. In Proc. of the Third Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’92), pages 103–114. Morgan Kauffman Publ., 1992.Google Scholar
  20. 20.
    A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733–749, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    B. Stephan and S. Biundo. Deduction based refinement planning. In B. Drabble, editor, Proceedings of the 3rd International Conference on Artificial Intelligence Planning Systems (AIPS-96), pages 213–220. AAAI Press, 1996.Google Scholar
  22. 22.
    P. Wolper. The tableau method for temporal logic: an overview. Logique et Analyse, 28:119–152, 1985.zbMATHMathSciNetGoogle Scholar
  23. 23.
    Q. Yang. Formalizing planning knowledge for hierarchical planning. Computational Intelligence, 6:12–24, 1990.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Serenella Cerrito
    • 1
  • Marta Cialdea Mayer
    • 2
  1. 1.LRI, Bât 490Université de Paris-SudOrsay CedexFrance
  2. 2.Dipartimento di Informatica e AutomazioneUniversità di Roma TreRomaItalia

Personalised recommendations