Mercredi 22 juin 2022, 11h - 12h, Https:// \& Salle KB000

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.