Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems

摘要: We present a general framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In our framework, the number of agents or amount certain resources are (i.e. not known priori), corresponding verification problem asks whether given property is true regardless instantiation parameters. For example, in muddy children puzzle, one could ask each child will eventually find out (s)he muddy, children. Our regular model checking (RMC)-based, wherein synchronous finite-state automata (equivalently, monadic second-order logic words) used to specify systems. propose an extension announcement as specification language. Of special interests addition so-called iterated operators, which crucial reasoning about knowledge Although operators make undecidable, we show this becomes decidable when appropriate "disappearance relation" given. Further, how Angluin's L*-algorithm learning finite can be applied disappearance relation, guaranteed terminate if it regular. have implemented algorithm apply such examples Muddy Children Puzzle, Russian Card Problem, Large Number Challenge.