AVeRTS: Algorithmic Verification of Real-Time Systems

Speakers

Cost chains, Parikh images, Eulerian circuits and the Counting Hierarchy

Cost chains are Markov chains in which each transition additionally allows for incrementing an integer counter that represents costs occurring or time elapsing. Recently, quantile problems have been studied for cost chains: given a threshold t and some probability threshold p, is the probability that the target state is reached without exceeding the threshold t at least p? It turns out that this problem has a natural corresponding problem in formal language theory: given two DFA A,B over the same alphabet and a Parikh image i, does A accept more words than B with Parikh image i? In this talk, I will show that a particular version of this problem is hard for both PP and PosSLP and can be decided in the counting hierarchy. The technicalities of the upper bound involves strong results from circuit complexity as well as graph combinatorics in order to count Eulerian circuits in a graph.

This talk is based on joint work with Stefan Kiefer (Oxford) and Markus Lohrey (Siegen)

Improving search order for reachability testing in timed automata

Standard algorithms for reachability analysis of timed automata are sensitive to the order in which the transitions of the automata are taken. To tackle this problem, we propose a ranking system and a waiting strategy. In this talk we will discuss the reason why the search order matters and shows how a ranking system and a waiting strategy can be integrated into the standard reachability algorithm to alleviate and prevent the problem respectively. Experiments show that the combination of the two approaches gives optimal search order on standard benchmarks except for one example. This suggests that it should be used instead of the standard BFS algorithm for reachability analysis of timed automata.

Optimal strategies in weighted timed games: undecidability and approximation

A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question in this setting. Existence of optimal strategies is known to be undecidable in general, but the value problem (whether the optimal weight is less than a given value) had not been properly investigated. We prove that the value problem is undecidable as well, and introduce a large subclass of weighted timed games (to which the undecidability proof above applies) for which arbitrary-precise approximations of the optimal weight can be computed.

This talk is based on joint work with Patricia Bouyer and Samy Jaziri

Efficient Reactive Synthesis of MITL Properties

We study the bounded-precision reactive synthesis problem for real-time specifications. In this setting, the full reactive synthesis problem over classical real-time logics (such as MTL) is undecidable, and thus, we restrict the controller to have a required precision. For a specification described as the complement of a timed regular language, we show that if a controller exists with a finite number of clocks, a non primitive recursive number of clocks is sufficient. We therefore restrict further our attention to the bounded-resources synthesis problem, where we also limit the number of clocks of the controller. In the case of a specification given by a formula of MITL, we improve the results obtained in the case of MTL, to decrease the complexity of the realisability check from a non primitive recursive upper bound to 3-EXPTIME. We also propose an on-the-fly algorithm improving previous existing techniques.

This talk is based on joint work with Thomas Brihaye (UMONS), Morgane Estiévenart (UMONS), Gilles Geeraerts (ULB), and Nathalie Sznajder (Sorbonne Universités, UPMC, LIP6)

Continuous versus Pointwise time in Real-time Logics: The Final Showdown

Timed logics allow quantitative constraints on time distance between events to be specified. These timing constraints greatly enhance the ability of logic to specify complex behaviours. The properties of timed logics such as their expressive power and decidability (for a chosen set of operators) exhibit startling variations based on the underlying notion of time and the observability of time points. In this talk, we will map out the expressiveness and the decision complexities for satisfiability checking of various families of Metric Temporal Logic (MTL) under pointwise as well as continuous time and discuss their differences. An overview of the techniques (EF Games, Alternating Timed Automata, Temporal Projections) used to prove some of these results will also be given.

This talk is based on joint work with Krishna.S, Khushraj Madnani and Simoni Shah

Expressiveness for Real-Time Logics

Monadic first-order logic over the ordered real line with Euclidean metric is a natural and canonical language for specifying properties of real-time systems. In this talk we present a compositional principle for this logic and derive from this the 3-variable property: every formula with a most 3 free variables is equivalent to a formula that uses 3 variables in total, bound or free. We go on to present a stronger result, a generalisation of Kamp's Theorem, showing the expressive completeness of Metric Temporal Logic for monadic first-order logic of order and metric. To prove the latter result we develop a metric analog of Gabbay's notion of separation for linear temporal logic formulas. The new separation notion is closely related to the above-mentioned composition principle.

This talk is based on previous joint work with Antonopoulos, Hunter, Ouaknine and Raza