×

zbMATH — the first resource for mathematics

Automatic data-abstraction in model checking multi-agent systems. (English) Zbl 1327.68162
van der Meyden, Ron (ed.) et al., Model checking and artificial intelligence. 6th international workshop, MoChArt 2010, Atlanta, GA, USA, July 11, 2010. Revised selected and invited papers. Berlin: Springer (ISBN 978-3-642-20673-3/pbk). Lecture Notes in Computer Science 6572. Lecture Notes in Artificial Intelligence, 52-68 (2011).
Summary: We present an automatic data-abstraction technique for the verification of the universal fragment of the temporal-epistemic logic CTLK. We show the correctness of the methodology and present an implementation operating on ISPL models, the input files for MCMAS, a model checker for multi-agent systems. The experimental results point to the attractiveness of the technique in a number of examples in the multi-agent systems domain.
For the entire collection see [Zbl 1214.68023].
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68T42 Agent technology and artificial intelligence
Software:
CUDD; MCK; MCMAS; VerICS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000) · Zbl 0974.68517 · doi:10.1007/10722167_15
[2] Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994) · doi:10.1145/186025.186051
[3] Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
[4] Cohen, M., Dam, M., Lomuscio, A., Qu, H.: A data symmetry reduction technique for temporal-epistemic logic. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 69–83. Springer, Heidelberg (2009) · Zbl 1262.68110 · doi:10.1007/978-3-642-04761-9_6
[5] Cohen, M., Dam, M., Lomuscio, A., Russo, F.: Abstraction in model checking multi-agent systems. In: AAMAS 2009 (2009)
[6] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977) · doi:10.1145/512950.512973
[7] Dechesne, F., Orzan, S., Wang, Y.: Refinement of kripke models for dynamics. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 111–125. Springer, Heidelberg (2008) · Zbl 1161.68616 · doi:10.1007/978-3-540-85762-4_8
[8] Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982) · Zbl 0514.68032 · doi:10.1016/0167-6423(83)90017-5
[9] van Ditmarsch, H., van der Hoek, W., van der Meyden, R., Ruan, J.: Model Checking Russian Cards. Electr. Notes Theor. Comput. Sci. 149(2), 105–123 (2006) · Zbl 1273.68245 · doi:10.1016/j.entcs.2005.07.029
[10] Enea, C., Dima, C.: Abstractions of multi-agent systems. In: Burkhard, H., Lindemann, G., Verbrugge, R., Varga, L.Z. (eds.) CEEMAS 2007. LNCS (LNAI), vol. 4696, pp. 11–21. Springer, Heidelberg (2007) · Zbl 1151.68652 · doi:10.1007/978-3-540-75254-7_2
[11] Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995) · Zbl 0839.68095
[12] 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) · Zbl 1103.68614 · doi:10.1007/978-3-540-27813-9_41
[13] Graf, S., Saïdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997) · doi:10.1007/3-540-63166-6_10
[14] Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M., Wozna, B., Zbrzezny, A.: Verics 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1-4), 313–328 (2008) · Zbl 1167.68381
[15] 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) · Zbl 05571936 · doi:10.1007/978-3-642-02658-4_55
[16] Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003) · Zbl 1111.68512
[17] Wooldridge, M.: Computationally grounded theories of agency. In: Durfee, E. (ed.) ICMAS, pp. 13–22. IEEE Press, Los Alamitos (2000)
[18] Wooldridge, M.: An introduction to MultiAgent systems, 2nd edn. Wiley, Chichester (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.