Abstract
We address model checking problem for combination of Computation Tree Logic (CTL) and Propositional Logic of Knowledge (PLK) in finite systems with the perfect recall synchronous semantics. We have published already an (update+abstraction)-algorithm for model checking with detailed time upper bound. This algorithm reduces model checking of combined logic to model checking of CTL in a finite abstract space (that consists of some finite trees). Unfortunately, the known upper bound for size of the abstract space (i.e. number of trees) is a non-elementary function of the size of the background system. Thus a straightforward use of a model checker for CTL for model checking the combined logic seems to be infeasible. Hence it makes sense to try to apply techniques, which have been developed for infinite-state model checking. In the present paper we demonstrate that the abstract space provided with some partial order on trees is a well-structured labeled transition system where every property expressible in the propositional μ-Calculus, can be characterized by a finite computable set of maximal elements. We tried feasibility of this approach to model checking of the combined logic in perfect recall synchronous environment by automatic model checking a parameterized example.
Supported by joint grant RFBR 05-01-04003-a (DFG project COMO, GZ: 436 RUS 113/829/0-1) and by grant RFBR 06-01-00464-a.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., et al.: Algorithmic analysis of programs with well quasi-ordered domains. Algorithmic analysis of programs with well quasi-ordered domains 160(1-2), 109–127 (2000)
Arnold, A., Niwinski, D.: Rudiments of μ-calculus. North-Holland, Amsterdam (2001)
Bull, R.A., Segerberg, K.: Basic Modal Logic. In: Handbook of Philosophical Logic, vol. II, 2nd edn., pp. 1–88. Kluwer Academic Publishers, Dordrecht (1994)
Burch, J.R., et al.: Symbolic Model Checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dixon, C., et al.: Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols. In: Proceedings of TIME 2004, Tatihou, Normandie, France, 1-3 July 2004, IEEE Computer Society Press, Los Alamitos (2004)
Dixon, C., Nalon, C., Fisher, M.: Tableau for Logics of Time and Knowledge with Interactions Relating to Synchrony. Journal of Applied Non-Classical Logics 14(4), 397–445 (2004)
Emerson, E.A.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)
Fagin, R., et al.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comp. Sci. 256(1-2), 63–92 (2001)
Gammie, P., van der Meyden, R.M.: Model Checking the Logic of Knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)
Garanina, N.O.: Verification of Distributed Systems on base of Affine Data representation and Logics of Knowledge and Actions (in Russian). Ph.D Thesis, A.P. Ershov Institute of Informatics Systems (2004)
Garanina, N.O., Kalinina, N.A., Shilov, N.V.: Model checking knowledge, actions and fixpoints. In: Proc. of Concurrency, Specification and Programming Workshop CS&P’2004, Germany. Humboldt Universitat, Berlin, Informatik-Bericht 170(2), 351-357 (2004)
Halpern, J.Y., van der Meyden, R., Vardi, M.Y.: Complete Axiomatizations for Reasoning about Knowledge and Time. SIAM Journal on Computing 33(3), 674–703 (2004)
van der Hoek, W., Wooldridge, M.J.: Model Checking Knowledge and Time. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 95–111. Springer, Heidelberg (2002)
Kacprzak, M., Lomuscio, A., Penczek, W.: Unbounded Model Checking for Knowledge and Time. In: Proceedings of the CS&P’2003 Workshop, vol. 1, pp. 251–264. Warsaw University (2003)
Kacprzak, M., Penczek, W.: Model Checking for Alternating-Time mu-Calculus via Translation to SAT. In: Proc. of Concurrency, Specification and Programming Workshop CS&P’2004, Germany. Humboldt Universitat, Berlin, Informatik-Bericht 170(2) (2004)
Kozen, D.: Results on the Propositional Mu-Calculus. Theoretical Computer Science 27(3), 333–354 (1983)
Kouzmin, E.V., Shilov, N.V., Sokolov, V.A.: Model Checking μ-Calculau in Well-Structured Transition Systems. In: Proceedings of 11th International Symposium on Temporal Representation and Reasoning (TIME 2004), France, pp. 152–155. IEEE Computer Society Press, Los Alamitos (2004)
Kozen, D., Tiuryn, J.: Logics of Programs. In: Handbook of Theoretical Computer Science, vol. B, pp. 789–840. Elsevier, Amsterdam (1990)
van der Meyden, R.: Common Knowledge and Update in Finite Environments. Information and Computation 140(2), 115–157 (1998)
van der Meyden, R., Shilov, N.V.: Model Checking Knowledge and Time in Systems with Perfect Recall. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999)
van der Meyden, R., Wong, K.: Complete Axiomatizations for Reasoning about Knowledge and Branching Time. Studia Logica 75(1), 93–123 (2003)
Rescher, N.: Epistemic Logic. A Survey of the Logic of Knowledge. University of Pittsburgh Press, Pittsburgh (2005)
Shilov, N.V., Yi, K.: How to find a coin: propositional program logics made easy. In: Current Trends in Theoretical Computer Science, vol. 2, pp. 181–213. World Scientific, Singapore (2004)
Shilov, N.V., Garanina, N.O., Choe, K.-M.: Update and Abstraction in Model Checking of Knowledge and Branching Time. Fundameta Informaticae 72(1-3), 347–361 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shilov, N.V., Garanina, N.O. (2007). Well-Structured Model Checking of Multiagent Systems. In: Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2006. Lecture Notes in Computer Science, vol 4378. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70881-0_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-70881-0_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70880-3
Online ISBN: 978-3-540-70881-0
eBook Packages: Computer ScienceComputer Science (R0)