Dept of Mathematics, Computer Science, and Physics

Udine University

gabriele.puppis@uniud.it

- Formal languages
- Logics
- Databases
- Algebra

- Conference paper with S. Bose, S.N. Krishna, A. Muscholl and V. Penelle

**On Synthesis of Resynchronizers for Transducers**

In Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science (MFCS)

Leibniz International Proceedings in Informatics (LIPIcs), volume 138, pages 55:1-55:14, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex AbstractWe study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T1, T2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T1 is contained in R(T2) under the origin semantics. We show that synthesis of rational resynchronizers is decidable for functional, and even finite-valued, one-way transducers, and undecidable for relational one-way transducers. In the two-way setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous two-way transducers. For larger classes of two-way transducers, the decidability status is open. - Conference paper with A. Muscholl

**Equivalence of finite-valued streaming string transducers is decidable**

In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming (ICALP)

Leibniz International Proceedings in Informatics (LIPIcs), volume 132, pages 121:1-121:14, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex Slides AbstractIn this paper we provide a positive answer to a question left open by Alur and and Deshmukh in 2011 by showing that equivalence of finite-valued copyless streaming string transducers is decidable. - Conference paper with A. Muscholl

**The many facets of string transducers (invited paper)**

In 36th International Symposium on Theoretical Aspects of Computer Science (STACS)

Leibniz International Proceedings in Informatics (LIPIcs), volume 126, pages 2:1-2:22, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex AbstractRegular word transductions extend the robust notion of regular languages from a qualitative to a quantitative reasoning. They were already considered in early papers of formal language theory, but turned out to be much more challenging. The last decade brought considerable research around various transducer models, aiming to achieve similar robustness as for automata and languages. In this paper we survey some older and more recent results on string transducers. We present classical connections between automata, logic and algebra extended to transducers, some genuine definability questions, and review approaches to the equivalence problem.

- Conference paper with S. Bose, A. Muscholl and V. Penelle

**Origin-equivalence of two-way word transducers is in PSPACE**

In Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)

Leibniz International Proceedings in Informatics (LIPIcs), volume 122, pages 22:1-22:18, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex AbstractWe consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by non-deterministic transducers, and become decidable when restricting to functions from words to words. Here we prove that decidability can be equally recovered by adopting a slightly different, but natural semantics, called origin semantics and introduced by Bojanczyk in 2014. Specifically, we prove that the equivalence and containment problems for two-way word transducers in the origin semantics are PSPACE-complete. We also consider a variant of the containment problem where two-way transducers are compared under the origin semantics, but in a more relaxed way, by allowing distortions of the origins. The possible distortions are described by means of a resynchronization relation. We propose a logical formalism for describing a broad class of resynchronizations, while preserving the decidability of the variant of the containment problem. - Journal paper with O. Carton and T. Colcombet

**An algebraic approach to MSO-definability on countable linear orderings**

In Journal of Symbolic Logic

volume 83(3), pages 1147-1189, Association for Symbolic Logic

Pdf Bibtex AbstractWe 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ère, Carton, and Sénizergues. - Conference paper with M.E. Descotte and D. Figueira

**Resynchronizing Classes of Word Relations**

In Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP)

Leibniz International Proceedings in Informatics (LIPIcs), volume 107, pages 123:1-123:13, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex AbstractA natural approach to defining binary word relations over a finite alphabet A is through two-tape finite state automata, which can be seen as regular language L over {1,2} x A, where (i,a) is interpreted as reading letter a from tape i. Thus, a word w of the language L denotes the pair (u_1,u_2) in A* x A* in which u_i is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of Rational relations (a.k.a. non-deterministic finite state transducers), enforcing restrictions on the reading regime from the tapes, that we call synchronization, yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language onto {1,2}. In this way, for each regular language C contained in {1,2}*, one obtains a class Rel(C) of relations, such as the classes of Regular, Recognizable, or length-preserving relations, as well as (infinitely) many other classes. We study the problem of containment for synchronized classes of relations: given C,D subsets of {1,2}*, is Rel(C) contained in Rel(D)? We show a characterization in terms of C and D which gives a decidability procedure to test for class inclusion. This also yields a procedure to re-synchronize languages from {1,2} x A preserving the denoted relation whenever the inclusion holds. - Journal paper with F. Baschenis, O. Gauwin and A. Muscholl

**One-way definability of two-way word transducers**

In Logical Methods in Computer Science

volume CoRR abs/1706.01668

Pdf Bibtex AbstractFunctional 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.

- Conference paper with F. Baschenis, O. Gauwin and A. Muscholl

**Untwisting two-way transducers in elementary time**

In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

pages 1-12, IEEE Computer Society

Pdf Bibtex Slides AbstractFunctional 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. - Conference paper with P. Gallot, A. Muscholl and S. Salvati

**On the decomposition of finite-valued streaming string transducers**

In Proceedings of the 34th International Symposium on Theoretical Aspects of Computer Science (STACS)

Leibniz International Proceedings in Informatics (LIPIcs), volume 66(34), pages 1-14, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex Slides AbstractWe prove the following decomposition theorem: every 1-register streaming string transducer that associates a uniformly bounded number of outputs with each input can be effectively decomposed as a finite union of functional 1-register streaming string transducers. This theorem relies on a combinatorial result by Kortelainen concerning word equations with iterated factors. Our result implies the decidability of the equivalence problem for the considered class of transducers. This can be seen as a first step towards proving a more general decomposition theorem for streaming string transducers with multiple registers.

- Conference paper with F. Baschenis, O. Gauwin and A. Muscholl

**Minimizing resources of sweeping and streaming string transducers**

In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP)

Leibniz International Proceedings in Informatics (LIPIcs), volume 55, pages 1-14, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex Slides AbstractWe consider minimization problems for natural parameters of word transducers: the number of passes performed by two-way transducers and the number of registers used by streaming transducers. We show how to compute in ExpSpace the minimum number of passes needed to implement a transduction given as sweeping transducer, and we provide effective constructions of transducers of (worst-case optimal) doubly exponential size. We then consider streaming transducers where concatenations of registers are forbidden in the register updates. Based on a correspondence between the number of passes of sweeping transducers and the number of registers of equivalent concatenation-free streaming transducers, we derive a minimization procedure for the number of registers of concatenation-free streaming transducers. - Conference paper with M. Benedikt, P. Bourhis and B. ten Cate

**Querying Visible and Invisible Information**

In Proceedings of the 31st Annual IEEE Symposium on Logic in Computer Science (LICS)

pages 297-306, ACM

Pdf Bibtex AbstractWe provide a wide-ranging study of the scenario where a subset of the relations in the schema are visible - that is, their complete contents are known - while the remaining relations are invisible. We also have integrity constraints (invariants given by logical sentences) which may relate the visible relations to the invisible ones. We want to determine which information about a query (a positive existential sentence) can be inferred from the visible instance and the constraints. We consider both positive and negative query information, that is, whether the query or its negation holds. We consider the instance-level version of the problem, where both the query and the visible instance are given, as well as 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. - Journal paper with P. Bourhis, C. Riveros and S. Staworko

**Bounded Repairability for Regular Tree Languages**

In ACM Transactions on Database Systems

volume 41(3), pages 1-45, ACM

Pdf Bibtex AbstractWe study the problem of bounded repairability of a given restriction tree language R into a target tree language T. More precisely, we say that R is bounded repairable w.r.t. T if there exists a bound on the number of standard tree editing operations necessary to apply to any tree in R in order to obtain a tree in T. We consider a number of possible specifications for tree languages: bottom-up tree automata (on curry encoding of unranked trees) that capture the class of XML Schemas and DTDs. We also consider a special case when the restriction language R is universal, i.e., contains all trees over a given alphabet. We give an effective characterization of bounded repairability between pairs of tree languages represented with automata. This characterization introduces two tools, synopsis trees and a coverage relation between them, allowing one to reason about tree languages that undergo a bounded number of editing operations. We then employ this characterization to provide upper bounds to the complexity of deciding bounded repairability and we show that these bounds are tight. In particular, when the input tree languages are specified with arbitrary bottom-up automata, the problem is coNEXPTIME-complete. The problem remains coNEXPTIME-complete even if we use deterministic non-recursive DTDs to specify the input languages. The complexity of the problem can be reduced if we assume that the alphabet, the set of node labels, is fixed: the problem becomes PSPACE-complete for non-recursive DTDs and coNP-complete for deterministic non-recursive DTDs. Finally, when the restriction tree language R is universal, we show that the bounded repairability problem becomes EXPTIME-complete if the target language is specified by an arbitrary bottom-up tree automaton and becomes tractable (PTIME-complete, in fact) when a deterministic bottom-up automaton is used. - Journal paper with A. Manuel and A. Muscholl

**Walking on Data Words**

In Theory of Computing Systems

volume 89(2), pages 180-208, Springer

Pdf Bibtex AbstractData words are words with additional edges that connect pairs of positions carrying the same data value. We consider a natural model of automaton walking on data words, called Data Walking Automaton, and study its closure properties, expressiveness, and the complexity of some basic decision problems. Specifically, we show that the class of deterministic Data Walking Automata is closed under all Boolean operations, and that the class of non-deterministic Data Walking Automata has decidable emptiness, universality, and containment problems. We also prove that deterministic Data Walking Automata are strictly less expressive than non-deterministic Data Walking Automata, which in turn are captured by Class Memory Automata.

- Conference paper with F. Baschenis, O. Gauwin and A. Muscholl

**One-way definability of sweeping transducers**

In Proceedings of the 35th IARCS Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)

Leibniz International Proceedings in Informatics (LIPIcs), volume 45, pages 178-191, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Pdf Bibtex Slides AbstractTwo-way finite-state transducers on words are strictly more expressive than one-way transducers. It has been shown recently how to decide if a two-way functional transducer has an equivalent one-way transducer, and the complexity of the algorithm is non-elementary. We propose an alternative and simpler characterization for sweeping functional transducers, namely, for transducers that can only reverse their head direction at the extremities of the input. Our algorithm works in 2EXPSPACE and, in the positive case, produces an equivalent one-way transducer of doubly exponential size. We also show that the bound on the size of the transducer is tight, and that the one-way definability problem is undecidable for (sweeping) non-functional transducers. - Journal paper with A. Montanari and P. Sala

**A decidable weakening of Compass Logic based on cone-shaped cardinal directions**

In Logical Methods in Computer Science

volume CoRR abs/1510.03319

Pdf Bibtex AbstractWe introduce a modal logic, called Cone Logic, whose formulas describe properties of points in the plane and spatial relationships between them. Points are labelled by proposition letters and spatial relations are induced by the four cone-shaped cardinal directions. Cone Logic can be seen as a weakening of Venema's Compass Logic. We prove that, unlike Compass Logic and other projection-based spatial logics, its satisfiability problem is decidable (precisely, PSPACE-complete). We also show that it is expressive enough to capture meaningful interval temporal logics - in particular, the interval temporal logic of Allen's relations `Begins', `During', and `Later', and their transposes. - Journal paper with M. Benedikt and H. Vu

**The complexity of higher-order queries**

In Information and Computation

volume 244, pages 172-202, Springer

Pdf Bibtex AbstractHigher-order transformations are ubiquitous within data management. In relational databases, higher-order queries appear in numerous aspects including query rewriting and query specification. This work investigates languages that combine higher-order transformations with ordinary relational database query languages. We study the two most basic computational problems associated with these query languages – the evaluation problem and the containment problem. We isolate the complexity of evaluation at every order, in an analysis similar to that for that standard typed lambda calculus. We show that the containment problem (and hence, the equivalence problem) is decidable in several important subcases, particularly in the case where query constants and variables range over the positive relational operators. The main decidability result relies on techniques that differ from those used in classical query containment. We also show that the analysis of higher-order queries is closely connected to the evaluation and containment problems for non-recursive Datalog. - Journal paper with T. Colcombet and C. Ley

**Logics with Rigidly Guarded Data Tests**

In Logical Methods in Computer Science

volume CoRR abs/1410.2022

Pdf Bibtex AbstractThe 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. - Special issue with Angelo Montanari and Tiziano Villa

**Games, Automata, Logics, and Formal Verification (GandALF 2013)**

In Special issue of Information and Computation

volume 245, pages 1-2, Springer

Pdf Bibtex - Journal paper with P. Bourhis, C. Riveros and S. Staworko

**Which XML schemas are streaming bounded repairable?**

In Theory of Computing Systems

volume 57(4), pages 1250-1321, Springer

Pdf Bibtex AbstractIn this paper we consider the problem of repairing, that is, restoring validity of, documents with respect to XML schemas. We formalize this as the problem of determining, given an XML schema, whether or not a streaming procedure exists that transforms an input document so as to satisfy the XML schema, using a number of edits independent of the document. We show that this problem is decidable. In fact, we show the decidability of a more general problem, which allows the repair procedure to work on documents that are already known to satisfy another XML schema. The decision procedure relies on the analysis of the structure of an automaton model specifying the restriction and target XML schemas and reduces te problem to a novel notion of game played on pushdown systems associated with the schemas.

- Conference paper with T. Colcombet and C. Ley

**Logics with Rigidly Guarded Data Tests**

In Proceedings of the conference on Frontiers of Recognizability (FREC)

volume CoRR abs/1410.2022

Pdf Bibtex AbstractThe 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. - Conference paper with A. Montanari and P. Sala

**Decidability of the Interval Temporal Logic AA*BB* Over the Rationals**

In Proceedings of the 39th International Symposium on Mathematical Foundations of Computer Science (MFCS)

volume 8634, pages 451-463, Springer

Pdf Bibtex AbstractThe classification of the fragments of Halpern and Shoham's logic with respect to decidability/undecidability of the satisfiability problem is now very close to the end. We settle one of the few remaining questions concerning the fragment AA'BB', which comprises the Allen's interval relations 'meets' and 'begins' and their symmetric versions. We already proved that AA'BB' is decidable over the class of all finite linear orders and undecidable over ordered domains isomorphic to N. In this paper, we first show that AA'BB' is undecidable over R and over the class of all Dedekind-complete linear orders. We then prove that the logic is decidable over Q and over the class of all linear orders. - Journal paper with M. Benedikt and C. Riveros

**The Per-character Cost of Repairing Word Languages**

In Theoretical Computer Science

volume 539, pages 38-67, Elsevier Science Publishers Ltd.

Pdf Bibtex AbstractWe show how to calculate the maximum number of edits per character needed to convert any string in one regular language to a string in another language. Our algorithm makes use of a local determinization procedure applicable to a subclass of distance automata. We then show how to calculate the same property when the editing needs to be done in streaming fashion, by a finite state transducer, using a reduction to mean-payoff games. In this case, we show that the optimal streaming editor can be produced in polynomial time.

- Editorship with T. Villa

**Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification, GandALF'13**

EPTCS, volume 119

Pdf Bibtex AbstractThis 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. - Journal paper with M. Benedikt and C. Riveros

**Bounded Repairability of Word Languages**

In Journal of Computer and System Sciences

volume 79(8), pages 1302-1321, Elsevier Science Publishers Ltd.

Pdf Bibtex AbstractWhat do you do if a computational object (e.g. program trace) fails a specification? An obvious approach is to perform a repair: modify the object minimally to get something that satisfies the constraints. This approach has been investigated in the database community, for integrity constraints, and in the AI community for propositional logics. Here we study how difficult it is to repair a document in the form of a string. Specifically, we consider number of edits that must be applied to an input string in order to satisfy a given target language. This number may be unbounded; our main contribution is to isolate the complexity of the bounded repair problem based on a characterization of the regular languages that admit bounded repair. We consider the settings where the repair strategy is unconstrained and when the editing must be produced in a streaming way, i.e. by a letter-to-letter transducer. - Conference paper with A. Manuel and A. Muscholl

**Walking on Data Words**

In Proceedings of the 8th International Computer Science Symposium in Russia (CSR)

pages 64-75, Springer

Pdf Bibtex Slides AbstractWe see data words as sequences of letters with additional edges that connect pairs of positions carrying the same data value. We consider a natural model of automaton walking on data words, called Data Walking Automaton, and study its closure properties, expressiveness, and the complexity of paradigmatic problems. We prove that deterministic DWA are strictly included in non-deterministic DWA, that the former subclass is closed under all boolean operations, and that the latter class enjoys a decidable containment problem. - Conference paper with P. Bourhis and C. Riveros

**Which DTDs are Streaming Bounded Repairable?**

In Proceedings of the 16th International Conference on Database Theory (ICDT)

pages 57-68, ACM

Pdf Bibtex AbstractIntegrity constraint management concerns both checking whether data is valid and taking action to restore correctness when invalid data is discovered. In XML the notion of valid data can be captured by schema languages such as Document Type Definitions (DTDs) and more generally XML schemas. DTDs have the property that constraint checking can be done in streaming fashion. In this paper we consider when the corresponding action to restore validity - repair - can be done in streaming fashion. We formalize this as the problem of determining, given a DTD, whether or not a streaming procedure exists that transforms an input document so as to satisfy the DTD, using a number of edits independent of the document. We show that this problem is decidable. In fact, we show the decidability of a more general problem, allowing a more general class of schemas than DTDs, and requiring a repair procedure that works only for documents that are already known to satisfy another class of constraints. The decision procedure relies on a new analysis of the structure of DTDs, reducing to a novel notion of game played on pushdown systems associated with the schemas.

- Conference paper with C. Riveros and S. Staworko

**Bounded Repairability for Regular Tree Languages**

In Proceedings of the 15th International Conference on Database Theory (ICDT)

pages 155-168, ACM

Pdf Bibtex Slides AbstractWe consider the problem of repairing unranked trees (e.g., XML documents) satisfying a given restriction specification R (e.g., a DTD) into unranked trees satisfying a given target specification T. Specifically, we focus on the question of whether one can get from any tree in a regular language R to some tree in another regular language T with a finite, uniformly bounded, number of edit operations (i.e., deletions and insertions of nodes). We give effective characterizations of the pairs of specifications R and T for which such a uniform bound exists, and we study the complexity of the problem under different representations of the regular tree languages (e.g., non-deterministic stepwise automata, deterministic stepwise automata, DTDs). Finally, we point out some connections with the analogous problem for regular languages of words, which was previously studied in [6].

- Conference paper with T. Colcombet and C. Ley

**On the Use of Guards for Logics with Data**

In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS)

LNCS, volume 6907, pages 243-255, Springer

Pdf Bibtex Slides AbstractThe 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 the new logic 'rigidly guarded MSO' and show that the data languages definable in this logic are exactly those recognizable by orbit finite data monoids. We also establish, following this time the approach of Schutzenberger, McNaughton and Papert, that the first-order variant of this logic defines exactly the languages recognizable by aperiodic orbit finite data monoids. Finally, we give a variant of the logic that captures the larger class of languages recognized by non-deterministic finite memory automata. - Conference paper with M. Benedikt and C. Riveros

**The Cost of Traveling between Languages**

In Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP)

LNCS, volume 6756, pages 234-245, Springer

Pdf Bibtex AbstractWe show how to calculate the maximum number of edits per character needed to convert any string in one regular language to a string in another language. Our algorithm makes use of a local determinization procedure applicable to a subclass of distance automata. We then show how to calculate the same property when the editing needs to be done in streaming fashion, by a finite state transducer, using a reduction to mean-payoff games. We show that the optimal streaming editor can be produced in polynomial time. - Conference paper with O. Carton and T. Colcombet

**Regular Languages of Words over Countable Linear Orderings**

In Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP)

LNCS, volume 6756, pages 125-136, Springer

Pdf Bibtex Slides AbstractWe develop an algebraic model for recognizing languages of words indexed by countable linear orderings. This notion of recognizability is effectively equivalent to definability in monadic second-order (MSO) logic. The proofs also imply the first known collapse result for MSO logic over countable linear orderings. - Conference paper with M. Benedikt and C. Riveros

**Regular Repair of Specifications**

In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS)

pages 335-344, IEEE Computer Society

Pdf Bibtex Slides AbstractWhat do you do if a computational object (e.g. program trace) fails a specification? An obvious approach is to perform repair: modify the object minimally to get something that satisfies the constraints. In this paper we study repair of temporal constraints, given as automata or temporal logic formulas. We focus on determining the number of repairs that must be applied to a word satisfying a given input constraint in order to ensure that it satisfies a given target constraint. This number may well be unbounded; one of our main contributions is to isolate the complexity of the 'bounded repair problem', based on a characterization of the pairs of regular languages that admit such a repair. We consider this in the setting where the repair strategy is unconstrained and also when the strategy is restricted to use finite memory. Although the streaming setting is quite different from the general setting, we find that there are surprising connections between streaming and non-streaming, as well as within variants of the streaming problem.

- Conference paper with M. Benedikt and C. Ley

**Automata vs. Logics on Data Words**

In Proceedings of the 19th Annual Conference on Computer Science Logic (CSL)

LNCS, volume 6247, pages 110-124, Springer

Pdf Bibtex AbstractThe relationship between automata and logics has been investigated since the 1960s. In particular, it was shown how to determine, given an automaton, whether or not it is definable in first-order logic with label tests and the order relation, and for first-order logic with the successor relation. In recent years, there has been much interest in languages over an infinite alphabet. Kaminski and Francez introduced a class of automata called finite memory automata (FMA), that represent a natural analog of finite state machines. A FMA can use, in addition to its control state, a (bounded) number of registers to store and compare values from the input word. The class of data languages recognized by FMA is incomparable with the class of data languages defined by first-order formulas with the order relation and an additional binary relation for data equality. We first compare the expressive power of several variants of FMA with several data word logics. Then we consider the corresponding decision problem: given an automaton A and a logic, can the language recognized by A be defined in the logic? We show that it is undecidable for several variants of FMA, and then investigate the issue in detail for deterministic FMA. We show the problem is decidable for first-order logic with local data comparisons - an analog of first-order logic with successor. We also show instances of the problem for richer classes of first-order logic that are decidable. - Conference paper with A. Montanari and P. Sala

**Maximal Decidable Fragments of Halpern and Shoham's Modal Logic of Intervals**

In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP)

LNCS, volume 6199, pages 345-356, Springer

Pdf Bibtex AbstractIn this paper, we focus our attention on the fragment of Halpern and Shoham's modal logic of intervals (HS) that features four modal operators corresponding to the relations 'meets', 'met by', 'begun by', and 'begins' of Allen's interval algebra (AA'BB' logic). AA'BB' properly extends interesting interval temporal logics recently investigated in the literature, such as the logic BB' of Allen's 'begun by/begins' relations and propositional neighborhood logic AA', in its many variants (including metric ones). We prove that the satisfiability problem for AA'BB', interpreted over finite linear orders, is decidable, but not primitive recursive (as a matter of fact, AA'BB' turns out to be maximal with respect to decidability). Then, we show that it becomes undecidable when AA'BB' is interpreted over classes of linear orders that contains at least one linear order with an infinitely ascending sequence, thus including the natural time flows N, Z, and R. - Conference paper with M. Benedikt and C. Ley

**What You Must Remember When Processing Data Words**

In Proceedings of the 4th Alberto Mendelzon International Workshop on Foundations of Data Management (AMW)

CEUR Workshop Proceedings, volume 619, CEUR-WS.org

Pdf Bibtex AbstractWe provide a Myhill-Nerode-like theorem that characterizes the class of data languages recognized by deterministic finite-memory automata (DMA). As a byproduct of this characterization result, we obtain a canonical representation for any DMA-recognizable language. We then show that this canonical automaton is minimal in a strong sense: it has the minimal number of control states and also the minimal amount of internal storage. - Conference paper with M. Benedikt and H. Vu

**Positive Higher-order Queries**

In Proceedings of the 29th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS)

pages 27-38, ACM

Pdf Bibtex AbstractWe investigate a higher-order query language that embeds operators of the positive relational algebra within the simply-typed lambda calculus. Our language allows one to succinctly define ordinary positive relational algebra queries (conjunctive queries and unions of conjunctive queries) and, in addition, second-order query functionals, which allow the transformation of CQs and UCQs in a generic (i.e., syntax-independent) way. We investigate the equivalence and containment problems for this calculus, which subsumes traditional CQ/UCQ containment. Query functionals are said to be equivalent if the output queries are equivalent, for each possible input query, and similarly for containment. These notions of containment and equivalence depend on the class of (ordinary relational algebra) queries considered. We show that containment and equivalence are decidable when query variables are restricted to positive relational algebra and we identify the precise complexity of the problem. We also identify classes of functionals where containment is tractable. Finally, we provide upper bounds to the complexity of the containment problem when functionals act over other classes. - Book

**Automata for Branching and Layered Temporal Structures: an investigation into regularities of infinite transition systems**

FoLLI LNAI Monograph, volume 5955, Springer

Pdf Bibtex AbstractThis manuscript is a revised version of the PhD Thesis I wrote under the supervision of Prof. Angelo Montanari at Udine University. The leitmotif underlying the results herein provided is that, given any infinite complex system (e.g., a computer program) to be verified against a finite set of properties, there often exists a simpler system that satisfies the same properties and, in addition, presents strong regularities (e.g., periodicity) in its structure. Those regularities can then be exploited to decide, in an effective way, which property is satisfied by the system and which is not. Perhaps the most natural and effective way to deal with inherent regularities of infinite systems is through the notion of finite-state automaton. Intuitively, a finite-state automaton is an abstract machine with only a bounded amount of memory at its disposal, which processes an input (e.g., a sequence of symbols) and eventually outputs true or false, depending on the way the machine was designed and on the input itself. The present book focuses precisely on automaton-based approaches that ease the representation of and the reasoning on properties of infinite complex systems. The most simple notion of finite-state automaton, is that of single-string automaton. Such a device outputs true on a single (finite or infinite) sequence of symbols and false on any other sequence. We will show how single-string automata processing infinite sequences of symbols can be successfully applied in various frameworks for temporal representation and reasoning. In particular, we will use them to model single ultimately periodic time granularities, namely, temporal structures that are left-bounded and that, ultimately, periodically group instants of the underlying temporal domain (a simple example of such a structure is given by the partitioning of the temporal domain of days into weeks). The notion of single-string automaton can be further refined by introducing counters in order to compactly represent repeated occurrences of the same subsequence in the given input. By introducing restricted policies of counter update and by exploiting suitable abstractions of the configuration space for the resulting class of automata, we will devise efficient algorithms for reasoning on quasi-periodic time granularities (e.g., the partitioning of the temporal domain of days into years). Similar abstractions can be used when reasoning on infinite branching (temporal) structures. In such a case, one has to consider a generalized notion of automaton, which is able to process labeled branching structures (hereafter called trees), rather than linear sequences of symbols. We will show that sets of trees featuring the same properties can be identified with the equivalence classes induced by a suitable automaton. More precisely, given a property to be verified, one can first define a corresponding automaton that accepts all and only the trees satisfying that property, then introduce a suitable equivalence relation that refines the standard language equivalence and groups all trees being indistinguishable by the automaton, and, finally, exploit such an equivalence to reduce several instances of the verification problem to equivalent simpler instances, which can be eventually decided. - Conference paper with A. Montanari, P. Sala and G. Sciavicco

**Decidability of the Interval Temporal Logic ABB* Over the Natural Numbers**

In Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science (STACS)

Leibniz International Proceedings in Informatics (LIPIcs), volume 5, pages 597-608, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik

Pdf Bibtex AbstractIn this paper, we focus our attention on the interval temporal logic of the Allen's relations 'meets', 'begins', and 'begun by' (ABB' for short), interpreted over natural numbers. We first introduce the logic and we show that it is expressive enough to model distinctive interval properties, such as accomplishment conditions, to capture basic modalities of point-based temporal logic, such as the until operator, and to encode relevant metric constraints. Then, we prove that the satisfiability problem for ABB' over natural numbers is decidable by providing a small model theorem based on an original contraction method. Finally, we prove the EXPSPACE-completeness of the problem.

- Conference paper with A. Montanari and P. Sala

**A Decidable Spatial Logic with Cone-shaped Cardinal Directions**

In Proceedings of the 18th Annual Conference on Computer Science Logic (CSL)

LNCS, volume 5771, pages 394-408, Springer

Pdf Bibtex Slides AbstractWe introduce a spatial modal logic based on cone-shaped cardinal directions over the rational plane and we prove that, unlike projection-based ones, such as, for instance, Compass Logic, its satisfiability problem is decidable (PSPACE-complete). We also show that it is expressive enough to subsume meaningful interval temporal logics, thus generalizing previous results in the literature, e.g., its decidability implies that of the subinterval/superinterval temporal logic interpreted over the rational line. - Journal paper with D. Bresolin and A. Montanari

**A Theory of Ultimately Periodic Languages and Automata With an Application to Time Granularity**

In Acta Informatica

volume 46(5), pages 331-360, Springer

Pdf Bibtex AbstractIn this paper, we develop a theory of regular omega-languages that consist of ultimately periodic words only and we provide it with an automaton-based characterization. The resulting class of automata, called Ultimately Periodic Automata (UPA), is a subclass of the class of Büchi automata and inherits some properties of automata over finite words (NFA). Taking advantage of the similarities among UPA, Buchi automata, and NFA, we devise efficient solutions to a number of basic problems for UPA, such as the inclusion, the equivalence, and the size optimization problems. The original motivation for developing a theory of ultimately periodic languages and automata was to represent and to reason about sets of time granularities in knowledge-based and database systems. In the last part of the paper, we show that UPA actually allow one to represent (possibly infinite) sets of granularities, instead of single ones, in a compact and suitable to algorithmic manipulation way. In particular, we describe an application of UPA to a concrete time granularity scenario taken from clinical medicine.

- Conference paper with A. Montanari

**A Contraction Method to Decide MSO Theories of Deterministic Trees**

In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS)

pages 141-150, IEEE Computer Society

Pdf Bibtex Slides Other slides AbstractIn this paper we generalize the contraction method, originally proposed by Elgot and Rabin and later extended by Carton and Thomas, from labeled linear orderings to colored deterministic trees. The method we propose rests on a suitable notion of indistinguishability of trees with respect to tree automata that allows us to reduce a number of instances of the acceptance problem for tree automata to decidable instances involving regular trees. We prove that such a method works effectively for a large class of trees, which is closed under noticeable operations and includes all the deterministic trees of the Caucal hierarchy obtained via unfoldings and inverse finite mappings as well as several trees outside such a hierarchy. - Conference paper with U. Dal Lago and A. Montanari

**On the Equivalence of Automaton-Based Representations of Time Granularities**

In Proceedings of the 14th International Symposium on Temporal Representation and Reasoning (TIME)

pages 82-93, IEEE Computer Society

Pdf Bibtex Slides AbstractA time granularity can be viewed as the partitioning of a temporal domain in groups of elements, where each group is perceived as an indivisible unit. In this paper we explore an automaton-based approach to the management of time granularity that compactly represents time granularities as single-string automata with counters, that is, Buchi automata, extended with counters, that accept a single infinite word. We focus our attention on the equivalence problem for the class of restricted labeled single-string automata (RLA for short). The equivalence problem for RLA is the problem of establishing whether two given RLA represent the same time granularity. The main contribution of the paper is the reduction of the (non-)equivalence problem for RLA to the satisfiability problem for linear diophantine equations with bounds on variables. Since the latter problem has been shown to be NP-complete, we have that the RLA equivalence problem is in co-NP. - Journal paper with U. Dal Lago and A. Montanari

**Compact and Tractable Automaton-based Representations for Time Granularities**

In Theoretical Computer Science

volume 373(1-2), pages 115-141, Elsevier Science Publishers Ltd.

Pdf Bibtex AbstractMost approaches to time granularity proposed in the literature are based on algebraic and logical formalisms [11]. Here we follow an alternative automaton-based approach, originally outlined in [7], which makes it possible to deal with infinite time granularities in an effective and efficient way. Such an approach provides a neat solution to fundamental algorithmic problems, such as the granularity equivalence and granule conversion problems, which have been often neglected in the literature. In this paper, we focus our attention on two basic optimization problems for the automaton-based representation of time granularities, namely, the problem of computing the smallest representation of a time granularity and that of computing the most tractable representation of it, that is, the one on which crucial algorithms, such as granule conversion algorithms, run fastest.

- Journal paper with A. Montanari and A. Peron

**On the Relationships Between Theories of Time Granularity and the Monadic Second-order Theory of One Successor**

In Journal of Applied Non-Classical Logics

volume 16(3-4), pages 433-455, Oxford University Press

Pdf Bibtex AbstractIn this paper we explore the connections between the monadic second-order theory of one successor (MSO for short) and the theories of omega-layered structures for time granularity. We first prove that the decision problem for MSO and that for a suitable first-order theory of the upward unbounded layered structure are inter-reducible. Then, we show that a similar result holds for suitable chain variants of the MSO theory of the totally unbounded layered structure (this allows us to solve some decision problems about theories of time granularity left open by Franceschet et al. [FRA 06]).

- Conference paper with A. Montanari

**Decidability of the Theory of the Totally Unbounded omega-Layered Structure**

In Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME)

pages 156-160, IEEE Computer Society

Pdf Bibtex Slides AbstractIn this paper, we address the decision problem for a system of monadic second-order logic interpreted over an omega-layered temporal structure devoid of both a finest layer and a coarsest one (we call such a structure totally unbounded). We propose an automaton-theoretic method that solves the problem in two steps: first, we reduce the considered problem to the problem of determining, for any given Rabin tree automaton, whether it accepts a fixed vertex-colored tree; then, we exploit a suitable notion of tree equivalence to reduce the latter problem to the decidable case of regular trees. - Conference paper with A. Montanari

**Decidability of MSO Theories of Tree Structures**

In Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)

LNCS, volume 3328, pages 430-442, Springer

Pdf Bibtex Slides AbstractIn this paper we provide an automaton-based solution to the decision problem for a large set of monadic second-order theories of deterministic tree structures. We achieve it in two steps: first, we reduce the considered problem to the problem of determining, for any Rabin tree automaton, whether it accepts a given tree; then, we exploit a suitable notion of tree equivalence to reduce (a number of instances of) the latter problem to the decidable case of regular trees. We prove that such a reduction works for a large class of trees, that we call residually regular trees. We conclude the paper with a short discussion of related work. - Conference paper with D. Bresolin and A. Montanari

**Time Granularities and Ultimately Periodic Automata**

In Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA)

LNCS, volume 3229, pages 513-525, Springer

Pdf Bibtex Slides AbstractThe relevance of the problem of managing periodic phenomena is widely recognized in the area of knowledge representation and reasoning. One of the most effective attempts at dealing with this problem has been the addition of a notion of time granularity to knowledge representation systems. Different formalizations of such a notion have been proposed in the literature, following algebraic, logical, string-based, and automaton-based approaches. In this paper, we focus our attention on the automaton-based one, which allows one to represent a large class of granularities in a compact and suitable to algorithmic manipulation form. We further develop such an approach to make it possible to deal with (possibly infinite) sets of granularities instead of single ones. We define a new class of automata, called Ultimately Periodic Automata, we give a characterization of their expressiveness, and we show how they can be used to encode and to solve a number of fundamental problems, such as the membership problem, the equivalence problem, and the problem of granularity comparison. Moreover, we give an example of their application to a concrete problem taken from clinical medicine.

- Conference paper with U. Dal Lago and A. Montanari

**Towards Compact and Tractable Automaton-based Representations of Time Granularity**

In Proceedings of the 8th International Conference on Theoretical Computer Science (ICTCS)

LNCS, volume 2841, pages 72-85, Springer

Pdf Bibtex Slides AbstractDifferent approaches to time granularity have been proposed in the database literature to formalize the notion of calendar, based on algebraic, logical, and string-based formalisms. In this paper, we further develop an alternative approach based on automata, originally proposed in [4], which makes it possible to deal with infinite time granularities in an effective (and efficient) way. In particular, such an approach provides an effective solution to fundamental problems such as equivalence and conversion of time granularities. We focus our attention on two kinds of optimization problems for automaton-based representations, namely, computing the smallest representation and computing the most tractable representation, that is, the one on which crucial algorithms (e.g., granule conversion algorithms) run fastest. We first introduce and compare these two minimization problems; then, we give a polynomial time algorithm that solves the latter.

- 2019-now: Assistant Professor, Tenure Track at Udine University, Italy
- 2012-2019: CNRS researcher at LaBRI, France
- 2010-2012: Junior Research Fellowship, Linacre College Oxford, UK
- 2009-2012: Postdoc, Oxford University, UK
- 2006-2008: Postdoc, Udine University, Italy
- 2006: PhD in CS, Udine University, Italy

- 2016: Course for PhD students at ESSLLI School on Logical Foundations of Databases (Abstract Slides part 1 part 2 part 3 part 4 part 5)
- 2015: Course for PhD students at ECI School on Logical Foundations of Databases (Abstract Slides part 1 part 2 part 3 part 4 part 5)
- 2014: Course for PhD students at Udine University on Verification of Infinite State Systems (Slides part 1 part 2 part 3 part 4 part 5 part 6)

- 2019-2023: Member of research project QUID
- 2016-2020: Member of research project DeLTA
- 2014-2018: Member of research project ExStream
- 2012-2014: Member of research project FRec

- 2020: PC member of MFCS (45th International Symposium on Mathematical Foundations of Computer Science)
- 2020: PC member of Highlights of Logic, Games, and Automata
- 2019: Invited speaker at Trends 2019 - Trends in Transformations (Slides)
- 2019: co-organizer of GandALF (10th International Symposium on Games, Automata, Logics, and Formal Verification 2019)
- 2019: PC member of ICLA (8th Indian Conference on Logic and its Applications 2019)
- 2017: PC member of ICDT (20th International Conference on Database Theory)
- 2014: PC member of TIME (21st International Symposium on Temporal Representation and Reasoning)
- 2014: PC member of PODS (33rd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems)
- 2013: PC co-chair of GandALF (4th International Symposium on Games, Automata, Logics and Formal Verification)
- 2013: PC member of WoLLIC (20th Workshop on Logic, Language, Information and Computation)
- 2012: PC member of GandALF (3rd International Symposium on Games, Automata, Logics and Formal Verification)
- 2011: PC member of GandALF (2nd International Symposium on Games, Automata, Logics and Formal Verification)
- 2010: PC member of GandALF (1st International Symposium on Games, Automata, Logics and Formal Verification)