Verification Seminar

Games with a fixed number of players have been extensively studied in the literature. For instance, in traditional concurrent games on graphs, a fixed number of players take decisions simultaneously, which determine the next vertex of the game. With Nathalie Bertrand and Patricia Bouyer-Decitre, we introduced a parameterized variant of such concurrent games, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear (regular) languages to describe the possible move combinations that lead from one vertex to another. For instance, the label a+ represents that all players choose action a, while ab+ is the situation where the first player chooses a, while all other players play b.

In this talk, I will report on results on two different settings on the so-called parameterized concurrent games. The first setting is where a distinguished player Eve is trying to achieve a given objective against the coalition of her opponents, not knowing a priori how many they are; and second, a coalition setting, where all players collectively try to achieve a common goal. In the first setting, we prove the existence of a winning strategy for Eve is decidable, and show for reachability objectives, the problem is PSPACE-complete. In the coalition setting, we show that for safety objectives, the existence of a winning coalition strategy is decidable, and show that the problem is in EXPSPACE and PSPACE-hard. Furthermore, if it exists, one can synthesize a winning coalition strategy with the memory size at most exponential.

Timed Automata is a popular tool for modelling real-time systems. Updatable Timed Automata (UTA) extends the model of Timed Automata, by allowing more general updates (to clock variables) of the form x := y + 1, z := 2 etc. Checking reachability for Timed Automata is PSPACE-complete, whereas, it is undecidable for the general class of UTA. However, there are several (interesting) subclasses of UTA for which reachability remains decidable.

The aim of our work is to improve the state-of-the-art of checking reachability in the decidable subclasses of UTA. There exists an efficient reachability algorithm-based on ‘zones’ for Timed Automata, when no diagonal constraints (i.e. inequalities of the form x - y <= 3) are present in its transitions. We extend this algorithm to be able to check reachability, firstly, when diagonal constraints are present in Timed Automata, and also, for the decidable subclasses of UTA.

To ensure that this algorithm terminates, we need a suitable simulation relation between zones. We propose such a simulation relation and provide an algorithm for checking this relation between two zones. Preliminary experiments show improvement over the existing algorithms.

This talk will be based on joint work with Paul Gastin (ENS Paris-Saclay) and B Srivathsan (Chennai Mathematical Institute).

Petri nets are a popular and well-studied formal model for the representation and verification of parallel processes. The central problem for Petri nets is reachability: given two configurations of a Petri net, does there exist a run from one to the other. This problem is very difficult: it has recently been proven to be Tower-hard (non-elementary). This motivates the study of subclasses in the hopes of having a more reasonable complexity. Some classic syntactic restrictions of Petri nets are BPP nets (Branching Parallel Process), or marked graphs (sometimes called T-systems).

We introduce and study a new syntactic restriction: immediate observation Petri nets (or IO nets), motivated by applications to population protocols — a model of distributed computation — and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for IO nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. We also show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques (like FAST).

Finally, we introduce and study a powerful generalization of IO nets: Branching IO nets (BIO nets), in which transitions can create tokens. BIO nets extend both IO nets and BPP nets. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the parameterized coverability and reachability problems remain in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.

Link for recorded video: here

Active learning of timed languages is concerned with the inference of timed automata by observing some of the timed words in their languages. The learner can query for the membership of words in the language or propose a candidate model and ask for equivalence with the target. The major difficulty of this framework is the inference of clock resets, which are central to the dynamics of timed automata but not directly observable.

Interesting first steps have already been made by restricting to the subclass of event-recording automata, where clock resets are tied to observations. In order to advance towards learning of general timed automata, we generalize this method to a new class, called reset-free event-recording automata, where transitions may reset no clocks.

Central to our contribution is the notion of invalidity of reset combinations. This notion is a key to any efficient active learning procedures for generic timed automata.In this talk i will present the results of the Formats 2020 of same name, as well as some more recent results, and interesting research directions.

Link for recorded video: here

The state complexity of a regular operation is a measure of how much the operation increases the complexity of its inputs. Even though operational state complexity is an active research topic, there is no general framework built for computing state complexities. A usual method is to compute an upper bound by resorting to some ingenious tricks, and then to provide a family of languages, called a witness, whose image by the operation matches this upper bound. Furthermore, witnesses are chosen in an ad hoc manner, and no general results are known.

We introduce an algebraic framework, from which we derive a method to compute the state complexity of a large number of operations. This method can be used to recover some well-known state complexity results, like the exact state complexity of the Kleene star, catenation, or of any boolean operation. In addition, we very quickly give some ideas that we used to compute the exact state complexity of the Kleene star composed with symmetric difference, which is a new result.

Finally, we study a class of modifiers defined by simple algebraic properties, called friendly modifiers. We give the regular operations associated with friendly modifiers, and we give their maximal state complexity.

Link for recorded video: here

In this paper, we study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. For games in which objectives are either all parity or all reachability objectives, we show that this problem is fixed-parameter tractable and NEXPTIME-complete. This problem is already NP-complete in the simple case of reachability objectives and graphs that are trees.

Link for recorded video: here

The notion of Nash equilibrium (NE) is one of the most important solution concepts in game theory: it refers to profiles of strategies such that no player has an incentive to change unilaterally their strategy. But in sequential games, NEs suffer from the problem of non-credible threats: there can be NEs where some players do not play rationally in subgames, and use non-credible threats to force the NE. This is why one could prefer the stronger notion of subgame-perfect equilibrium (SPE): a profile of strategies is an SPE if it is an NE in all the subgames.

In these seminars, we study infinite duration games on graph with mean-payoff objectives. While NEs are guaranteed to exist on such games, it is not the case of SPEs. We provide an algorithmic solution to the SPE existence problem, and a characterization of the plays that are SPE plays.

In a first seminar, we will introduce the concept of requirement, that defines a notion of rationality for a coalition of players, and the concept of negociation, a function that updates the requirements of each player according to the requirements of the other players. We show that SPEs are characterized by the requirement that is the least fixpoint of the negociation function. In a second seminar, we provide a way to compute effectively the negociation function, by constructing a game on the game, called negociation game.

Link for recorded video: Part 1 Part 2

Church's synthesis problem asks whether a synchronous specification from infinite words to infinite words can be realized by a synchronous function. We relax this requirement and ask whether a synchronous specification from infinite words to infinite words can be realized by a computable function, in other words, we simply ask whether a specification is implementable.

This question has been previously studied by Holtmann et al. who showed that the problem is decidable (it was later shown to be EXPtime-complete) for synchronous specifications with total domain. We show that the question is EXPtime-complete for synchronous specifications with partial domain. A specification with partial domain is implementable if for every input sequence in its domain an output sequence can be computed that is correct w.r.t. the specification. A fundamental difference between the total and the partial domain setting is that, if the specification is implementable, in the former setting sequential transducers suffice to do so and in the latter setting a more powerful computation model is needed. We show that if a synchronous specification from infinite words to infinite words is implementable then a deterministic two-way transducer can compute an implementation.

This is joint work with Emmanuel Filiot.

In this seminar, we explore a robust version of the Linear Temporal Logic (LTL) fragment that only contains the always and eventually temporal operators. Formulas in rLTL are syntactically identical to LTL formulas but are endowed with a many-valued semantics that encodes robustness. In particular, the semantics of the rLTL formula \varphi\implies\psi is such that a “small” violation of the environment assumption \varphi is guaranteed to only produce a “small” violation of the system guarantee \psi.

In addition to that, we explore a payoff game based on rLTL which addresses the problem of synthesizing controllers that are optimal with respect to a quality criterion based on rLTL.  Intuitively, given a property P that the controller should satisfy always, we would prefer a controller that satisfies P infinitely often over one that only satisfies P finitely often; similarly, we would prefer a controller that satisfies P eventually always over one that satisfies P infinitely often, and so on.

Link for recorded video: here

We consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice is used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice.

Link for recorded video: here

The framework used in Games and in Markov decision processes is quite close. The main difference is that the objective in a game has to be fulfilled whatever happens, and the objective in a Markov Decision Process has to be fulfilled with at least a given probability. We are interested in a generalization by considering Boolean combinations of such objectives. More precisely, we consider combinations of omega-regular properties, defined with a parity condition, where every condition needs to be enforced either surely, almost surely, existentially, or with non-zero probability. In this setting, relevant strategies are randomized infinite memory strategies: both infinite memory and randomization may be needed to play optimally. We provide algorithms to solve the general case of Boolean combinations. We also investigate relevant subcases and report on complexity bounds for these problems.

Link for recorded video: here

Part of MoVe seminar (LIS, Aix-Marseille Université)

We investigate the problem of synthesizing computable functions of infinite words over an infinite alphabet (data omega-words). The notion of computability is defined through Turing machines with infinite inputs which can produce the corresponding infinite outputs in the limit. We use non-deterministic transducers equipped with registers, an extension of register automata with outputs, to specify functions. Such transducers may not define functions but more generally relations of data omega-words, and we show that it is PSpace-complete to test whether a given transducer defines a function. Then, given a function defined by some register transducer, we show that it is decidable (and again, PSpace-complete) whether such function is computable. As for the known finite alphabet case, we show that computability and continuity coincide for functions defined by register transducers, and show how to decide continuity.

Link for recorded video: here

Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an infinite alphabet, and compare this data for equality. They provide a simple formalism to specify the behaviour of reactive systems operating data. Initially defined with the equality predicate only, they can be extended to allow for comparison of data with regards to a linear order, like (N,<) or (Q,<). We study the synthesis problem for those specifications. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately pick some data, and Eve wins whenever their interaction satisfies the specification, which is a language of infinite words over infinite data alphabet. Unfortunately, such games are undecidable already for specifications described by deterministic register automata. Therefore, we study one-sided Church games, where Eve uses a finite alphabet but Adam still manipulates data. We show such games are decidable in exponential time in the number of registers in the specification, both for Q and N, are determined, and strategies describable by finite-state register transducers suffice for Eve to win. To obtain this result we study constraint sequences, which abstract the behaviour of register automata and allow for reduction of Church games to omega-regular games. Finally, we apply these results to the transducer-synthesis problem.

Link for recorded video: here