Abstract
We investigate a SAT-based bounded model checking (BMC) method for EMTLK (the existential fragment of the metric temporal logic with knowledge) that is interpreted over timed models generated by timed interpreted systems. In particular, we translate the existential model checking problem for EMTLK to the existential model checking problem for a variant of linear temporal logic (called HLTLK), and we provide a SAT-based BMC technique for HLTLK. We evaluated the performance of our BMC by means of a variant of a timed generic pipeline paradigm scenario and a timed train controller system.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur R., Henzinger T. A.: Real-time logics: complexity and expressiveness. Information and Computation 104, 390–401 (1993)
Alur R., Feder T., Henzinger T.: The benefits of relaxing punctuality. Journal of the ACM 43(1), 116–146 (1996)
Biere A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 4, 75–97 (2008)
Biere, A., K. Heljanko, T. Junttila, T. Latvala, and V. Schuppan, Linear encodings of bounded ltl model checking, Logical Methods in Computer Science 2(5:5):1–64, 2006.
Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic, vol. 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 2001.
Cabodi, G., P. Camurati, and S. Quer, Can BDDs compete with SAT solvers on bounded model checking?, in Proceedings of the 39th Annual Design Automation Conference (DAC’2002), ACM, New York, 2002, pp. 117–122.
Clarke E., Biere A., Raimi R., Zhu Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Emerson, E. A., Temporal and modal logic, in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, vol. B, Chap. 16, Elsevier Science Publishers, 1990, pp. 996–1071.
Fagin, R., J. Y. Halpern, Y. Moses, and M. Y. Vardi, Reasoning about Knowledge, MIT Press, Cambridge, 1995.
Furia, C. A., and P. Spoletini, Tomorrow and all our yesterdays: MTL satisfiability over the integers, in Proceedings of the Theoretical Aspects of Computing (ICTAC’2008), vol. 5160 of LNCS. Springer-Verlag, New York, 2008, pp. 253–264.
Gammie, P., and R. van der Meyden, MCK: Model checking the logic of knowledge, in Proceedings of 16th International Conference on Computer Aided Verification (CAV’04), vol. 3114 of LNCS, Springer-Verlag, New York, 2004, pp. 479–483.
Huang, X., and R. van der Meyden, The complexity of epistemic model checking: Clock semantics and branching time, in Proceedings of the 2010 Conference on ECAI 2010: 19th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2010, pp. 549–554.
Levesque, H., A logic of implicit and explicit belief, in Proceedings of the 6th National Conference of the AAAI, Morgan Kaufman, Palo Alto, 1984, pp. 198–202.
Lomuscio A., Sergot M.: Deontic interpreted systems. Studia Logica 75(1), 63–92 (2003)
Lomuscio, A., W. Penczek, and B. Woźna, Bounded model checking for knowledge and real time, Artificial Intelligence 171:1011–1038, 2007.
Lomuscio, A., H. Qu, and F. Raimondi, Mcmas: A model checker for the verification of multi-agent systems, in Proceedings of the 21st International Conference on Computer Aided Verification (CAV 2009), vol. 5643 of LNCS, Springer-Verlag, New York, 2009, pp. 682–688.
Mȩski, A., W. Penczek, M. Szreter, B. Woźna-Szcześniak, and A. Zbrzezny, BDD- versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance, Autonomous Agents and Multi-Agent Systems 28(4):558–604, 2014.
Peled, D., All from one, one for all: On model checking using representatives, in Proceedings of the 5th International Conference on Computer Aided Verification (CAV’93), vol. 697 of LNCS, Springer-Verlag, New York, 1993, pp. 409–423.
Penczek, W., and A. Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae 55(2):167–185, 2003.
Tripakis, S., Minimization of timed systems. http://verimag.imag.fr/~tripakis/dea.ps.gz, 1998.
Wooldridge M.: An introduction to multi-agent systems. Wiley, Chichester (2002)
Woźna-Szcześniak, B., and A. Zbrzezny, A translation of the existential model checking problem from MITL to HLTL, Fundamenta Informaticae 122(4):401–420, 2013.
Woźna-Szcześniak, B., and A. Zbrzezny, Checking MTL properties of discrete timed automata via bounded model checking, Fundamenta Informaticae 135(4):553–568, 2014.
Zbrzezny A.: A new translation from ECTL* to SAT. Fundamenta Informaticae 120(3–4), 377–397 (2012)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Woźna-Szcześniak, B., Zbrzezny, A. Checking EMTLK Properties of Timed Interpreted Systems Via Bounded Model Checking. Stud Logica 104, 641–678 (2016). https://doi.org/10.1007/s11225-015-9637-9
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-015-9637-9