Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems
Daniel Stan, Technische Universität Kaiserslautern
We present a framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In this 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. As in other regular model checking (RMC) techniques, a finite-state automaton is used to specify a parameterized family of systems.
Parameterized systems might also require an arbitrary number of announcements, leading to the introduction of the so-called iterated public announcement. Although model checking becomes undecidable because of this operator, we provide a semi-decision procedure based on Angluin's L*-algorithm for learning finite automata. Moreover, the procedure is guaranteed to terminate when some regularity properties are met. We illustrate the approach on the Muddy Children puzzle, and we further discuss dynamic protocol encodings through the Dining Cryptographer example.
Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomas
Since October 2019, Daniel Stan is a PostDoc in the Automated Reasoning group.
He was previously a PhD student (2013-2017) at LSV, ENS Paris Saclay under the
supervision of Patricia Bouyer and Nicolas Markey, then a PostDoc in the
Dependable Systems and Software chair of Saarbrücken. His research interests
include formal methods and model checking techniques with a particular focus on
Regular Model Checking and Automatic Structures, Parameterized Systems,
Stochastic Systems and Games. In particular, his current work put an emphasis on
exact learning algorithms with applications to model checking.