
Functional transductions realized by twoway transducers (or, equally, by
streaming transducers or MSO transductions) are the natural and standard notion
of "regular" mappings from words to words. It was shown in 2013 that it is
decidable if such a transduction can be implemented by some oneway transducer,
but the given algorithm has nonelementary complexity. We provide an algorithm
of different flavor solving the above question, that has doubly exponential
space complexity. In the special case of sweeping transducers the complexity is
one exponential less. We also show how to construct an equivalent oneway
transducer, whenever it exists, in doubly or triply exponential time, again
depending on whether the input transducer is sweeping or twoway. In the
sweeping case our construction is shown to be optimal.

We develop an algebraic notion of recognizability for languages of words
indexed by countable linear orderings. We prove that this notion is effectively
equivalent to definability in monadic secondorder (MSO) logic. We also provide
three logical applications. First, we establish the first known collapse result
for the quantifier alternation of MSO logic over countable linear orderings.
Second, we solve an open problem posed by Gurevich and Rabinovich, concerning
the MSOdefinability of sets of rational numbers using the reals in the
background. Third, we establish the MSOdefinability of the set of yields
induced by an MSOdefinable set of trees, confirming a conjecture posed by
Bruy{\`e}re, Carton, and S{\'e}nizergues.

We provide a wideranging study of the scenario where a subset of the
relations in a relational vocabulary are visible to a user  that is, their
complete contents are known  while the remaining relations are invisible. We
also have a background theory  invariants given by logical sentences 
which may relate the visible relations to invisible ones, and also may
constrain both the visible and invisible relations in isolation. We want to
determine whether some other information, given as a positive existential
formula, can be inferred using only the visible information and the background
theory. This formula whose inference we are concered with is denoted as the
\emph{query}. We consider whether positive information about the query can be
inferred, and also whether negative information  the sentence does not hold
 can be inferred. We further consider both the instancelevel version of the
problem, where both the query and the visible instance are given, and the
schemalevel version, where we want to know whether truth or falsity of the
query can be inferred in some instance of the schema.

Functional transductions realized by twoway transducers (equivalently, by
streaming transducers and by MSO transductions) are the natural and standard
notion of "regular" mappings from words to words. It was shown recently
(LICS'13) that it is decidable if such a transduction can be implemented by
some oneway transducer, but the given algorithm has nonelementary complexity.
We provide an algorithm of different flavor solving the above question, that
has double exponential space complexity. We further apply our technique to
decide whether the transduction realized by a twoway transducer can be
implemented by a sweeping transducer, with either known or unknown number of
passes.

The notion of orbit finite data monoid was recently introduced by Bojanczyk
as an algebraic object for defining recognizable languages of data words.
Following Buchi's approach, we introduce a variant of monadic secondorder
logic with data equality tests that captures precisely the data languages
recognizable by orbit finite data monoids. We also establish, following this
time the approach of Schutzenberger, McNaughton and Papert, that the
firstorder fragment of this logic defines exactly the data languages
recognizable by aperiodic orbit finite data monoids. Finally, we consider
another variant of the logic that can be interpreted over generic structures
with data. The data languages defined in this variant are also recognized by
unambiguous finite memory automata.

This volume contains the proceedings of the Fourth International Symposium on
Games, Automata, Logic and Formal Verification (GandALF 2013). The symposium
took place in Borca di Cadore, Italy, from 29th to 31st of August 2013.
The proceedings of the symposium contain the abstracts of three invited talks
and 17 papers that were accepted after a careful evaluation for presentation at
the conference. The topics of the accepted papers range over a wide spectrum,
including algorithmic and behavioral game theory, game semantics, formal
languages and automata theory, modal and temporal logics, software
verification, hybrid systems.