Unbounded Model Checking for Knowledge and Time

• Autorzy: Kacprzak M. , Lomuscio A. , Penczek W.
• Języki publikacji: EN

Abstrakty

EN

We present an approach to the problem of verification of epistemic properties in multi-agent systems by means of symbolic model checking. In particular, it isshown how to extend the technique of unbounded model checking from a purely temporal setting to a temporal-epistemic one. In order to achieve this, we baseour discussion on interpreted systems semantics, a popular semantics used in multi-agent systems literature. We give details of the technique and show howit can be applied to the well known train, gate and controller problem.

PL

Nieograniczona weryfikacja modelowa dla systemów z wiedzą i czasem. Praca dotyczy problemu weryfikacji epistemicznych własności systemów wieloagentowych za pomocą symbolicznej weryfikacji modelowej. Pokazujemy jak poszerzyć technikę zwaną nieograniczoną weryfikacją modelową stosowaną do badania temporalnych własności systemów tak, aby można było ją wykorzystać również do analizowania epistemicznych własności. W tym celu bazujemy na interpretowanych systemach - popularnej semantyce szeroko opisywanej w literaturze dotyczącej systemów wieloagentowych. Podajemy szczegóły techniki oraz demonstrujemy zastosowanie jej do znanego problemu kontroli przejazdów kolejowych.

Słowa kluczowe

EN

model checking; unbounded model checking; multi-agent system

PL

nieograniczona weryfikacja modelowa; weryfikacja modelowa

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2003
• Tom: Nr 966
• Strony: 1--27

Twórcy

autor

Kacprzak M.

• Institute of Mathematics and Physics, Białystok University of Technology, Wiejska 45A, 15-351 Białystok, Poland

autor

Lomuscio A.

• Department of Computer Science King’s College London London WC2R 2LS, United Kingdom

autor

Penczek W.

• Institute of Computer Science, PAS Ordona 21 01-237 Warsaw, Poland

Bibliografia

• [BCCZ99] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.
• [BdRV0l] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
• [CGP99] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
• [DLL62] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7):394-397, 1962.
• [EC80] E. A. Emerson and E. M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Proc. of the 7th Int. Colloquium on Automata, Languages and Programming (ICALP’80), volume 85 of LNCS, pages 1G9-1S1. Springer-Verlag, 1980.
• [EC82] E. A. Emerson and E. M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982.
• [FHMV95a] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [[FHMV95b] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [HV91] J. Halpern and M. Vardi. Model checking vs. theorem proving: a manifesto, pages 151-176. Artificial Intelligence and Mathematical Theory of Computation. Academic Press. Inc, 1991.
• [[LŁP03] A. Lomuscio, T. Lasica, and W. Penczek. Bounded model checking for interpreted systems: Preliminary experimental results. In Proc. of the 2nd NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS’02), volume 2699 of LNAI, pages 115-125. Springer-Verlag, 2003.
• [McM02] K. L. McMillan. Applying SAT methods in unbounded symbolic model checking. In Proc. of the 14th Int. Conf. on Computer- Aided Verification (CAV’02), volume 2404 of LNCS, pages 250- 264. Springer-Verlag, 2002.
• [MS99] R. van der Meyden and H. Shilov. Model checking knowledge and time in systems with perfect recall. In Proceedings of Proc. of FST&TCS, volume 1738 of Lecture Notes in Computer Science, pages 432-445, Hyderabad, India, 1999.
• [PL03] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167-185, 2003.
• [RL03] F. Raimondi and A. Lomuscio. A tool for specification and verification of epistemic and temporal properties of multi-agent system. Electronic Lecture Notes in Theoretical Computer Science, 2003. To appear.
• [Tar55] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955.
• [vdHW02a] W. van der Hoek and M. Wooldridge. Model checking knowledge and time. In Proc. of the 9th Int. SPIN Workshop (SPIN’02), volume 2318 of LNCS, pages 95-111. Springer-Verlag, 2002.
• [vdHW02b] W. van der Hoek and M. Wooldridge. Tractable multiagent planning for epistemic goals. In Proc. of the 1st Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS’02), volume III, pages 1167-1174. ACM, July 2002.
• [WFHP02] M. Wooldridge, M. Fisher, M. Huget, and S. Parsons. Model checking multiagent systems with mable. In Proceedings of the First International Conference on Autonomous Agents and Multiagent Systems (AAMAS-2), Bologna, Italy, July 2002.
• [Woo00] M. Wooldridge. Computationally grounded theories of agency. In E. Durfce, editor, Proceedings of ICMAS, International Conference of Multi-Agent Systems. IEEE Press, 2000.
• [Woo02] M. Wooldridge. An introduction to multi-agent systems. John Wiley, England, 2002.