Abstract
Model checking techniques traditionally deal with temporal logic languages and automata interpreted over ω-words, i.e., where time is infinite in the future but finite in the past. This is motivated by the study of reactive systems, which are typically nonterminating: system termination may be abstracted away by allowing an infinite future. In the same way, if time is infinite also in the past one is allowed to ignore the complexity of system initialization. Specifications may then be simpler and more easily understandable, because they do not necessarily include the description of operations (such as configuration or installation) typically performed at system deployment time. In this paper, we investigate the feasibility of bounded model checking and bounded satisfiability checking when dealing with bi-infinite automata and logics. We present a tool and we discuss its application to a set of case studies, arguing that bi-infinite time does not entail significant penalties in verification time and space.
Work partially supported by FME Small Project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18–33. Springer, Heidelberg (2003)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science 2(5), 1–64 (2006)
Capobianchi, R., Coen-Porisini, A., Mandrioli, D., Morzenti, A.: A framework architecture for supervision and control systems. ACM Comput. Surv. 32(1es), 26 (2000)
Ciapessoni, E., Mirandola, P., Coen-Porisini, A., Mandrioli, D., Morzenti, A.: From formal models to formally based methods: An industrial experience. ACM Trans. Softw. Eng. Methodol. 8(1), 79–113 (1999)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Furia, C.A., Pradella, M., Rossi, M.: Dense-time MTL verification through sampling. In: Cuellar, J., Maibaum, T.S.E. (eds.) FM 2008. LNCS, vol. 5014. Springer, Heidelberg (2008)
Ghezzi, C., Mandrioli, D., Morzenti, A.: TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and Software 12(2), 107–123 (1990)
Gire, F., Nivat, M.: Langages algébriques de mots biinfinis. Theoret. Comput. Sci. 86(2), 277–323 (1991)
Heitmeyer, C., Mandrioli, D.: Formal Methods for Real-Time Computing. John Wiley & Sons, Inc., New York (1996)
Kamp, J.A.W.: Tense Logic and the Theory of Linear Order (Ph.D. thesis). University of California at Los Angeles (1968)
Lamport, L.: A fast mutual exclusion algorithm. ACM TOCS-Transactions On Computer Systems 5(1), 1–11 (1987)
Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple is better: Efficient bounded model checking for past LTL. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 380–395. Springer, Heidelberg (2005)
Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT solving. In: 12th Asia and South Pacific Design Automation Conference (2007)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Proceedings of the Conf. on Logic of Programs, London, UK, pp. 196–218. Springer, Heidelberg (1985)
Morasca, S., Morzenti, A., San Pietro, P.: A case study on applying a tool for automated system analysis object oriented logic specification of time-critical systems. Based on modular specifications written in TRIO. Autom. Softw. Eng. 7(2), 125–155 (2000)
Morzenti, A., Mandrioli, D., Ghezzi, C.: A model parametric real-time logic. ACM Trans. Program. Lang. Syst. 14(4), 521–573 (1992)
Morzenti, A., Pradella, M., San Pietro, P., Spoletini, P.: Model-checking TRIO specifications in SPIN. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 542–561. Springer, Heidelberg (2003)
Morzenti, A., San Pietro, P.: Object-oriented logical specification of time-critical systems. ACM Trans. Softw. Eng. Methodol. 3(1), 56–98 (1994)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC 2001: Proceedings of the 38th Conf. on Design automation, pp. 530–535. ACM Press, New York (2001)
Perrin, D., Pin, J.-É.: Infinite Words. Pure and Applied Mathematics, vol. 141. Elsevier, Amsterdam (2004)
Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future: Bi-infinite time in the verification of temporal properties. In: Proc. of The 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering ESEC/FSE, Dubrovnik, Croatia (September 2007)
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pradella, M., Morzenti, A., San Pietro, P. (2008). Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)