Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

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

Treść / Zawartość
Warianty tytułu
Języki publikacji
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 EyCTLK) interpreted over an abstract model, and we redefine an SAT-based BMC technique for EyCTLK.
  • Jan Długosz University in Czestochowa Institute of Mathematics and Computer Science Al. Armii Krajowej 13/15, 42-200 Czestochowa, Poland
  • Czestochowa University of Technology Institute of Computer and Information Sciences ul. Dabrowskiego 69, 42-201 Czestochowa, Poland
  • [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.
Typ dokumentu
Identyfikator YADDA
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.