Abstract
The introduction of Past Operators enables to produce more natural formulation of a wide class of properties of reactive systems, compared to traditional pure future temporal logics. For this reason, past temporal logics are gaining increasing interest in several application areas, ranging from Requirement Engineering to Formal Verification and Model Checking. We show how SAT-based Bounded Model Checking techniques can be extended to deal with Linear Temporal Logics with Past Operators (PLTL). Though apparently simple, this task turns out to be absolutely non-trivial when tackled in its full generality. We discuss a bounded semantics for PLTL, we show that it is correct (and complete), and propose an encoding scheme able to cope with PLTL formulas. Finally, we implement the encoding in NuSMV, and present a first experimental evaluation of the approach.
Chapter PDF
References
P. A. Abdullah, P. Bjesse, and N. Een. Symbolic Reachability Analysis based on SAT-Solvers. In Sixth Int.nl Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00), 2000.
F. Bacchus and F. Kabanza. Control Strategies in Planning. In Proc. of the AAAI Spring Symposium Series on Extending Theories of Action: Formal Theory and Practical Applications, pages 5–10, Stanford University, CA, USA, March 1995.
J. Baumgartner, A. Kuehlmann, and J. Abraham. Property Checking via Structural Analysis. In Proc. CAV’02, volume 2404, pages 151–165, 2002.
M. Benedetti and A. Cimatti. Bounded Model Checking for Past LTL. Technical Report 0301-05, ITC-Irst, Trento, Italy, 2003.
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. LNCS, 1579:193–207, 1999.
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking Using SAT Procedures instead of BDDs. In Proc. DAC’99, pages 317–320, 1999.
A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. In Proc CAV99, volume 1633 of LNCS. Springer, 1999.
J. Castro, M. Kolp, and J. Mylopoulos. A Requirements-Driven Development Methodology. In Proc. of the 13th Int.nl Conf. on Advanced Information Systems Engineering, 2001.
A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In Proc. of Int.nl Conf. on Computer-Aided Verification (CAV 2002), 2002.
A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a newSymbolic ModelVerifier. In N. Halbwachs and D. Peled, editors, Proceedings Eleventh Conference on Computer-Aided Verification (CAV’99), number 1633 in LNCS, pages 495–499, 1999.
A. Cimatti, E. Giunchiglia, M. Roveri, M. Pistore, R. Sebastiani, and A. Tacchella. Integrating BDD-based and SAT-based Symbolic Model Checking. In Proceeding of 4th International Workshop on Frontiers of Combining Systems (FroCoS’2002), 2002.
E. Clarke, O. Grumberg, and K. Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design, 10:47–71, 1997.
F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In Proceedings of CAV 2001, pages 436–453, 2001.
E.A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier Science Publisher B.V., 1990.
A. Fuxman. Formal Analysis of Early Requirements Specifications. PhD thesis, University of Toronto, Toronto, Canada, 2001.
Dov Gabbay. The Declarative Past and Imperative Future. In Proccedings of the Colloquium on Temporal Logic and Specifications, volume 398, pages 409–448. Springer-Verlag, 1987.
S. Gnesi, D. Latella, and G. Lenzini. Formal Verification of Cryptographic Protocols using History Dependent Automata. In Proc. of the 4thWorkshop on Sistemi Distribuiti: Algoritmi, Architetture e Linguaggi, 1999.
O. Kupferman, N. Piterman, and M. Vardi. Extended Temporal Logic Revisited. In Proc. 12th Int.nl Conf. on Concurrency Theory, number 2154 in LNCS, pages 519–534, 2001.
F. Laroussinie and Ph. Schnoebelen. A Hierarchy of Temporal Logics with Past. Theoretical Computer Science, 148:303–324, 1995.
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Proc. of the 38th Design Automation Conference, 2001.
M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-solver. In Proc. Int.nl Conf. on Formal Methods in Computer-Aided Design, 2000.
O. Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV’2000, volume 1855 of LNCS. Springer, 2000.
A. van Lamsweerde. Goal-Oriented Requirements Engineering:A Guided Tour. In Proc. 5th IEEE International Symposium on Requirements Engineering, pages 249–263, 2001.
M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Annual Symposium on Logic in Computer Science, 1986.
P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In Proc. CAV’2000, volume 1855 of LNCS, pages 124–138. Springer, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benedetti, M., Cimatti, A. (2003). Bounded Model Checking for Past LTL. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_3
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive