Automatic Synthesis of Systems with Data

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.

Authors

• Léo Exibard

Keywords

No keywords are indexed for this paper.