Abstract
The paper deals with the SAT- and ROBDD-based bounded model checking (BMC) methods for the existential fragment of a flat weighted epistemic computation tree logic (FWECTLK) interpreted over weighted interpreted systems. We implemented the both BMC algorithms, and compared them with each other on several benchmarks for multi-agent systems.
Partly supported by National Science Centre under the grant No. 2011/01/B/ST6/ 05317.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation 4, 75–97 (2008)
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers 35(8), 677–691 (1986)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (1999)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)
Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)
Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press (2000)
Jones, A.V., Lomuscio, A.: Distributed BDD-based BMC for the verification of multi-agent systems. In: Proc. of AAMAS 2010, pp. 675–682. IFAAMAS (2010)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)
Lomuscio, A., Sergot, M.: Deontic interpreted systems. Studia Logica 75(1), 63–92 (2003)
Męski, A., Woźna-Szcześniak, B.z., Zbrzezny, A.M., Zbrzezny, A.: Two approaches to bounded model checking for a soft real-time epistemic computation tree logic. In: Omatu, S., Neves, J., Rodriguez, J.M.C., Paz Santana, J.F., Gonzalez, S.R. (eds.) Distrib. Computing & Artificial Intelligence. AISC, vol. 217, pp. 483–491. Springer, Heidelberg (2013)
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. Autonomous Agents and Multi-Agent Systems 28(4), 558–604 (2014)
Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003)
Raimondi, F.: Model Checking Multi-Agent Systems. PhD thesis, UCL (2006)
Wooldridge, M.: An introduction to multi-agent systems, 2nd edn. John Wiley & Sons (2009)
Woźna-Szcześniak, B.: SAT-based bounded model checking for weighted deontic interpreted systems. In: Correia, L., Reis, L.P., Cascalho, J. (eds.) EPIA 2013. LNCS, vol. 8154, pp. 444–455. Springer, Heidelberg (2013)
Woźna-Szcześniak, B., Zbrzezny, A.M., Zbrzezny, A.: SAT-based bounded model checking for weighted interpreted systems and weighted linear temporal logic. In: Boella, G., Elkind, E., Savarimuthu, B.T.R., Dignum, F., Purvis, M.K. (eds.) PRIMA 2013. LNCS, vol. 8291, pp. 355–371. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Woźna-Szcześniak, B., Szcześniak, I., Zbrzezny, A.M., Zbrzezny, A. (2014). Bounded Model Checking for Weighted Interpreted Systems and for Flat Weighted Epistemic Computation Tree Logic. In: Dam, H.K., Pitt, J., Xu, Y., Governatori, G., Ito, T. (eds) PRIMA 2014: Principles and Practice of Multi-Agent Systems. PRIMA 2014. Lecture Notes in Computer Science(), vol 8861. Springer, Cham. https://doi.org/10.1007/978-3-319-13191-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-13191-7_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-13190-0
Online ISBN: 978-3-319-13191-7
eBook Packages: Computer ScienceComputer Science (R0)