Abstract
We propose a bounded model checking (BMC) method for the verification of multi-agent systems’ (MASs). The MASs are modelled by deontic interleaved interpreted systems, and specifications are expressed in the logic \(\sc{RTECTLKD}\). The verification approach is based on the state of the art solutions to BMC, one of the mainstream approaches in verification of reactive systems. We test our results on a typical communication scenario: train controller problem with faults.
Partly supported by National Science Center under the grant No. 2011/01/B/ST6/05317.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic Reachability Analysis Based on SAT-Solvers. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 411–425. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Sistla, A.P., Emerson, E.A., Mok, A.K., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Systems 4(4), 331–352 (1992)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Jones, A., Lomuscio, A.: A BDD-based BMC approach for the verification of multi-agent systems. In: CS&P 2009, vol. 1, pp. 253–264. Warsaw University (2009)
Kacprzak, M., Lomuscio, A., Łasica, T., Penczek, W., Szreter, M.: Verifying Multi-agent Systems via Unbounded Model Checking. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A. (eds.) FAABS 2004. LNCS (LNAI), vol. 3228, pp. 189–212. Springer, Heidelberg (2004)
Lomuscio, A., Penczek, W., Qu, H.: Partial order reduction for model checking interleaved multi-agent systems. In: AAMAS 2010, pp. 659–666. IFAAMAS Press (2010)
Lomuscio, A., Sergot, M.: Deontic interpreted systems. Studia Logica 75(1), 63–92 (2003)
Męski, A., Penczek, W., Szreter, M.: Bounded model checking linear time and knowledge using decision diagrams. In: CS&P 2011, pp. 363–375. Biaystok University of Technology (2011)
Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: AAMAS 2003, pp. 209–216. ACM (2003)
Penczek, W., Woźna-Szcześniak, B., Zbrzezny, A.: Towards SAT-based BMC for LTLK over interleaved interpreted systems. In: CS&P 2011, pp. 565–576. Białystok University of Technology (2011)
Raimondi, F., Lomuscio, A.: Symbolic Model Checking of Deontic Interpreted Systems via OBDDs. In: Lomuscio, A., Nute, D. (eds.) DEON 2004. LNCS (LNAI), vol. 3065, pp. 228–242. Springer, Heidelberg (2004)
Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic 5(2), 235–251 (2005)
Wooldridge, M.: An introduction to multi-agent systems. John Wiley, England (2002)
Woźna, B., Lomuscio, A., Penczek, W.: Bounded model checking for deontic interpreted systems. In: LCMAS 2004. ENTCS, vol. 126, pp. 93–114. Elsevier (2005)
Woźna-Szcześniak, B., Zbrzezny, A., Zbrzezny, A.: The BMC Method for the Existential Part of RTCTLK and Interleaved Interpreted Systems. In: Antunes, L., Pinto, H.S. (eds.) EPIA 2011. LNCS (LNAI), vol. 7026, pp. 551–565. Springer, Heidelberg (2011)
Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1-4), 513–531 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woźna-Szcześniak, B., Zbrzezny, A. (2012). SAT-Based Bounded Model Checking for Deontic Interleaved Interpreted Systems. In: Jezic, G., Kusek, M., Nguyen, NT., Howlett, R.J., Jain, L.C. (eds) Agent and Multi-Agent Systems. Technologies and Applications. KES-AMSTA 2012. Lecture Notes in Computer Science(), vol 7327. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30947-2_54
Download citation
DOI: https://doi.org/10.1007/978-3-642-30947-2_54
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30946-5
Online ISBN: 978-3-642-30947-2
eBook Packages: Computer ScienceComputer Science (R0)