Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then 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, and show this is the best we can get.

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 (ℕ, =). This paper extends the decidability border to the domain (ℕ, <) 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 (ℕ, <). 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 (ℕ^d, <^d) of tuples of numbers equipped with the component-wise partial order and in the domain (Σ^*,≺) of finite strings with the prefix relation.

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 $$({\mathbb {Q}},\le )$$ and $$({\mathbb {N}},\le )$$ . 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 $$({\mathbb {N}},\le )$$ 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 $${\mathbb {Q}}$$ and $${\mathbb {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.

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 describe specifications. Being non-deterministic, such transducers may not define functions but more generally relations of data $\omega$-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 $\omega$-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},<)$.

Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an unbounded or infinite alphabet. They provide a simple formalism to specify the behaviour of reactive systems operating over data ω-words. We study the synthesis problem for specifications given as register automata over a linearly ordered data domain (e.g. (N, ≤) or (Q, ≤)), which allow for comparison of data with regards to the linear order. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately play some data, and Eve wins whenever their interaction complies with the specification, which is a language of ω-words over ordered data. Such games are however undecidable, even when the specification is recognised by a deterministic register automaton. This is in contrast with the equality case, where the problem is only undecidable for nondeterministic and universal specifications. Thus, we study one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show they are determined, and 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 ω-regular games. Lastly, we apply these results to the transducer synthesis problem for input-driven register automata, where each output data is restricted to be the content of some register, and show that if there exists an implementation, then there exists one which is a register transducer.

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 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-c) 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.

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.