Well-Structured Model Checking of Multiagent Systems

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 d already an (update+abstraction)-algorithm for model checking with detailed time upper bound. This algorithm reduces model checkombined logic to model checking of CTL in a finite abstract space (that consists of some finite trees). Unfortunately, the known upd 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 . 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 pr...

• Type: Conference
• Year: 2006
• Where: ERSHOV
• Authors: Nikolay V. Shilov, Natalya Olegovna Garanina
• Keywords: Abstract Space, ERSHOV 2006, Model Checking, Model Checking Problem, Theoretical Computer Science