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 the amount of certain resources are parameterized (i.e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. For example, in a muddy children puzzle, one could ask whether each child will eventually find out whether (s)he is muddy, regardless of the number of children.
Our framework is regular model checking (RMC)-based, wherein synchronous finite-state automata (equivalently, monadic second-order logic over words) are used to specify the systems. We propose an extension of public announcement logic as specification language. Of special interests is the addition of the so-called iterated public announcement operators, which are crucial for reasoning about knowledge in parameterized systems. Although the operators make the model checking problem undecidable, we show that this becomes decidable when an appropriate "disappearance relation" is given. Further, we show how Angluin's L*-algorithm for learning finite automata can be applied to find a disappearance relation, which is guaranteed to terminate if it is regular. We have implemented the algorithm and apply this to such examples as the Muddy Children Puzzle, the Russian Card Problem, and Large Number Challenge.
Kofola 1.0: A Modular Approach to ω-Regular Complementation and Inclusion Checking (Technical Report)
Brno University of Technology（布尔诺理工大学）；Aalborg University（奥尔堡大学）；Key Lab. of System Software (Chinese Academy of Sciences), ISCAS（中国科学院系统软件重点实验室）；Slovak University of Technology in Bratislava（布拉迪斯拉发斯洛伐克科技大学）
Parameterized Verification of Quantum Circuits (Technical Report)
Uppsala University（乌普萨拉大学）；Mälardalen University（马拉尔登大学）；Brno University of Technology（布尔诺理工大学）；Aalborg University（奥尔堡大学）；National Taipei University of Technology（台北科技大学）
Parameterized Verification of Timed Networks with Clock Invariants
Université Sorbonne Paris Nord, LIPN, CNRS UMR 7030（索邦巴黎北大学，LIPN，CNRS UMR 7030）；Institut universitaire de France (IUF)（法国高等研究院）；CISPA Helmholtz Center for Information Security（CISPA赫尔霍兹信息安全中心）；Université de Rennes, CNRS, Inria, Rennes（雷恩大学，CNRS，Inria）
