Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Fundamenta Informaticae

1 2006

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Update and Abstraction in Model Checking of Knowledge and Branching Time

Shilov N.V., Garanina N.O., Choe K.M.

Fundamenta Informaticae

2006

Vol. 72, nr 1-3

347-361

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