Abstract
We present a new translation of Metric Temporal Logic with knowledge operators (MTLK) to the Linear Temporal Logic with knowledge operators and with a new set of the atomic propositions (\({\mathrm{{\mathrm{{LTL}}}}_\mathrm{q}\mathrm {K}}\)). We investigate a SAT-based bounded model checking (BMC) method for MTLK. The semantics of MTLK is defined over timed interpreted systems (TIS). We show how to implement the bounded model checking technique for \({\mathrm{{\mathrm{{LTL}}}}_\mathrm{q}\mathrm {K}}\) and timed interpreted systems, and as a case study, we apply the technique in the analysis of the Timed Generic Pipeline Paradigm modelled by TIS. We also present the differences between the old translation of MTLK and the new one. The theoretical description is supported by the experimental results that demonstrate the efficiency of the method.
Partly supported by National Science Centre under the grant No. 2014/15/N/ST6/05079.
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
References
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)
Męski, A., Penczek, W., Szreter, M., Woźna-Szcześniak, B., Zbrzezny, A.: Bdd-versus sat-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Auton. Agent. Multi-Agent Syst. 28(4), 558–604 (2014)
Wooldridge, M.: An Introduction to Multi-agent Systems, 2nd edn. Wiley, New York (2009)
Woźna-Szcześniak, B., Zbrzezny, A.: Checking EMTLK properties of timed interpreted systems via bounded model checking. Studia Logica 104(4), 641–678 (2016)
Zbrzezny, A.: A new translation from ECTL\(^*\) to SAT. Fundamenta Informaticae 120(3–4), 377–397 (2012)
Zbrzezny, A.M., Zbrzezny, A.: Simple bounded MTL model checking for discrete timed automata (extended abstract). In: Proceedings of CS&P 2016, pp. 37–48 (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Zbrzezny, A.M., Zbrzezny, A. (2018). Simple Bounded MTLK Model Checking for Timed Interpreted Systems. In: Jezic, G., Kusek, M., Chen-Burger, YH., Howlett, R., Jain, L. (eds) Agent and Multi-Agent Systems: Technology and Applications. KES-AMSTA 2017. Smart Innovation, Systems and Technologies, vol 74. Springer, Cham. https://doi.org/10.1007/978-3-319-59394-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-59394-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-59393-7
Online ISBN: 978-3-319-59394-4
eBook Packages: EngineeringEngineering (R0)