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
Lossy Channel Systems with Data
Lossy channel systems are a classical model with applications ranging from the modelling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this talk, we present two extensions of lossy channel systems. In the first part of the talk, we extend lossy channel systems by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of Timed Lossy Channel Systems (TLCS). We show that the state reachability problem is decidable for TLCS. In the second part of the talk, we extend lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.
This talk is based on previous joint work with Parosh Aziz Abdula, Jonathan Cederberg and C. Aiswarya
Analyzing Timed Systems Using Tree Automata
Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. As an example, we develop the technique on timed pushdown systems. We show that their behaviors are graphs of bounded tree-width. Hence, they can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems.
This is joint work with S. Akshay and S. Krishna from IIT Bombay, the extended abstract appeared in CONCUR 2016
Timed Automata and Battery Kinetics in Thermosphere
For a satellite orbiting the earth all resources are sparse and the most critical resource of all is power. It is therefore crucial to have detailed knowledge on how much power is available for an energy harvesting satellite in orbit at every time – especially when in eclipse, where it draws its power from onboard batteries. This presentation addresses this problem by a two-step procedure to perform task scheduling for satellites orbiting the earth. It combines cost-optimal reachability analyses of priced timed automata networks with a realistic kinetic battery model capable of capturing capacity limits as well as stochastic fluctuations. The procedure has been put in place for the automatic and resource-optimal day-ahead scheduling of GomX–3, a power-hungry nanosatellite orbiting the earth in thermosphere. We explain how this approach has overcome existing problems, has led to improved designs, and has provided new insights.
This presentation covers joint work with Morten Bisgaard, David Gerhardt (both from Gomspace AS, Denmark), Jan Krčál, Gilles Nies, and Marvin Stenger (all from Saarland University, Germany)
Timed pushdown automata and branching vector addition systems
We advocate the framework of first-order definable sets (also known as sets with atoms) as the right setting to define and investigate timed extensions of automata. The emptiness problem for the timed extension of prefix-rewriting is undecidable, but decidable (in EXPTIME) for the timed extension of context-free grammars. The decidability status of the timed extension of pushdown automata was unknown (except for decidability results for some subclasses). We prove that the emptiness problem of the timed extension of pushdown automata is inter-reducible with the same problem for an extension of branching vector addition systems in dimension one, and that the latter problem is decidable.
Algorithmic Verification of Stability of Hybrid Systems
Hybrid systems refer to systems exhibiting mixed discrete-continuous behaviors and arise as a natural byproduct of the interaction of a network of embedded processors with physical systems. Hybrid systems manifest in safety critical application domains including aeronautics, automotive, robotics and power systems. Reliability is of utmost importance, and a grand challenge in the area is the development of techniques and tools to aid the development of high-confidence hybrid systems. In this talk, we focus on the verification of stability of hybrid systems. Stability is a fundamental property in control system design and captures the notion that small perturbations to the initial state or input to the system result in only small variations in the eventual behavior of the system. We present foundations for approximation based analysis of stability, and provide formal simplification techniques based on the classical predicate abstraction and hybridization techniques for their analysis. We illustrate the benefits of using our algorithmic approach as compared to well-known deductive methods for automated verification of stability based on Lyapunov functions.
Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs
The winning condition of a parity game with costs requires an arbitrary, but fixed bound on the distance between occurrences of odd colors and the next occurrence of a larger even one. Such games quantitatively extend parity games while retaining most of their attractive properties, i.e, determining the winner is in NP and co-NP and one player has positional winning strategies. We show that the characteristics of parity games with costs are vastly different when asking for strategies realizing the minimal such bound: the solution problem becomes PSPACE-complete and exponential memory is both necessary in general and always sufficient. Thus, playing parity games with costs optimally is harder than just winning them. Moreover, we show that the tradeoff between the memory size and the realized bound is gradual in general.
Based on joint work with Alexander Weinert, published at CSL 2016
|Easy To Win, Hard To Master: Optimal Strategies in Parity Games with Costs|
|Timed Automata and Battery Kinetics in Thermosphere|
|Timed PDA and Branching Vector Addition Systems|
|Algorithmic Verification of Stability of Hybrid Systems|
|Analyzing Timed Systems Using Tree Automata|
|16:30-17:30||M. Faouzi Atig|
|Lossy Channel Systems with Data|
Chennai Mathematical Institute
H1, SIPCOT IT Park, Siruseri,
Tamil Nadu 603103