Gala

2019

Gems of Automata,

Logic and Algebra

co-located with FSTTCS 2019

This workshop will be targeted towards the participants of FSTTCS 2019, consisting of academicians and graduate students broadly in the area of theoretical computer science, with a focus on classical and recent topics in automata, logic and algebraic techniques in formal methods.

Speakers

 
photo.jpg

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

photo17.jpg

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

bild.jpg

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

mm-small.jpg

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

muschollkar.jpg

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

Schedule

 

16.40 - 17.40                Madhavan Mukund: Realizability for MSC specifications, revisited

16.10 - 16.40                Coffee break

15.10 - 16.10                Dietrich Kuske: The theory of the subword order

14.00 - 15.00                Benjamin Monmege: Logics for Weighted Automata

15.00 - 15.10                Short break

09.45 - 09.50                Welcome

09.50 - 10.50                Béatrice Bérard: Verification of Hybrid Systems

10.50 - 11.20                Coffee break

11.20 - 12.20                Anca Muscholl: The many facets of string transducers

12.30 - 14.00                Lunch break

17.45                              Concluding remarks

Registration

 

To register and for local information, please refer to the homepage of FSTTCS 2019.

Organization

 

C. Aiswarya

Chennai Mathematical Institute

S. Akshay

Indian Institute of Technology Bombay

Benedikt Bollig

CNRS, LSV, ENS Paris-Saclay

Sponsors