-
Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory
Authors:
Luca Aceto,
Antonis Achilleos,
Duncan Paul Attard,
Léo Exibard,
Adrian Francalanza,
Anna Ingólfsdóttir,
Karoliina Lehtinen
Abstract:
Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its execution. It is used as a lightweight verification technique to complement or substitute costlier methods such as model-checking.
In the regular setting, Hennessy-Milner logic with recursion, a variant of the modal mu-calculu…
▽ More
Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its execution. It is used as a lightweight verification technique to complement or substitute costlier methods such as model-checking.
In the regular setting, Hennessy-Milner logic with recursion, a variant of the modal mu-calculus, provides a versatile formalism for expressing linear- and branching-time specifications of the control flow of the system.
In this paper, we shift the focus from control to data and study the monitorability of an extension of this logic that allows one to express properties of the data flow. Data values are modelled as values from an infinite domain. They are stored using data variables and manipulated using predicates and first-order quantification.
The resulting logic is closely related to register automata with guessing. This correspondence yields a monitor synthesis algorithm, and allows us to derive a strict monitorability hierarchy between the different fragments of the logic, in stark contrast to the regular setting. In particular, restricting to deterministic monitors strictly reduces the set of monitorable properties.
Last, we exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic. We finally show that this is unavoidable because, in fact, there is no decidable fragment of the logic that captures all monitorable properties.
△ Less
Submitted 6 June, 2025;
originally announced June 2025.
-
A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders
Authors:
Léo Exibard,
Emmanuel Filiot,
Ayrat Khalimov
Abstract:
We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata i…
▽ More
We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register automata which can compare data for equality, i.e., for data domain $(N,=)$. This paper extends the decidability border to the domain $(N,<)$ of natural numbers with linear order. Our solution is generic: we define a sufficient condition on data domains (regular approximability) for decidability of register-bounded synthesis. The condition is satisfied by natural data domains like $(N,<)$. It allows one to use simple language-theoretic arguments and avoid technical game-theoretic reasoning. Further, by defining a generic notion of reducibility between data domains, we show the decidability of synthesis in the domain $(N^d,<^d)$ of tuples of numbers equipped with the component-wise partial order and in the domain $(Σ^*,\prec)$ of finite strings with the prefix relation.
△ Less
Submitted 8 June, 2022; v1 submitted 4 May, 2022;
originally announced May 2022.
-
A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders
Authors:
Léo Exibard,
Emmanuel Filiot,
Ayrat Khalimov
Abstract:
We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata i…
▽ More
We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register automata which can compare data for equality, i.e., for data domain (N,=). This paper extends the decidability border to the domain (N,<) of natural numbers with linear order. Our solution is generic: we define a sufficient condition on data domains (regular approximability) for decidability of register-bounded synthesis. The condition is satisfied by natural data domains like (N,<). It allows one to use simple language-theoretic arguments and avoid technical game-theoretic reasoning. Further, by defining a generic notion of reducibility between data domains, we show the decidability of synthesis in the domain (N^d,<^d) of tuples of numbers equipped with the component-wise partial order and in the domain (Σ^*,\prec) of finite strings with the prefix relation.
△ Less
Submitted 20 May, 2022; v1 submitted 20 May, 2021;
originally announced May 2021.
-
Computability of Data-Word Transductions over Different Data Domains
Authors:
Léo Exibard,
Emmanuel Filiot,
Nathan Lhote,
Pierre-Alain Reynier
Abstract:
In this paper, we investigate the problem of synthesizing computable functions of infinite words over an infinite alphabet (data $ω$-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…
▽ More
In this paper, we investigate the problem of synthesizing computable functions of infinite words over an infinite alphabet (data $ω$-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 describe specifications. Being non-deterministic, such transducers may not define functions but more generally relations of data $ω$-words. In order to increase the expressive power of these machines, we even allow guessing of arbitrary data values when updating their registers.
For functions over data $ω$-words, we identify a sufficient condition (the possibility of determining the next letter to be outputted, which we call next letter problem) under which computability (resp. uniform computability) and continuity (resp. uniform continuity) coincide.
We focus on two kinds of data domains: first, the general setting of oligomorphic data, which encompasses any data domain with equality, as well as the setting of rational numbers with linear order; and second, the set of natural numbers equipped with linear order. For both settings, we prove that functionality, i.e. determining whether the relation recognized by the transducer is actually a function, is decidable. We also show that the so-called next letter problem is decidable, yielding equivalence between (uniform) continuity and (uniform) computability. Last, we provide characterizations of (uniform) continuity, which allow us to prove that these notions, and thus also (uniform) computability, are decidable. We even show that all these decision problems are PSpace-complete for $(\mathbb{N},<)$ and for a large class of oligomorphic data domains, including for instance $(\mathbb{Q},<)$.
△ Less
Submitted 28 July, 2022; v1 submitted 18 January, 2021;
originally announced January 2021.
-
Church Synthesis on Register Automata over Linearly Ordered Data Domains
Authors:
Léo Exibard,
Emmanuel Filiot,
Ayrat Khalimov
Abstract:
In a Church synthesis game, two players, Adam and Eve, alternately pick some element in a finite alphabet, for an infinite number of rounds. The game is won by Eve if the omega-word formed by this infinite interaction belongs to a given language S, called the specification. It is well-known that for omega-regular specifications, it is decidable whether Eve has a strategy to enforce the specificati…
▽ More
In a Church synthesis game, two players, Adam and Eve, alternately pick some element in a finite alphabet, for an infinite number of rounds. The game is won by Eve if the omega-word formed by this infinite interaction belongs to a given language S, called the specification. It is well-known that for omega-regular specifications, it is decidable whether Eve has a strategy to enforce the specification no matter what Adam does. We study the extension of Church synthesis games to the linearly ordered data domains (Q, <) and (N, <). In this setting, the infinite interaction between Adam and Eve results in an omega-data word, i.e., an infinite sequence of elements in the domain.
We study this problem when specifications are given as register automata. Those automata consist in finite automata equipped with a finite set of registers in which they can store data values, that they can then compare with incoming data values with respect to the linear order. Church games over (N, <) are however undecidable, even for deterministic register automata. Thus, we introduce one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show that they are determined, and that deciding the existence of a winning strategy is in ExpTime, both for Q and N. This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to omega-regular games. We present an application of one-sided Church games to a transducer synthesis problem. In this application, a transducer models a reactive system (Eve) which outputs data stored in its registers, depending on its interaction with an environment (Adam) which inputs data to the system.
△ Less
Submitted 22 June, 2023; v1 submitted 25 April, 2020;
originally announced April 2020.
-
On Computability of Data Word Functions Defined by Transducers
Authors:
Léo Exibard,
Emmanuel Filiot,
Pierre-Alain Reynier
Abstract:
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 outpu…
▽ More
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 solvable in polynomial time.
△ Less
Submitted 19 February, 2020;
originally announced February 2020.
-
The Complexity of Transducer Synthesis from Multi-Sequential Specifications
Authors:
Léo Exibard,
Emmanuel Filiot,
Ismaël Jecker
Abstract:
The transducer synthesis problem on finite words asks, given a specification $S \subseteq I \times O$, where $I$ and $O$ are sets of finite words, whether there exists an implementation $f: I \rightarrow 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 $\mathcal{T}_f$. If such an implement…
▽ More
The transducer synthesis problem on finite words asks, given a specification $S \subseteq I \times O$, where $I$ and $O$ are sets of finite words, whether there exists an implementation $f: I \rightarrow 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 $\mathcal{T}_f$. If such an implementation $f$ exists, the procedure should also output $\mathcal{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 $ω$-words, solved by Büchi and Landweber in 1969, and the realisability problem is known to be ExpTime-c in both finite and $ω$-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.
△ Less
Submitted 9 May, 2019;
originally announced May 2019.
-
Synthesis of Data Word Transducers
Authors:
Léo Exibard,
Emmanuel Filiot,
Pierre-Alain Reynier
Abstract:
In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals ($ω$-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed t…
▽ More
In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals ($ω$-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we consider data $ω$-words instead, i.e., words over an infinite alphabet. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers. We consider different instances, depending on whether the specification is nondeterministic, universal or deterministic, and depending on whether the number of registers of the implementation is given or not.
In the unbounded setting, we show undecidability for both universal and nondeterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for nondeterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications.
△ Less
Submitted 17 March, 2021; v1 submitted 9 May, 2019;
originally announced May 2019.
-
Two-way Two-tape Automata
Authors:
Olivier Carton,
Léo Exibard,
Olivier Serre
Abstract:
In this article we consider two-way two-tape (alternating) automata accepting pairs of words and we study some closure properties of this model. Our main result is that such alternating automata are not closed under complementation for non-unary alphabets. This improves a similar result of Kari and Moore for picture languages. We also show that these deterministic, non-deterministic and alternatin…
▽ More
In this article we consider two-way two-tape (alternating) automata accepting pairs of words and we study some closure properties of this model. Our main result is that such alternating automata are not closed under complementation for non-unary alphabets. This improves a similar result of Kari and Moore for picture languages. We also show that these deterministic, non-deterministic and alternating automata are not closed under composition.
△ Less
Submitted 30 September, 2017;
originally announced October 2017.
