skip to main content
10.1145/1287624.1287669acmconferencesArticle/Chapter ViewAbstractPublication PagesfseConference Proceedingsconference-collections
Article

The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties

Published: 07 September 2007 Publication History

Abstract

Model checking techniques have traditionally dealt with temporal logic languages and automata interpreted over ω-words, i.e., infinite in the future but finite in the past. However, time with also an infinite past is a useful abstraction in specification. It allows one to ignore the complexity of system initialization in much the same way as system termination may be abstracted away by allowing an infinite future. One can then write specifications that are simpler and more easily understandable, because they do not include the description of the operations (such as configuration or installation) typically performed at system deployment time. The present paper is centered on the problem of satisfiability checking of linear temporal logic (LTL) formulae with past operators. We show that bounded model checking techniques can be adapted to deal with bi-infinite time in temporal logic, without incurring in any performance loss. Our claims are supported by a tool, whose application to a case study shows that satisfiability checking may be feasible also on nontrivial examples of temporal logic specifications.

References

[1]
M. Benedetti and A. Cimatti. Bounded model checking for past LTL. In Proceedings of the Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003, Warsaw, Poland, April 7-11, 2003., volume 2619 of Lecture Notes in Computer Science, pages 18--33. Springer, 2003.
[2]
D. Bianculli, A. Morzenti, M. Pradella, P. San Pietro, and P. Spoletini. Trio2Promela: a model checker for temporal metric specifications. In 29th International Conference on Software Engineering (ICSE'07), pages 61--62, Los Alamitos, CA, USA, May 2007. IEEE Computer Society. Research Demo.
[3]
D. Bianculli, P. Spoletini, A. Morzenti, M. Pradella, and P. San Pietro. Model checking temporal metric specification with Trio2Promela. In Proc. of IPM International Symposium on Fundamentals of Software Engineering (FSEN'07), Lecture Notes in Computer Science. Springer, 2007. To appear.
[4]
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. Lecture Notes in Computer Science, 1579:193--207, 1999.
[5]
A. Biere, K. Heljanko, T. Junttila, T. Latvala, and V. Schuppan. Linear encodings of bounded LTL model checking. Logical Methods in Computer Science, 2(5):1--64, 2006.
[6]
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677--691, 1986.
[7]
R. Capobianchi, A. Coen-Porisini, D. Mandrioli, and A. Morzenti. A framework architecture for supervision and control systems. ACM Comput. Surv., 32(1es):26, 2000.
[8]
E. Ciapessoni, P. Mirandola, A. Coen-Porisini, D. Mandrioli, and A. Morzenti. From formal models to formally based methods: An industrial experience. ACM Trans. Softw. Eng. Methodol., 8(1):79--113, 1999.
[9]
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 CAV '02: Proceedings of the 14th Intern. Conf. on Computer Aided Verification, pages 359-364, London, UK, 2002. Springer-Verlag.
[10]
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244--263, 1986.
[11]
E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999.
[12]
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626--643, 1996.
[13]
A. Coen-Porisini, M. Pradella, and P. San Pietro. A finite-domain semantics for testing temporal logic specifications. In Formal Techniques in Real-Time and Fault-Tolerant Systems, 5th Intern. Symposium, FTRTFT'98, Lyngby, Denmark, September 14-18, 1998, Proceedings, pages 41--54, 1998.
[14]
N. Eén and N. Sörensson. An extensible sat-solver. In E. Giunchiglia and A. Tacchella, editors, SAT, volume 2919 of Lecture Notes in Computer Science, pages 502--518. Springer, 2003.
[15]
M. Felder and A. Morzenti. Validating real-time systems by history-checking trio specifications. ACM Trans. Softw. Eng. Methodol., 3(4):308--339, 1994.
[16]
A. Gargantini and A. Morzenti. Automated deductive requirements analysis of critical systems. ACM Trans. Softw. Eng. Methodol., 10(3):255--307, 2001.
[17]
P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of the 13th Conf. on Computer Aided Verification (CAV'01), number 2102 in Lecture Notes in Computer Science, pages 53--65. Springer Verlag, 2001.
[18]
P. Gastin and D. Oddoux. LTL with past and two-way very-weak alternating automata. In Proceedings of the 28th Intern. Symposium on Mathematical Foundations of Computer Science (MFCS'03), number 2747 in Lecture Notes in Computer Science, pages 439--448. Springer Verlag, 2003.
[19]
C. Ghezzi, D. Mandrioli, and A. Morzenti. Trio: A logic language for executable specifications of real-time systems. Journal of Systems and Software, 12(2):107--123, 1990.
[20]
F. Gire and M. Nivat. Langages algébriques de mots biinfinis. Theoret. Comput. Sci., 86(2):277--323, 1991.
[21]
G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279--295, May 1997. Special Issue: Formal Methods in Software Practice.
[22]
G. J. Holzmann. The SPIN model checker: Primer and reference manual. Addison Wesley, 2004. HOL g 03:1 1.Ex.
[23]
T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is better: Efficient bounded model checking for past LTL. In R. Cousot, editor, Proceedings of the 6th Intern. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI'2005), volume 3385 of Lecture Notes in Computer Science, pages 380--395, Paris, France, January 2005. Springer-Verlag.
[24]
O. Lichtenstein, A. Pnueli, and L. D. Zuck. The glory of the past. In Proceedings of the Conf. on Logic of Programs, pages 196--218, London, UK, 1985. Springer-Verlag.
[25]
D. Mandrioli, S. Morasca, and A. Morzenti. Generating test cases for real-time systems from logic specifications. ACM Trans. Comput. Syst., 13(4):365--398, 1995.
[26]
Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York, NY, USA, 1992.
[27]
K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.
[28]
S. Morasca, A. Morzenti, and P. San Pietro. A case study on applying a tool for automated system analysis based on modular specifications written in TRIO. Autom. Softw. Eng., 7(2):125--155, 2000.
[29]
A. Morzenti, D. Mandrioli, and C. Ghezzi. A model parametric real-time logic. ACM Trans. Program. Lang. Syst., 14(4):521--573, 1992.
[30]
A. Morzenti, M. Pradella, P. San Pietro, and P. Spoletini. Model-checking TRIO specifications in SPIN. In K. Araki, S. Gnesi, and D. Mandrioli, editors, FME, volume 2805 of Lecture Notes in Computer Science, pages 542--561. Springer, 2003.
[31]
A. Morzenti and P. San Pietro. Object-oriented logical specification of time-critical systems. ACM Trans. Softw. Eng. Methodol., 3(1):56--98, 1994.
[32]
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: engineering an efficient sat solver. In DAC '01: Proceedings of the 38th Conf. on Design automation, pages 530--535, New York, NY, USA, 2001. ACM Press.
[33]
D. Perrin and J. Éric Pin. Infinite Words, volume 141 of Pure and Applied Mathematics. Elsevier, 2004. ISBN 0-12-532111-2.
[34]
A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-77), pages 46--57, Providence, Rhode Island, 31- 2 1977. IEEE Computer Society Press.
[35]
M. Pradella, P. San Pietro, P. Spoletini, and A. Morzenti. Practical model checking of LTL with Past. In ATVA03, Taipei, Taiwan, 2003, 2003.
[36]
P. San Pietro, A. Morzenti, and S. Morasca. Generation of execution sequences for modular time critical systems. IEEE Trans. Software Eng., 26(2):128--149, 2000.
[37]
M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a SAT-solver. In FMCAD00, volume 1954 of LNCS, pages 108--125. Springer-Verlag, 2000.
[38]
F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 248--263. Springer, 2000.
[39]
M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, LICS'86, Cambridge, MA, USA, 16-18 June 1986, pages 332--344, Washington, DC, 1986. IEEE Computer Society Press.
[40]
P. Wolper. Temporal logic can be more expressive. In FOCS, pages 340-348. IEEE, 1981.

Cited By

View all
  • (2015)Specifying event-based systems with a counting fluent temporal logicProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818843(733-743)Online publication date: 16-May-2015
  • (2015)Specifying Event-Based Systems with a Counting Fluent Temporal Logic2015 IEEE/ACM 37th IEEE International Conference on Software Engineering10.1109/ICSE.2015.86(733-743)Online publication date: May-2015
  • (2014)Checking MTL Properties of Discrete Timed Automata via Bounded Model CheckingFundamenta Informaticae10.5555/2692080.2692095135:4(553-568)Online publication date: 1-Oct-2014
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering
September 2007
638 pages
ISBN:9781595938114
DOI:10.1145/1287624
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 September 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. bi-infinite time
  2. bounded model checking
  3. satisfiability checking
  4. temporal logic

Qualifiers

  • Article

Conference

ESEC/FSE07
Sponsor:

Acceptance Rates

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1
  • Downloads (Last 6 weeks)1
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2015)Specifying event-based systems with a counting fluent temporal logicProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818843(733-743)Online publication date: 16-May-2015
  • (2015)Specifying Event-Based Systems with a Counting Fluent Temporal Logic2015 IEEE/ACM 37th IEEE International Conference on Software Engineering10.1109/ICSE.2015.86(733-743)Online publication date: May-2015
  • (2014)Checking MTL Properties of Discrete Timed Automata via Bounded Model CheckingFundamenta Informaticae10.5555/2692080.2692095135:4(553-568)Online publication date: 1-Oct-2014
  • (2014)Offline Trace Checking of Quantitative Properties of Service-Based ApplicationsProceedings of the 2014 IEEE 7th International Conference on Service-Oriented Computing and Applications10.1109/SOCA.2014.14(9-16)Online publication date: 17-Nov-2014
  • (2014)SMT-Based Checking of SOLOIST over Sparse TracesProceedings of the 17th International Conference on Fundamental Approaches to Software Engineering - Volume 841110.1007/978-3-642-54804-8_19(276-290)Online publication date: 5-Apr-2014
  • (2013)Lightweight analysis of software design models at the whiteboardProceedings of the 5th International Workshop on Modeling in Software Engineering10.5555/2662737.2662743(18-23)Online publication date: 18-May-2013
  • (2013)Bounded satisfiability checking of metric temporal logic specificationsACM Transactions on Software Engineering and Methodology10.1145/2491509.249151422:3(1-54)Online publication date: 30-Jul-2013
  • (2013)Lightweight analysis of software design models at the whiteboard2013 5th International Workshop on Modeling in Software Engineering (MiSE)10.1109/MiSE.2013.6595291(18-23)Online publication date: May-2013
  • (2013)The Tale of SOLOIST: A Specification Language for Service Compositions InteractionsFormal Aspects of Component Software10.1007/978-3-642-35861-6_4(55-72)Online publication date: 2013
  • (2012)Towards the verification of multi-diagram UML modelsProceedings of the 34th International Conference on Software Engineering10.5555/2337223.2337475(1531-1534)Online publication date: 2-Jun-2012
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media