Verification of Hybrid Systems

​

For Hybrid systems that combine discrete and continuous components, verification is a notoriously difficult task. I will give several decidability results involving various techniques, starting with the well known model of Timed Automata and extending the quotient construction to Polynomial Interrupt Timed Automata. In the last part, I will show some conditions to obtain a bisimulation for o-minimal dynamical systems where trajectories can overlap.

​

​

​

​

Sorbonne Université

Béatrice Bérard

Logics for Weighted Automata

​

This talk will present the line of results obtained on the relationship between weighted automata and weighted logics. The story started 15 years ago with the introduction of a quantitative semantics for MSO logic over words and an equivalence theorem between weighted automata and a restricted weighted MSO logic. Since then, many extensions have been studied: from words to trees, infinite words, pictures, etc; from semirings to more general weight computations. Also, the proof techniques have matured, from low level, carefully mimicking the classical proofs in the boolean setting, to higher level, using various abstract semantics. We illustrate this evolution by presenting the results by using a core weighted logic and its abstract semantics as multisets of weight structures. The equivalence between weighted automata and core weighted logic holds at the level of the abstract semantics. We will then extend the logic showing an equivalence with pebble weighted automata. As an opening, we will also demonstrate the versatility of the weighted automata approach by instantiating it into the transducer setting, showing a possible lead towards the design of an alternative logic for (non-necessarily functional) transductions, a topic resurgent in the automata community.

Aix-Marseille Université

Benjamin Monmege

The theory of the subword order

​

The subword order is one of the simplest well quasi orders which  allows, e.g., its use in termination proofs and in the verification of lossy channel systems. In this talk, we review decidable instances of the satisfiability problem for different logics that allow to make statements about this partial order. The logics we consider are all first-order languages; they vary in as far as we may allow threshold
or modulo-counting quantifiers, restrict the quantifier alternation or the number of variable names, and can or cannot use constants or regular predicates. Some of the results on the subword order are shown to also hold for Mazurkiewicz traces.

Technische Universität Ilmenau

Dietrich Kuske

Realizability for MSC specifications, revisited

​

The realizability question asks whether an abstract behavioural specification is implementable in a target computational model. We examine this problem for message sequence chart (MSC) specifications with respect to communicating finite-state machines.  MSC specifications describe joint behaviours of a distributed set of agents communicating via message-passing. Such specifications may be unrealizable for a variety of reasons, including the inevitability of implied scenarios --- unwanted behaviours that are locally compatible with the given MSC specification --- as well as the possibility of deadlock. The realizability question for MSC specifications has been explored extensively in the past two decades and would appear to be a solved problem. Nevertheless, we show that there are subtleties involved and some interesting and relevant questions remain unresolved.

Chennai Mathematical Institute

Madhavan Mukund

The many facets of string transducers

​

Regular word transductions extend the robust notion of regular languages from a qualitative to a quantitative reasoning. They were already considered in early papers of formal language theory, but turned out to be much more challenging. The last decade brought considerable research around various transducer models, aiming to achieve similar robustness as for automata and languages. In this paper we survey some older and more recent results on string transducers. We present classical connections between automata, logic and algebra extended to transducers, some genuine definability questions, and review approaches to the equivalence problem. Joint work with G. Puppis (U. of Bordeaux and U. of Udine).

Université Bordeaux

Anca Muscholl