Difference between revisions of "Seminar/2022-06-22"
From LRDE
(Created page with "{{SeminarHeader | id = 2022-06-22 | date = Mercredi 22 juin 2022 | schedule = 11h - 12h | location = Https://meet.jit.si/SeminaireLRDE \& Salle KB000 }} {{Talk | id = 2...") |
|||
| Line 12: | Line 12: | ||
resources are parameterized (i.e. not known a priori), and the corresponding |
resources are parameterized (i.e. not known a priori), and the corresponding |
||
verification problem asks whether a given epistemic property is true regardless |
verification problem asks whether a given epistemic property is true regardless |
||
| − | of the instantiation of the parameters. As in other regular model checking |
+ | 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, |
Parameterized systems might also require an arbitrary number of announcements, |
||
leading to the introduction of the so-called iterated public announcement. |
leading to the introduction of the so-called iterated public announcement. |
||
| − | Although model checking becomes undecidable because of this operator, we |
+ | 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 |
regularity properties are met. We illustrate the approach on the Muddy Children |
||
puzzle, and we further discuss dynamic protocol encodings through the Dining |
puzzle, and we further discuss dynamic protocol encodings through the Dining |
||
| Line 27: | Line 27: | ||
Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomas |
Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomas |
||
| duration = 1h |
| duration = 1h |
||
| − | | orator = Daniel Stan, |
+ | | orator = Daniel Stan, Technische Universität Kaiserslautern |
| − | | resume = Daniel Stan |
+ | | resume = 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 |
||
| − | Holger Hermanns since May 2017. Before that, he got his Ph.D at ENS Cachan/Paris |
||
| + | supervision of Patricia Bouyer and Nicolas Markey, then a PostDoc in the |
||
| − | Saclay, whose title is “Randomized Strategies in Concurrent Games”, and that he |
||
| + | Dependable Systems and Software chair of Saarbrücken. His research interests |
||
| − | defended in March 2017. His research includes quantitative verification |
||
| + | include formal methods and model checking techniques with a particular focus on |
||
| − | techniques, parametric stochastic systems, game theoretical approaches. He is |
||
| + | Regular Model Checking and Automatic Structures, Parameterized Systems, |
||
| − | more recently considering the study of cyber-physical systems. |
||
| + | Stochastic Systems and Games. In particular, his current work put an emphasis on |
||
| + | exact learning algorithms with applications to model checking. |
||
| schedule = 11h - 12h |
| schedule = 11h - 12h |
||
| title = Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems |
| title = Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems |
||
| − | | urls = https:// |
+ | | urls = https://arg.cs.uni-kl.de/gruppe/stan/ |
}} |
}} |
||
Revision as of 12:19, 27 June 2022
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, 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.
https://arg.cs.uni-kl.de/gruppe/stan/