Update and Abstraction in Model Checking of Knowledge and Branching Time

• Autorzy: Shilov N.V. , Garanina N.O. , Choe K.M.
• Języki publikacji: EN

Abstrakty

EN

We present (update+abstraction) algorithm for model checking a fusion of Computation Tree Logic and Propositional Logic of Knowledge in systems with the perfect recall synchronous semantics. It has been already known that the problem is decidable with a non-elementary lower bound. The decidability follows from interpretation of the problem in a so-called Chain Logic and then in the Second Order Logic of Monadic Successors. This time we give a direct algorithm for model checking and detailed time upper bound where a number of different parameters are taken into count (i.e. a number of agents, a number of states, knowledge depth, formula size). We present a toy experiment with this algorithm that encourages our hope that the algorithm can be used in practice

Słowa kluczowe

EN

model checking; algorithm

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 72, nr 1-3
• Strony: 347--361
• Opis fizyczny: bibliogr. 29 poz.

Twórcy

autor

Shilov N.V.

autor

Garanina N.O.

autor

Choe K.M.

• Institute of Informatics Systems, Siberian Division of the Russian Academy of Sciences, 6, Acad. Lavrentiev avenue, 630090, Novosibirsk, Russia,

Bibliografia

• [1] Abdulla P.A., Cêrâns K., Jonsson B., and Tsay Yih-Kuen. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, v.160(1-2), 2000, p.109-127.
• [2] Börger E., Gr¨adel E., Gurevich Yu. The Classical Decision Problem. Springer Verlag, 1997.
• [3] Büchi J.R. On a decision method in restricted second order arithmetic. Proc. Intern. Congr. on Logic, Methodology and Philosophy of Science. Stanford Univ. Press, Stanford, 1960, p. 1-11.
• [4] Bull R.A., Segerberg K. Basic Modal Logic. In: Handbook of Philosophical Logic. Vol.II. Reidel Publishing Company, 1984 (1-st ed.), Kluwer Academic Publishers, 1994 (2-nd ed.). p. 1-88.
• [5] Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J. Symbolic Model Checking: 1020 states and beyond. Information and Computation, 1992. v.98(2), p. 142-170.
• [6] Clarke E.M., Grumberg O., Peled D. Model Checking. MIT Press, 1999.
• [7] Dixon C., Fernandez Gago M-C., Fisher M., and van der HoekW. Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols. In: Proceedings of TIME 2004, 1st-3rd July 2004, Tatihou, Normandie, France. IEEE, p.148-151.
• [8] Dixon C., Nalon C. and Fisher M. Tableau for Logics of Time and Knowledge with Interactions Relating to Synchrony, Journal of Applied Non-Classical Logics, v.14, n.4, p.397-445, 2004.
• [9] Emerson E.A. Temporal and Modal Logic. In: Handbook of Theoretical Computer Science. v.B, Elsevier and MIT Press, 1990, p. 995-1072.
• [10] Fagin R., Halpern J.Y., Moses Y., Vardi M.Y. Reasoning about Knowledge. MIT Press, 1995.
• [11] Finkel A., Schnoebelen Ph. Well-structured transition systems everywhere! Theor. Comp. Sci., v.256(1-2), 2001, p.63-92.
• [12] Gammie P. and van der Meyden R. MCK: Model Checking the Logic of Knowledge. Springer-Verlag Lect. Notes Comp. Sci., v.3114, 2004, p.479-483.
• [13] Garanina N.O. Verification of Distributed Systems on base of Affine Data representation and Logics of Knowledge and Actions. Ph.D Thesis, A.P. Ershov Institute of Informatics Systems, 2004 (in Russian).
• [14] Garanina N.O., Kalinina N.A. and Shilov N.V. Model checking knowledge, actions and fixpoints. Proc. Of Concurrency, Specification and ProgrammingWorkshop CS&P'2004, Germany, 2004, Humboldt Universitat, Berlin, Informatik-Bericht Nr.170, v.2, p.351-357.
• [15] Halpern J. Y., van der Meyden R., and Vardi M. Y. Complete Axiomatizations for Reasoning about Knowledge and Time. SIAM Journal on Computing, v.33(3), 2004, p. 674-703.
• [16] van der Hoek W. and Wooldridge M.J. Model Checking Knowledge and Time. Lecture Notes in Computer Science, v.2318, p.95-111, 2002.
• [17] Kacprzak M., Lomuscio A., Penczek W. Unbounded Model Checking for Knowledge and Time. Proceedings of the CS&P'2003Workshop,Warsaw University, v.1, p.251-264.
• [18] Kacprzak M., PenczekW. Model Checking for Alternating-Time mu-Calculus via Translation to SAT. Proc. of Concurrency, Specification and Programming Workshop CS&P'2004, Germany, 2004, Humboldt Universitat, Berlin, Informatik-Bericht Nr.170, v.2, p. 286-297.
• [19] Kozen D., Tiuryn J. Logics of Programs. In: Handbook of Theoretical Computer Science, v.B., Elsevier and MIT Press, 1990, p. 789-840.
• [20] Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking 􀀀 -Calculau in Well-Structured Transition Systems. Proceedings of 11th International Symposium on Temporal Representation and Reasoning (TIME 2004), France 2004, IEEE Press, p. 152-155.
• [21] van der Meyden R. Common Knowledge and Update in Finite Environments. Information and Computation, 1998, v.140(2), p. 115-157.
• [22] van der Meyden R., Shilov N.V. Model Checking Knowledge and Time in Systems with Perfect Recall. Springer-Verlag Lect. Notes Comput. Sci., 1999, v.1738, p. 432-445.
• [23] van der Meyden R. andWong K. Complete Axiomatizations for Reasoning about Knowledge and Branching Time. Studia Logica, v.75(1), 2003, p. 93-123.
• [24] Meyer A.R. The inherent complexity of theories of ordered sets. Proc. of the Intern. Congress of Math. Vol.2.-Canadian Mathematical Congress, Vancouver, 1974, p. 477-482.
• [25] Rabin M.O. Decidability of second order theories and automata on infinite trees. Trans. Amer. Math. Soc., 1969, v.141, p. 1-35.
• [26] Rabin M.O. Decidable Theories. In: Handbook of Mathematical Logic. North-Holland Pub. Co., 1977, p. 595-630.
• [27] Rescher N. Epistemic Logic. A Survey of the Logic of Knowledge. University of Pitsburgh Press, 2005.
• [28] Shilov N.V. and Yi K. How to find a coin: propositional program logics made easy. In: Current Trends in Theoretical Computer Science,World Scientific, v. 2, 2004, p.181-213.
• [29] ThomasW. Infinite trees and automaton-definable relations over ω-words. Theor. Comput. Sci., 1992, v.103, p. 143-159.