Seminar/2022-06-22

Mercredi 22 juin 2022, 11h - 12h, Https://meet.jit.si/SeminaireLRDE \& Salle KB000

Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems

Daniel Stan, Universität des Saarlandes

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

Daniel Stan has been a postdoctoral researcher at the chair of Prof. Dr.-Ing. Holger Hermanns since May 2017. Before that, he got his Ph.D at ENS Cachan/Paris Saclay, whose title is “Randomized Strategies in Concurrent Games”, and that he defended in March 2017. His research includes quantitative verification techniques, parametric stochastic systems, game theoretical approaches. He is more recently considering the study of cyber-physical systems.

https://depend.cs.uni-saarland.de/~dstan/