Sciweavers

ERSHOV
2006
Springer

Well-Structured Model Checking of Multiagent Systems

13 years 4 months ago
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...
Nikolay V. Shilov, Natalya Olegovna Garanina
Added 14 Oct 2010
Updated 14 Oct 2010
Type Conference
Year 2006
Where ERSHOV
Authors Nikolay V. Shilov, Natalya Olegovna Garanina
Comments (0)