VerICS 2007 - a Model Checker for Knowledge and Real-Time

• Autorzy: Kacprzak M. , Nabiałek W. , Niewiadomski A. , Penczek W. , Półrola A. , Szreter M. , Woźna B. , Zbrzezny A.
• Języki publikacji: EN

Abstrakty

EN

The papers presents the current stage of the development of VerICS - a model checker for real-time and multi-agent systems. Depending on the type of a system considered, it enables to test various classes of properties - from reachability to temporal, epistemic and deontic formulas. The model checking methods used to this aim include both SAT-based and enumerative ones. In the paper we focus on new features of the verifier: SAT-based model checking for multi-agent systems and several extensions and improvements to real-time systems' verification.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 313--328
• Opis fizyczny: bibliogr. 27 poz., rys., tab.

Twórcy

autor

Kacprzak M.

autor

Nabiałek W.

autor

Niewiadomski A.

autor

Penczek W.

autor

Półrola A.

autor

Szreter M.

autor

Woźna B.

autor

Zbrzezny A.

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

Bibliografia

• [1] R. Bordini, M. Fisher, C. Pardavila, W. Visser, and M. Wooldridge. Model checking multi-agent programs with CASP. In Proc. of the 15th Int. Conf. on Computer Aided Verification (CAV'03), volume 2725 of LNCS, pages 110-113. Springer-Verlag, 2003.
• [2] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [3] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerICS: A tool for verifying timed automata and Estelle specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [4] E. A. Emerson and E. 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 169-181. Springer-Verlag, 1980.
• [5] R. Fagin, J. Y. Halpern, Y. Moses, and M. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [6] P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In Proc. of the 16th Int. Conf. on Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 479-483. Springer-Verlag, 2004.
• [7] ISO/IEC 9074(E), Estelle - a formal description technique based on an extended state-transition model. International Standards Organization, 1997.
• [8] M. Kacprzak, A. Lomuscio, T. Łasica, W. Penczek, and M. Szreter. Verifying multiagent systems via unboundedmodel checking. In Proc. of the 3rd NASAWorkshop on Formal Approaches to Agent-Based Systems (FAABS III), volume 3228 of LNCS, pages 189-212. Springer-Verlag, 2005.
• [9] 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, 72(1-2):215-234, 2006.
• [10] M. Kacprzak, A. Lomuscio, and W. Penczek. From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae, 63(2-3):221-240, 2004.
• [11] A. Lomuscio, C. Pecheur, and F. Raimondi. Automatic verification of knowledge and time with NuSMV. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI'07), pages 1384-1389, 2007.
• [12] A. Lomuscio, W. Penczek, and B. Woźna. Bounded model checking for knowledge and real time. Artificial Intelligence, 171:1011-1038, 2007.
• [13] A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In Proc. of the 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), volume 3920 of LNCS, pages 450-454. Springer-Verlag, 2006.
• [14] A. Lomuscio, B. Woźna, and A. Zbrzezny. Bounded model checking real-time multi-agent systems with clock differences: Theory and implementation. In Proc. of the 4th Int. Workshop on Model Checking and Artificial Intelligence (MoChArt'06), pages 62-78. ECCAI, 2006.
• [15] 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.
• [16] MiniSat. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat, 2006.
• [17] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. In Proc. of the 2nd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'03), pages 209-216. ACM, 2003.
• [18] W. Penczek and A. Półrola. Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach, volume 20 of Studies in Computational Intelligence. Springer-Verlag, 2006.
• [19] RSat. http://reasoning.cs.ucla.edu/rsat, 2006.
• [20] M. Szreter. SAT-Based Model Checking of Distributed Systems. PhD thesis, ICS PAS, January 2007.
• [21] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955.
• [22] M. Wooldridge, M. Fisher, M. P. Huget, and S. Parsons. Model checking multiagent systems with MABLE. In Proc. of the 1st Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'02), volume II, pages 952-959. ACM, 2002.
• [23] B.Woźna, A. Lomuscio, and W. Penczek. Bounded model checking for deontic interpreted systems. In Proc.of the 2nd Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'04), volume 126 of ENTCS, pages 93-114. Elsevier, 2005.
• [24] B. Woźna, A. Lomuscio, and W. Penczek. Bounded model checking for knowledge and real time. In Proc. of the 4th Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'05), pages 165-172. ACM, 2005.
• [25] A. Zbrzezny. Improvements in SAT-based reachability analysis for timed automata. Fundamenta Informaticae, 60(1-4):417-434, 2004.
• [26] A. Zbrzezny. SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae, 67(1-3):303-322, 2005.
• [27] L. Zhang. Zchaff. http://www.ee.princeton.edu/_chaff/zchaff.php, 2001.