About AVeRTS

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

  • [Foundations and semantics:] theoretical aspects of timed and probabilistic systems, languages and comparison between different models such as timed automata, timed Petri nets, hybrid automata, probabilistic models, timed logics;
  • [Methods and tools:] algorithms, data structures, and software tools for analyzing timed and probabilistic systems with a focus on optimization and model-checking; The range of performance metrics of interest in probabilistic systems spans classical measures involving performance and reliability, as well as quantification of properties that are classically qualitative, such as safety, correctness, and security.
  • [Applications:] case studies highlighting the role of quantitative evaluation in the design of systems, where the notion of system is broad. Systems of interest include computer hardware and software architectures, communication systems, embedded systems, infrastructural systems, and biological systems. Moreover, tools for supporting the practical application of research results in all of the above areas are of special interest.


  • Christoph Haase, LSV, ENS Cachan
  • 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)

  • Frédéric Herbreteau, LaBRI, Bordeaux
  • 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.

  • Nicolas Markey, LSV, ENS Cachan
  • 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

  • Benjamin Monmege, Aix-Marseille Université, LIF, France
  • 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)

  • Paritosh Pandya, TIFR Mumbai
  • 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

  • James Worrell, Oxford
  • 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

    Event Schedule

    Venue: CSA Seminar Hall, CSA, IISc


    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