DEVINE: Vérification efficace pour des systèmes distribués fiables

International audience

International audience

Deterministic two-way transducers with pebbles (aka pebble transducers) capture the class of polyregular functions, which extend the string-to-string regular functions allowing polynomial growth instead of linear growth. One of the most fundamental operations on functions is composition, and (poly)regular functions can be realized as a composition of several simpler functions. In general, composition of deterministic two-way transducers incur a doubly exponential blow-up in the size of the inputs. A major improvement in this direction comes from the fundamental result of Dartois et al. [10] showing a polynomial construction for the composition of reversible two-way transducers. A precise complexity analysis for existing composition techniques of pebble transducers is missing. But they rely on the classic composition of two-way transducers and inherit the double exponential complexity. To overcome this problem, we introduce reversible pebble transducers. Our main results are efficient uniformization techniques for non-deterministic pebble transducers to reversible ones and efficient composition for reversible pebble transducers.

We consider the automatic online synthesis of black-box test cases from functional requirements specified as automata for reactive implementations. The goal of the tester is to reach some given state, so as to satisfy a coverage criterion, while monitoring the violation of the requirements. We develop an approach based on Monte Carlo Tree Search, which is a classical technique in reinforcement learning for efficiently selecting promising inputs. Seeing the automata requirements as a game between the implementation and the tester, we develop a heuristic by biasing the search towards inputs that are promising in this game. We experimentally show that our heuristic accelerates the convergence of the Monte Carlo Tree Search algorithm, thus improving the performance of testing.

International audience

We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value. This reachability problem has been known to be NP-hard and in PSPACE, and characterising its computational complexity has been left as a challenging open question by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell (2020). We reduce the complexity gap, placing the problem into the second level of the polynomial hierarchy, namely into the class $\mathsf{coNP}^{\mathsf{NP}}$. In the presence of both equality and disequality tests, our upper bound is at the third level, $\mathsf{P}^{\mathsf{NP}^{\mathsf{NP}}}$. To prove this result, we show that non-reachability can be witnessed by a pair of invariants (forward and backward). These invariants are almost inductive. They aim to over-approximate only a "core" of the reachability set instead of the entire set. The invariants are also leaky: it is possible to escape the set. We complement this with separate checks as the leaks can only occur in a controlled way.

International audience

Metro networks are usually operated with timetables, i.e. schedules with fixed dates for departure and arrival events. However, when a delay occurs, timetables have to be adapted to mitigate the effect of this time gap. This paper proposes several algorithms to propagate the effects of primary delays in a timetable. The principle of delay propagation is to compute the minimal modification to the original timetable induced by this delay. We define timetables as weighted acyclic graphs depicting events, causal dependencies, and timing constraints, and show that the minimal modification is achieved by rescheduling events as soon as possible in this graph. We propose five algorithms to compute efficiently new consistent dates after a delay, with the minimal modification w.r.t. the original timetable. The first algorithm uses properties of critical paths in the timetable, the second algorithm builds a topological ordering on events before a linear rescheduling of events dates. The third algorithm is a recursive scheme that may explore the whole timetable in the worst case, but stops on events that need no rescheduling. The next algorithms are still recursive schemes, but use heuristics to choose an ordering for events updates. Recursive schemes have a bad theoretical worst case complexity. However, tests on two real case studies show that they are efficient in practice, and reschedule timetables in a fraction of seconds.