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
Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement
In this talk, I will present Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, the uniformity being defined with respect to volume measure of timed languages previously studied by Asarin, Degorre and me. We implement our algorithms using tools PRISM, SageMath and COSMOS, and demonstrate their usefulness on statistical timed language inclusion measurement in terms of volume.
This talk is based on joint work with B. Barbot, B. Beunardeau and M. Kwiatkowska
Modelling time and recursion
Timed automata are a classical formalism used to model time in finite state systems. The classical view on timed automata uses *clocks* recording differences between the timestamps of events. Another view is to use *registers* recording the timestamps themselves. While these two views are essentially equivalent for finite state systems, we argue that in the presence of recursion the register approach yields a more expressive and natural model, and that this model is still analysable algorithmically.
A decidable logic for finite word transductions
A finite word transduction is a binary relation of finite words. After a brief introduction on recent results about word transductions, in particular about logics, algebra and automata for word transductions, the talk introduces a new logic to specify properties of word transductions, and presents some of its expressiveness and algorithmic properties. In particular, the model-checking and synthesis problems for the expressive class of MSO-definable (functional) transductions, against/from properties specified in this logic, are considered. A connection with a logic for finite words over infinite alphabets (data words) will be shown as well.
This work is joint with Luc Dartois (ULB) and Nathan Lhote (ULB / UBordeaux).
A tour of recent results on word transducers
Transducers are a fundamental notion of computation, where one is interested in transforming objects. Finite state word transducers were considered in very early work in formal language theory, and it was soon clear that they are much more challenging than the classical finite-state automata. In this talk we survey recent results on word transducers. We first discuss how some of the classical connections between automata, logic and algebra extend to transducers. Then we consider some advanced constructions related to two-way transducers.
Optimal Control for Multi-Mode Systems with Discrete Costs
We study optimal time-bounded control in multi-mode systems with discrete costs. Multi-mode systems are an important subclass of linear hybrid systems, in which there are no guards on transitions and all invariants are global. Each state has a continuous cost attached to it, which is linear in the sojourn time, while a discrete cost is attached to each transition taken. We show that an optimal control for this model can be computed in NEXPTIME and approximated in PSPACE. We also show that the one-dimensional case is simpler: although the problem is NP-complete (and in LOGSPACE for an infinite time horizon), we develop an FPTAS for finding an approximate solution.
This talk is based on a joint work with Mahmoud A. Mousa and Sven Schewe.
State equations for Petri Nets with data
Algebraic techniques for Petri Nets are an important tool in the nets analysis. From the applications point of view, to model certain behaviors and features, the extensions of Petri nets are needed. One of the most established models is Colored Petri Nets. In 2008, in the paper "Nets with Tokens which Carry Data", it appears under a new name, so called data nets, where the emphasis is put on restrictions on data/colors manipulation. I will present preliminary published and unpublished results on Petri Nets with data.