Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems

• Autorzy: Lomuscio, A. , Penczek, W. , Qu, H.
• Języki publikacji: EN

Abstrakty

EN

We investigate partial order reduction techniques for the verification of multi-agent systems. We investigate the case of interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed in the system. We present a notion of stuttering-equivalence and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing implementations and the experimental results obtained against well-known examples in the MAS literature.

Słowa kluczowe

EN

semantics; behavioural equivalence; model checking

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 101, nr 1/2
• Strony: 71-90
• Opis fizyczny: Bibliogr. 34 poz., tab.

Twórcy

autor

Lomuscio, A.

autor

Penczek, W.

autor

Qu, H.

• Department of Computing, Imperial College London, 180 Queen’s Gate London SW7 2AZ, UK,

Bibliografia

• [1] R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. MOCHA: User Manual. In cMocha (Version 1.0.1) Documentation, 1998. http://mtc.epfl.ch/software-tools/mocha/doc/c-doc/
• [2] J. Archibald and J.-l. Baer. Cache coherence protocols: Evaluation using a multiprocessor simulation model. ACM Transactions on Computer Systems, 4:273-298, 1986.
• [3] K. Baukus and R. van der Meyden. A Knowledge Based Analysis of Cache Coherence. In Proceedings of 6th International Conference on Formal Engineering Methods (ICFEM'04), LNCS 3308, pages 99-114, Springer-Verlag, 2004.
• [4] R. Bordini, M. Fisher, C. Pardavila, W. Visser, and M. Wooldridge. Model checking multi-agent programs with CASP. In CAV'03, LNCS 2725, pages 110-113. Springer-Verlag, 2003.
• [5] D. Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology, 1(1), pages 65-75, 1988.
• [6] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
• [7] C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1(2/3), pages 275-288, 1992.
• [8] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, 1995.
• [9] P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In Proceedings of 16th International Conference on Computer Aided Verification (CAV'04), LNCS 3114, pages 479-483. Springer-Verlag, 2004.
• [10] R. Gerth, R. Kuiper, D. Peled, and W. Penczek. A partial order approach to branching time logic model checking. Information and Computation, 150, pages 132-152, 1999.
• [11] P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke and R. P. Kurshan, editors, Proceedings of the 2nd International Conference on Computer Aided Verification (CAV'90), volume 3 of ACM/AMS DIMACS Series, pages 321-340, 1991.
• [12] J. Halpern, R. Meyden, and M. Y. Vardi. Complete axiomatisations for reasoning about knowledge and time. SIAM Journal on Computing, 33(3), pages 674-703, 2003.
• [13] J. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3), pages 549-587, 1990.
• [14] W. van der Hoek, M. Roberts, and M. Wooldridge. Knowledge and social laws. In Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems (AAMAS'05), pages 674-681. ACM, 2005.
• [15] W. van der Hoek and M. Wooldridge. Model checking knowledge and time. In SPIN 2002 - Proceedings of the Ninth International SPIN Workshop on Model Checking of Software, Grenoble, France, Apr. 2002.
• [16] W. van der Hoek and M.Wooldridge. Tractable Multiagent Planning for Epistemic Goals. In Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS'02), pages 1167-1174. ACM, 2002.
• [17] G. Holzmann and D. Peled. Partial order reduction of the state space. In First SPIN Workshop, Montréal, Quebec, 1995.
• [18] G. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In Second SPIN Workshop, pages 23-32. AMS, 1996.
• [19] M. Kacprzak, W. Nabialek, A. Niewiadomski, W. Penczek, A. Polrola, M. Szreter, B. Wozna, and A. Zbrzezny. VerICS 2007 - aModel Checker for Knowledge and Real-Time. Fundamenta Informaticae 85(1-4), pages 313-328, 2008.
• [20] M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek, F. Raimondi, and M. Szreter. Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol. Fundamenta Informaticae, 63(2-3), pages 221-240, 2006.
• [21] M. E. Kurb´an, P. Niebert, H. Qu, and W. Vogler. Stronger reduction criteria for local first search. In ICTAC, LNCS 4281, pages 108-122. Springer-Verlag, 2006.
• [22] A. Lomuscio,W. Penczek, and H. Qu. Towards partial order reduction formodel checking temporal epistemic logic. In MoChArt, LNAI 5348, pages 106-121. Springer-Verlag, 2009.
• [23] A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: Amodel checker for the verification of multi-agent systems. In Proceedings of CAV 2009, LNCS 5643, pages 682-688. Springer-Verlag, 2009.
• [24] R. van der Meyden and K. Su. Symbolic model checking the knowledge of the dining cryptographers. In Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), pages 280-291, Washington, DC, USA, 2004. IEEE Computer Society.
• [25] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [26] K. L. McMillan. A technique of a state space search based on unfolding. Formal Methods in System Design, 6(1), pages 45-65, 1995.
• [27] R. Parikh and R. Ramanujam. Distributed processes and the logic of knowledge. In Logic of Programs, LNCS 193, pages 256-268. Springer-Verlag, 1985.
• [28] D. Peled. All from one, one for all: On model checking using representatives. In Proceedings of the 5th International Conference on Computer Aided Verification (CAV'93), volume 697 of LNCS, pages 409-423. Springer-Verlag, 1993.
• [29] D. Peled. Combining partial order reductions with on-the-fly model-checking. In Proceedings of the 6th International Conference on Computer Aided Verification (CAV'94), volume 818 of LNCS, pages 377-390. Springer-Verlag, 1994.
• [30] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2), pages 167-185, 2003.
• [31] W. Penczek, M. Szreter, R. Gerth, and R. Kuiper. Improving Partial Order Reductions for Universal Branching Time Properties. Fundamenta Informaticae, 43(1-4), pages 245-267, 2000.
• [32] F. Raimondi and A. Lomuscio. Automatic verification ofmulti-agent systems by model checking via OBDDs. Journal of Applied Logic, 5(2):235-251, 2007.
• [33] S. Rosenschein. Formal theories of ai in knowledge and robotics. New Generation Computing, 3:345-357, 1985.
• [34] A. Valmari. A stubborn attack on state explosion. In Proceedings of the 2nd International Conference on Computer Aided Verification (CAV'90), volume 531 of LNCS, pages 156-165. Springer-Verlag, 1990.