Author name cluster

Léo Exibard

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

Highlights Conference 2024 Conference Abstract

Runtime monitoring for Hennessy-Milner logic with recursion over systems with data

Léo Exibard

Runtime verification consists in checking whether a program satisfies a given specification by observing the trace it produces during its execution. In the regular setting, Hennessy-Milner logic with recursion (recHML), a variant of the modal $\mu$-calculus, provides a versatile back-end for expressing linear- and branching-time specifications. In this talk, I discuss an extension of this logic that allows to express properties over data values (i. e. values from an infinite domain) and examine which fragments can be verified at runtime. Data values are manipulated through equality tests in modalities and through first-order quantification outside of them. They can also be stored using parameterised recursion variables. I then examine what kind of properties can be monitored at runtime, depending on the monitor model. A key aspect is that the logic has close links with register automata with non-deterministic reassignment, which yields a monitor synthesis algorithm, and allows to derive impossibility results. In particular, contrary to the regular case, restricting to deterministic monitors strictly reduces the set of monitorable properties. I then conclude by examining whether we can delineate a maximally monitorable fragment for the logic, and the picture turns out to be quite intriguing. This is joint work with the MoVeMnt team (Reykjavik University): Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Adrian Francalanza, Karoliina Lehtinen.

Details

Highlights Conference 2020 Conference Abstract

On Computability of Data Word Functions Defined by Transducers

Léo Exibard

In this paper, we investigate the problem of synthesizing computable functions of infinite words over an infinite alphabet (data omega-words). The notion of computability is defined through Turing machines with infinite inputs which can produce the corresponding infinite outputs in the limit. We use non-deterministic transducers equipped with registers, an extension of register automata with outputs, to specify functions. Such transducers may not define functions but more generally relations of data omega-words, and we show that it is PSpace-complete to test whether a given transducer defines a function. Then, given a function defined by some register transducer, we show that it is decidable (and again, PSpace-complete) whether such function is computable. As for the known finite alphabet case, we show that computability and continuity coincide for functions defined by register transducers, and show how to decide continuity. We also define a subclass for which those problems are PTime.

Details

Highlights Conference 2018 Conference Abstract

Automatic Synthesis of Systems with Data

Léo Exibard

ABSTRACT. System synthesis aims at automatically generating a system from its high level specification. An interesting setting is the one of reactive systems, which are systems that continuously react, in a timely fashion, to the input stimuli of the environment in which they are executed. Their interaction yields a pair of input and output words. Then, the specification, provided as a logical formula or as an automaton, describes the set of admissible behaviours, which can be seen as a relation between input and output words. Most of the works on synthesis has been conducted under the assumption that the input and output alphabets are finite. However, many applications require an infinite set to model programs manipulating integers, reals, timestamps, etc. Thus, we consider specifications over data words, which are finite sequences of pairs in A x D, where A is a finite alphabet and D is an infinite set (of data). Then, from those specifications, our aim is to determine, for different classes of implementations, whether the synthesis problem is decidable and, if yes, what is its complexity. When the synthesis problem only constrains admissible behaviours, without imposing additional requisits, it can be formulated as a uniformisation problem, following a set-theoretic terminology. For f a function and R a relation, we say that f uniformises R when f and R have the same domain and when f (understood as a relation) is a subrelation of R. Then, the uniformisation problem from a class of relations C to a class of functions F can be defined as: given a relation R in C, provide a function f in F which uniformises R if it exists, and answer No otherwise. In this work, we consider instances of the uniformisation problem. To represent relations over data words, we introduce two models, namely Nondeterministic Data Transducers and Deterministic Register Transducers, which are generalisations of Nondeterministic Finite Transducers to data words. To handle data, we equip the machine with registers, in which it can store the data to output it later on. The difference between the two models is that the first one is not allowed to conduct any tests on the data which is read, whereas the second can test equality between the data and the content of one register. For both models, we provide an algorithm to solve the uniformisation problem to their input-deterministic version, i. e. to a machine which, given an input, deterministically produces an output.

Details

MFCS Conference 2018 Conference Paper

The Complexity of Transducer Synthesis from Multi-Sequential Specifications

Léo Exibard
Emmanuel Filiot
Ismaël Jecker

The transducer synthesis problem on finite words asks, given a specification S subseteq I x O, where I and O are sets of finite words, whether there exists an implementation f: I - > O which (1) fulfils the specification, i. e. , (i, f(i))in S for all i in I, and (2) can be defined by some input-deterministic (aka sequential) transducer T_f. If such an implementation f exists, the procedure should also output T_f. The realisability problem is the corresponding decision problem. For specifications given by synchronous transducers (which read and write alternately one symbol), this is the finite variant of the classical synthesis problem on omega-words, solved by Büchi and Landweber in 1969, and the realisability problem is known to be ExpTime-c in both finite and omega-word settings. For specifications given by asynchronous transducers (which can write a batch of symbols, or none, in a single step), the realisability problem is known to be undecidable. We consider here the class of multi-sequential specifications, defined as finite unions of sequential transducers over possibly incomparable domains. We provide optimal decision procedures for the realisability problem in both the synchronous and asynchronous setting, showing that it is PSpace-c. Moreover, whenever the specification is realisable, we expose the construction of a sequential transducer that realises it and has a size that is doubly exponential, which we prove to be optimal.

Details