Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata

• Autorzy: Belardinelli F. , Jones A. V. , Lomuscio A.
• Języki publikacji: EN

Abstrakty

EN

We introduce a novel automata-theoretic approach for the verification of multi-agent systems. We present epistemic alternating tree automata, an extension of alternating tree automata, and use them to represent specifications in the temporal-epistemic logic CTLK. We show that model checking a memory-less interpreted system against a CTLK property can be reduced to checking the language non-emptiness of the composition of two epistemic tree automata. We report on an experimental implementation and discuss preliminary results. We evaluate the effectiveness of the technique using two real-life scenarios: a gossip protocol and the train gate controller.

Słowa kluczowe

EN

multi-agent systems; temporal epistemic logic; epistemic alternating tree automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 112, nr 1
• Strony: 19--37
• Opis fizyczny: Bibliogr. 20 poz., tab.

Twórcy

autor

Belardinelli F.

autor

Jones A. V.

autor

Lomuscio A.

• Imperial College London, Exhibition Road, London SW7 2AZ, UK , UK,

Bibliografia

• [1] etav- Epistemic Tree Automata Verifier, http://vas.doc.ic.ac.uk/tools/etav/.SYMBOL!!
• [2] Blackburn, P., van Benthem, J., Wolter, F., Eds.: Handbook of Modal Logic, Elsevier, 2007.
• [3] Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A New Symbolic Model Verifier, Proc. 11th International Computer Aided Verification Conference, 1999.
• [4] Clarke, E. M., Grumberg, O., Peled, D. A.: Model Checking, The MIT Press, 1999.
• [5] Fagin, R., Halpern, J. Y., Moses, Y., Vardi, M. Y.: Reasoning About Knowledge, MIT Press, 1995.
• [6] Gammie, P., van der Meyden, R.: MCK: Model Checking the Logic of Knowledge, Proc. of the 16th Int. Conf. on Computer Aided Verification (CAV '04), 3114, Springer, 2004.
• [7] van der Hoek, W., Wooldridge, M.: Tractable Multiagent Planning for Epistemic Goals, Proc. of the 1st Int. Conf. on Autonomous Agents and Multiagent Systems (AAMAS '02), 2002.
• [8] Holzmann, G. J.: SPIN Model Checker, The: Primer and Reference Manual, AddisonWesley, 2003.
• [9] Huang, X., Luo, C., van der Meyden, R.: Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic, Proc. of the 6th Workshop on Model Checking and Artificial Intelligence (MoChArt '10), 2010.
• [10] Jelasity, M., Voulgaris, S., Guerraoui, R., Kermarrec, A., van Steen, M.: Gossip-based Peer Sampling, ACM Trans. Comput. Syst., 25(3), 2007.
• [11] Jones, A. V., Lomuscio, A.: Distributed BDD-based BMC for the Verification ofMulti-Agent Systems, Proc.of the 9th Int. Conf. on Autonomous Agents and Multiagent Systems (AAMAS '10), 2010.
• [12] Kupferman, O., Vardi, M. Y., Wolper, P.: An Automata-Theoretic Approach to Branching-Time Model Checking, J. ACM, 47(2), 2000, 312-360.
• [13] Lomuscio, A., Penczek, W., Qu, H.: Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems, Proc. of the 9th Int. Conf. on Autonomous Agents and Multiagent Systems (AAMAS '10), 2010.
• [14] Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A Model Checker for the Verification of Multi-Agent Systems, Proc. of the 21st Int. Conf. on Computer Aided Verification (CAV '09), 5643, Springer, 2009.
• [15] Lomuscio, A., Raimondi, F.: The Complexity of Model Checking Concurrent ProgramsAgainst CTLK Specifications, Proc. of 4th International Workshop on Declarative Agent Languages and Technologies (DALT 2006), 4327, Springer, 2006.
• [16] Meyer, J.-J. C., van der Hoek, W.: Epistemic Logic for AI and Computer Science, Cambridge University Press, 1995.
• [17] Muller, D., Saoudi, A., Schupp, P.: Alternating Automata. The Weak Monadic Theory of the Tree, and its Complexity, ICALP, 226, Springer, 1986.
• [18] Muller, D., Schupp, P.: Alternating Automata on Infinite Trees, Theoretical Computer Science, 54, 1987, 267-276.
• [19] Qian, K., Nymeyer, A.: Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis, ETCS, 149(2), 2006, 33-49.
• [20] Vardi, M. Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification, Proc. 1st Symp. on Logic in Computer Science, Cambridge, June 1986.