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.

*
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.

*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.
*

*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.