Abstract
There exist different semantics for Linear Temporal Logic (LTL) in terms of finiteness of the considered traces. Although several ones can be useful depending on the verification context, no verification framework handle their diversity in a simple way. Another limitation of current LTL verification tools is the treatment of concrete domains (bounded and infinite integers, real numbers, etc.). We present an approach to LTL model checking on both finite and infinite traces with concrete domains. Our method is based on an SMT solver and on Bounded Model Checking (BMC). We also present some experiments and compare our tool with NuSMV and nuXmv.
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
Similar content being viewed by others
References
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI 2013, pp. 854–860. AAAI Press (2013)
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: International Conference on Computer Aided Verification (2003)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer, Heidelberg (1991). https://doi.org/10.1007/978-1-4612-0931-7
Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: CAV, Denmark, Copenhagen (2002)
Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22
Macedo, N., Brunel, J., Chemouil, D., Cunha, A.: Pardinus: a temporal relational model finder. J. Autom. Reason. 66(4), 861–904 (2022)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis, revised edn. MIT Press, Cambridge (2012)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)
Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods Comput. Sci. 2 (2006)
Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281–283 (1979)
Pakonen, A.: Model-checking infinite-state nuclear safety I &C systems with nuXmv. In: 19th IEEE International Conference on Industrial Informatics, INDIN 2021, Palma de Mallorca, Spain, 21–23 July 2021, pp. 1–6. IEEE (2021)
Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 397–413. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24372-1_28
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. 12(2), 123–137 (2010)
Wulf, M.D. , Doyen, L., Maquet, N., Raskin, J.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: TACAS, Budapest (2008)
Li, J., Pu, G., Zhang, L., Vardi, M.Y., He, J.: Fast LTL satisfiability checking by SAT solvers. CoRR arxiv:1401.5677 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Doose, D., Brunel, J. (2024). Simple LTL Model Checking on Finite and Infinite Traces over Concrete Domains. In: Ogata, K., Mery, D., Sun, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2024. Lecture Notes in Computer Science, vol 15394. Springer, Singapore. https://doi.org/10.1007/978-981-96-0617-7_21
Download citation
DOI: https://doi.org/10.1007/978-981-96-0617-7_21
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-96-0616-0
Online ISBN: 978-981-96-0617-7
eBook Packages: Computer ScienceComputer Science (R0)