Parameterized synthesis of subsequetial transducers from rational relations over finite words

12^th March 2019, 13:00 Ashton Lecture Theater
Sarah Winter
RWTH Aachen University

Abstract

The synthesis problem asks, given a specification that relates possible inputs to allowed outputs, whether there is a program realizing the specification, and if so, construct one.

We consider synthesis of subsequential transducers with synchronization parameters from rational relations over finite words.
A subsequential transducer is basically a deterministic finite automaton that outputs a finite word on each transition.
A word relation can be represented by a set of synchronizations, called synchronization language.
A synchronization of a pair of words is a single word where each position is annotated over {1,2}, which indicates whether it came from the input or output component, e.g., the synchronization (1a 2a 2b 1b 2a) represents the pair (ab,aba).
The decision problems that have been studied so far either ask for synthesis by a synchronous subsequential or by an arbitrary subsequential transducer.
We ask whether a subsequential transducer whose allowed input/output behavior is specified by a given synchronization language can be synthesized from a given rational relation.
The given synchronization language is referred to as synchronization parameter.

Recently, main classes of rational relations have been characterized in terms of admissible synchronization languages, and we study the above problem for different combinations of classes of rational relations and classes of synchronization languages.
The problem is undecidable in general, because it is known to be undecidable whether an arbitrary subsequential transducer can be synthesized from a rational relation.
For automatic relations (also called synchronized rational relations) it is known that it is decidable whether an arbitrary subsequential transducer or a synchronous subsequential transducer can be synthesized.
Regarding our framework, the key contribution is that it is decidable whether a subsequential transducer whose synchronization language lies within a given ``automatic'' synchronization language can be synthesized from an automatic relation.