SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems

• Autorzy: Woźna-Szcześniak, B.
• Języki publikacji: EN

Abstrakty

EN

We present WECTL*KD, a weighted branching time temporal logic to specify knowledge, and correct functioning behaviour in multi-agent systems (MAS).We interpret the formulae of the logic over models generated by weighted deontic interpreted systems (WDIS). Furthermore, we investigate a SAT-based bounded model checking (BMC) technique for WDIS and for WECTL*KD.

Słowa kluczowe

EN

bounded arithmetics; deontic logic; mathematical formulas; branching processes; data analysis

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 1/2
• Strony: 173--205
• Opis fizyczny: Bibliogr. 29 poz., rys., tab.

Twórcy

autor

Woźna-Szcześniak, B.

• IM&CS, Jan Długosz University in Częstochowa, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland,

Bibliografia

• [1] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), volume 1579 of LNCS, pages 193–207. Springer-Verlag, 1999.
• [2] A. Biere, 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.
• [3] 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.
• [4] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
• [5] E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, chapter 16, pages 996–1071. Elsevier Science Publishers, 1990.
• [6] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, 1995.
• [7] C. A. Furia and P. Spoletini. Tomorrow and all our yesterdays: MTL satisfiability over the integers. In Proceedings of the Theoretical Aspects of Computing (ICTAC’2008), volume 5160 of LNCS, pages 253–264. Springer-Verlag, 2008.
• [8] X. Huang, C. Luo, and R. van der Meyden. Improved bounded model checking for a fair branching-time temporal epistemic logic. In Proceedings of the 6th International Workshop on Model Checking and Artificial Intelligence (MoChArt 2010), volume 6572 of LNAI, pages 95–111. Springer, 2011.
• [9] 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.
• [10] A. Lomuscio and M. Sergot. Deontic interpreted systems. Studia Logica, 75(1):63–92, 2003.
• [11] Artur Męski, 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.
• [12] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167–185, 2003.
• [13] W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135–156, 2002.
• [14] M. Pradella, A. Morzenti, and P. San Pietro. The Symmetry of the Past and of the Future: Bi-infinite Time in the Verification of Temporal Properties. In Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE ’07, pages 312–320. ACM, 2007.
• [15] M. Pradella, A. Morzenti, and P. San Pietro. A Metric Encoding for Bounded Model Checking. In 16th International Symposium on Formal Methods (FM 2009), volume 5850 of LNCS, pages 741–756. Springer-Verlag, 2009.
• [16] M. Wooldridge. An introduction to multi-agent systems - Second Edition. John Wiley & Sons, 2009.
• [17] B. Woźna. Bounded Model Checking for the universal fragment of CTL*. Fundamenta Informaticae, 63(1):65–87, 2004.
• [18] B. Woźna, A. Lomuscio, and W. Penczek. Bounded model checking for deontic interpreted systems. In Proceedings of the 2nd International Workshop on Logic and Communication in Multi-Agent Systems (LCMAS’2004), volume 126 of ENTCS, pages 93–114. Elsevier, 2005.
• [19] B. Woźna-Szcześniak. SAT-based bounded model checking for weighted deontic interpreted systems. In Proceedings of 15th Portuguese Conference on Artificial Intelligence (EPIA’2013), volume 8154 of LNAI, pages 444–455. Springer-Verlag, 2013.
• [20] B. Woźna-Szcześniak, I. Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. Bounded model checking for weighted interpreted systems and for flat weighted epistemic computation tree logic. In Proceedings of 17th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA’2014), volume 8861 of LNAI, pages 107–115. Springer, 2014.
• [21] B. Woźna-Szcześniak and A. Zbrzezny. SAT-based BMC for Deontic Metric Temporal Logic and Deontic Interleaved Interpreted Systems. In Post-proceedings of the 10th International Workshop on Declarative Agent Languages and Technologies (DALT’2012), volume 7784 of LNAI, pages 170–189. Springer, 2012.
• [22] B. Woźna-Szcześniak and A. Zbrzezny. SAT-based bounded model checking for deontic interleaved interpreted systems. In The Proceedings of the 6th KES International Conference on Agent and Multi-Agent Systems, Technologies and Applications (KES-AMSTA’2012), volume 7327 of LNCS, pages 494–503. Springer-Verlag, 2012.
• [23] 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 In Proceedings of the 15th Portuguese Conference on Artificial Intelligence (EPIA’2011), volume 7026 of LNAI, pages 551–565. Springer-Verlag, 2011.
• [24] B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. Verifying RTECTL properties of a train controller system. Scientific Issues of Jan Długosz University in Częstochowa: Mathematica, 16:153–162, 2011.
• [25] B.Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. SAT-based Bounded Model Checking for RTECTL and Simply-timed systems. In Proceedings of the 10th European Workshop on Performance Engineering (EPEW’2013), volume 8168 of LNCS, pages 337–349. Springer-Verlag, 2013.
• [26] B.Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. SAT-Based Bounded Model Checking for Weighted Interpreted Systems and Weighted Linear Temporal Logic. In Proceedings of the 16th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA’2013), volume 8291 of LNAI, pages 355–371. Springer-Verlag, 2013.
• [27] A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1-4):513–531, 2008.
• [28] A. Zbrzezny. A new translation from ECTL_ to SAT. Fundamenta Informaticae, 120(3-4):377–397, 2012.
• [29] A. M. Zbrzezny, B. Woźna-Szcześniak, and A. Zbrzezny. SMT-based Bounded Model Checking for Weighted Interpreted Systems and for Weighted Epistemic ECTL (Short paper). In Proceedings of the 14th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS’2015), pages 1671–1672. IFAAMAS Press, 2015.

Identyfikatory

DOI

10.3233/FI-2016-1310