Prochain Exposé
March 16, 4PM (Paris/France). Salle Aurigny (Online).
Christoph Haase (University of Oxford)
Directed Reachability for Infinite-State Systems ?
Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computa- tionally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as A ∗ and greedy best-first search. We provide and evaluate a prototype implemen- tation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.
Exposés des semaines suivantes
March 23, 3PM (Paris/France). Salle Aurigny (sans visio)
Edwin Hamel-De le Court (Université Libre de Bruxelles)
Two-player boundedness counter games
We consider two-player zero-sum games with winning objectives beyond regular languages, expressed as a parity condition in conjunction with a Boolean combination of boundedness conditions on a finite set of counters which can be incremented, reset to zero, but not tested. A boundedness condition requires that a given counter is bounded along the play. Such games are decidable, though with non-optimal complexity, by an encoding into the logic WMSO with the unbounded and path quantifiers, which is known to be decidable over infinite trees. Our objective is to give tight or tighter complexity results for particular classes of counter games with boundedness conditions, and study their strategy complexity. In particular, counter games with conjunction of boundedness conditions are easily seen to be equivalent to Streett games, so, they are CoNP-complete. Moreover, finite-memory strategies suffice for Eve and memoryless strategies suffice for Adam. For counter games with a disjunction of boundedness conditions, we prove that they are in solvable in NP ∩ CoNP, and in PTime if the parity condition is fixed. In that case memoryless strategies suffice for Eve while infinite memory strategies might be necessary for Adam. Finally, we consider an extension of those games with a max operation. In that case, the complexity increases: for conjunctions of boundedness conditions, counter games are EXPTIME-complete.
April 13, 3PM (Paris/France). Salle Aurigny.
Benjamin Bordais (Univ Paris-Saclay)
Playing (almost-)optimally in concurrent games with parity objectives
In a two-player win/lose concurrent graph game, two players at a given state concurrently (i.e. simultaneously) choose an action (among a finite set of available actions) which leads to another state. The process is repeated indefinitely thus forming an infinite sequence of states. The winnor of the game is determined by an objective (i.e. a subset of infinite sequences of states). Concurrent games are more general than their turn-based counterparts in which, at each state, only one player chooses the next state to visit. However, this comes at the cost of not enjoying the desirable properties that turn-based games do. (For instance, in turn-based games with parity objectives, there are always optimal strategies that are deterministic and positional whereas optimal strategies do not exist in general in concurrent games.) In this talk, I will illustrate the turn-based and concurrent formalisms and show on specific examples why concurrent games behave more poorly than turn-based games. Then I will present how to build concurrent games that are more general than turn-based games but still enjoy similar properties that turn-based game do for specific objectives.
Vos propositions sont les bienvenues !
