SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties

• Autorzy: Woźna-Szcześniak B. , Szcześniak I.

Identyfikatory

DOI

dx.doi.org/10.16926/m.2015.20.08

• Języki publikacji: EN

Abstrakty

EN

We define an SAT-based bounded model checking (BMC) method for RTECTLK (the existential fragment of the real-time computation tree logic with knowledge) that is interpreted over timed models generated by timed interpreted systems. Specifically, we translate the model checking problem for RTECTLK to the model checking problem for a variant of branching temporal logic (called E_yCTLK) interpreted over an abstract model, and we redefine an SAT-based BMC technique for E_yCTLK.

Słowa kluczowe

EN

timed models; timed logic; computation tree

PL

model czasowy; logika czasowa; drzewo obliczeń

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2015
• Tom: Vol. 20
• Strony: 69--81
• Opis fizyczny: Bibliogr. 16 poz.

Twórcy

autor

Woźna-Szcześniak B.

• Jan Długosz University in Czestochowa Institute of Mathematics and Computer Science Al. Armii Krajowej 13/15, 42-200 Czestochowa, Poland

autor

Szcześniak I.

• Czestochowa University of Technology Institute of Computer and Information Sciences ul. Dabrowskiego 69, 42-201 Czestochowa, Poland

Bibliografia

• [1] R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(1):2-34, 1993.
• [2] E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7-34, 2001.
• [3] E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 16, pages 996-1071. Elsevier Science Publishers, 1990.
• [4] E. A. Emerson, A.K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Real-Time Systems, 4(4):331-352, December 1992.
• [5] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [6] J. Gu, P. Purdom, J. Franco, and B. Wah. Algorithms for the satisfiability (SAT) problem: a survey. In Satisfiability Problem: Theory and Applications, volume 35 of Discrete Mathematics and Theoretical Computer Science (DIMASC), pages 19-152. American Mathematical Society, 1996.
• [7] H. Levesque. A logic of implicit and explicit belief. In Proceedings of the 6th National Conference of the AAAI, pages 198-202. Morgan Kaufman, 1984.
• [8] A. Lomuscio, W. Penczek, and B. Woźna. Bounded model checking for knowledge and real time. Artificial Intelligence, 171:1011-1038, 2007.
• [9] A. Lomuscio and M. Sergot. Deontic interpreted systems. Studia Logica, 75(1):63-92, 2003.
• [10] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167-185, 2003.
• [11] M. Wooldridge. An introduction to multi-agent systems. John Wiley & Sons, 2002.
• [12] B. Woźna-Szcześniak. Bounded model checking for the existential part of Real-Time CTL and knowledge. In Proceedings of 4th IFIP TC2 Central and Eastern European Conference on Software Engineering Techniques, pages 178-191, 2009.
• [13] B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. The BMC method for the existential part of RTCTLK and interleaved interpreted systems. In Proceedings of the 15th Portuguese Conference on Artificial Intelligence (EPIA’2011), volume 7026 of LNAI, pages 551-565. Springer-Verlag, 2011.
• [14] Bożena Woźna-Szcześniak. Checking EMTLK properties of timed interpreted systems via bounded model checking. In Proceedings of the 2014 International Conference on Autonomous Agents and Multi-agent Systems, pages 1477-1478. IFAAMS, 2014.
• [15] A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1-4):513-531, 2008.
• [16] A. Zbrzezny. A new translation from ECTL* to SAT. Fundamenta Informaticae, 120(3-4):377-397, 2012.