AVeRTS: Algorithmic Verification of Real-Time Systems

Speakers

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.