Well-Structured Model Checking of Multiagent Systems

摘要

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.