The aim of AVeRTS workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of probabilistic and real-time systems, and their application in automated verification of complex software and hardware systems. The satisfaction of time critical properties are crucial for ensuring safety in a wide range of computer science domains. The modeling, and the verification of such systems are hence of utmost importance. Algorithmic verification is an effective approach to analyse many properties of real-time systems: estimation of worst-case execution time, verification of timed specifications, synthesis of timely controllers, task scheduling and planning, etc. While these problems arise from different communities, formal methods provide a uniform approach to reason about timing constraints on the behaviors of systems. Several formalisms have been studied to model real-time systems (e.g. timed automata, timed Petri nets, etc) and formalize their specifications (e.g. metric temporal logic, timed computation tree logic, etc). In the recent years, stochastic models and logics have been introduced for quantitative evaluation of real-time systems, e.g. timeliness, reliability, response time, etc. The broad scope of the workshop includes
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
Schedule
08:00-09:00 | Registration |
08:50-09:00 | Opening Remarks |
09:00-10.00 | Benjamin Monmege |
Efficient Reactive Synthesis of MITL Properties | |
10:00-10:30 | Tea Break |
10:30-11:30 | Frédéric Herbreteau |
Improving search order for reachability testing in timed automata | |
11:30-12:30 | James Worrell |
Expressiveness for Real-Time Logics | |
12:30-14:00 | Lunch |
14:00-15:00 | Christoph Haase |
Cost chains, Parikh images, Eulerian circuits and the Counting Hierarchy | |
15:00-15:30 | Tea Break |
15:30-16:30 | Nicolas Markey |
Optimal strategies in weighted timed games: undecidability and approximation | |
16:30-17:30 | Paritosh Pandya |
Continuous versus Pointwise time in Real-time Logics: The Final Showdown |
Indian Institute of Science
Bengaluru, Karnataka
Pin Code: 560012