Update and Abstraction in Model Checking of Knowledge and Branching Time

Issue title: SPECIAL ISSUE ON CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P 2005) Ruciane-Nide, Poland, 28–30 September 2005

Article type: Research Article

Authors: Shilov, N.V. | Garanina, N.O. | Choe, K.-M.

Affiliations: Institute of Informatics Systems, Russian Academy of Science 6, Lavrentiev ave., 630090, Novosibirsk, Russia. E-mails: shilov@iis.nsk.su; garanina@iis.nsk.su | Korea Advanced Institute of Science and Technology 373-1 Kusong-dong Yusong-gu Taejon 305-701, Korea. E-mail: choe@cs.kaist.ac.kr

Abstract: 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.

Journal: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 347-361, 2006