Information Technology Reference
In-Depth Information
Logic-Automata Connections
for Transformations
Emmanuel Filiot
Universite Libre de Bruxelles, Brussels, Belgium
Abstract.
Pioneered by Buchi, Elgot and Trakhtenbrot, connections
between automata and logics that define languages of words and trees
are now well-established. During the last decade, some of these powerful
connections have been extended to binary relations (transformations) of
words and trees. This paper is a survey of known automata-logic con-
nections for transformations.
1
Introduction
The connections between mathematical logics and computational models have a
long research history, which goes back to the foundations of theoretical computer
science and the seminal works of Church and Turing [12,43]. In particular, Turing
has shown how to express the behaviour of a universal machine in first-order
logic, and then proved that first-order logic is undecidable, as a consequence of
the undecidability of the halting problem. The Curry-Howard isomorphism is
another important example of connection that shows correspondences between
the formulas of a logic and the types of a computational model, and between
proofs and programs [17,29].
Further connections between mathematical logic and automata theory have
been discovered in the 60
s
by Buchi [10], Elgot [20] and Trakhtenbrot [42], who
have shown that the class of finite word languages definable in monadic second-
order logic corresponds, in an effective way, to the class of languages definable by
finite state automata, and thus to regular languages. While logical formalisms
have a high-level descriptive power, automata are easier to analyse algorith-
mically. For instance, checking whether the language defined by a finite state
automaton is empty can be decided in linear-time. Therefore, as an application
of Buchi-Elgot-Trakhtenbrot's theorem, monadic second-order logic (interpreted
on finite words) has decidable satisfiability problem. Since this seminal result,
many other similar connections have been shown, most notably for regular lan-
guages of infinite words and trees [11,35,36] and first-order definable languages of
words [38]. More details can be found in the following survey: [41], [44] and [18].
A language of finite words over an alphabet
ʣ
is a mapping from the set of
words
ʣ
∗
to
.A
transformation
of finite words is a binary relation
R
on
ʣ
∗
, and therefore it generalises the concept of languages. It is
functional
if
R
{
0
,
1
}
FNRS Research Associate (
Chercheur Qualifie
).
