• Functional transductions realized by two-way 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 one-way transducer, but the given algorithm has non-elementary 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 one-way transducer, whenever it exists, in doubly or triply exponential time, again depending on whether the input transducer is sweeping or two-way. 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 second-order (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 MSO-definability of sets of rational numbers using the reals in the background. Third, we establish the MSO-definability of the set of yields induced by an MSO-definable set of trees, confirming a conjecture posed by Bruy{\`e}re, Carton, and S{\'e}nizergues.
  • We provide a wide-ranging 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 instance-level version of the problem, where both the query and the visible instance are given, and the schema-level 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 two-way 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 one-way transducer, but the given algorithm has non-elementary 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 two-way 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 second-order 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 first-order 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.