▹  Logics 
▹  Databases 
▹  Formal languages 
▹  Data transformation 
▹  Conference paper with Finitevalued Streaming String Transducers Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Pdf Bibtex Abstract A transducer is finitevalued if for some bound k, it maps any given input to at most k outputs. For classical, oneway transducers, it is known since the 80s that finite valuedness entails decidability of the equivalence problem. This decidability result is in contrast to the general case, which makes finitevalued transducers very attractive. For classical transducers it is also known that finite valuedness is decidable and that any kvalued finite transducer can be decomposed as a union of k singlevalued finite transducers. In this paper, we extend the above results to copyless streaming string transducers (SSTs), answering questions raised by Alur and Deshmukh in 2011. SSTs strictly extend the expressiveness of oneway transducers via additional variables that store partial outputs. We prove that any kvalued SST can be effectively decomposed as a union of k (singlevalued) deterministic SSTs. As a corollary, we obtain equivalence of SSTs and twoway transducers in the finitevalued case (those two models are incomparable in general). Another corollary is an elementary upper bound for checking equivalence of finitevalued SSTs. The latter problem was already known to be decidable, but the proof complexity was unknown (it relied on Ehrenfeucht's conjecture). Finally, our main result is that finite valuedness of SSTs is decidable. The complexity is PSPACE, and even PTIME when the number of variables is fixed.

▹  Conference paper with The Logic of Prefixes and Suffixes is Elementary under Homogeneity Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Pdf Bibtex Slides Abstract In this paper, we study the finite satisfiability problem for the logic BE under the homogeneity assumption. BE is the cornerstone of Halpern and Shoham's interval temporal logic, and features modal operators corresponding to the prefix (a.k.a. Begins) and suffix (a.k.a. Ends) relations on intervals. In terms of complexity, BE lies in between the Chop logic C, whose satisfiability problem is known to be nonelementary, and the PSPACEcomplete interval logic D of the subinterval (a.k.a. During) relation. BE was shown to be EXPSPACEhard, and the only known satisfiability procedure is primitive recursive, but not elementary. Our contribution consists of tightening the complexity bounds of the satisfiability problem for BE, by proving it to be EXPSPACEcomplete. We do so by devising an equisatisfiable normal form with boundedly many nested modalities. The normalization technique resembles Scott's quantifier elimination, but it turns out to be much more involved due to the limitations enforced by the homogeneity assumption.

▹  Journal paper with Dynamic Data Structures for Timed Automata Acceptance Algorithmica
volume Pdf Bibtex Abstract We study a variant of the classical membership problem in automata theory, which consists of deciding whether a given input word is accepted by a given automaton. We do so through the lenses of parameterized dynamic data structures: we assume that the automaton is fixed and its size is the parameter, while the input word is revealed as in a stream, one symbol at a time following the natural order on positions. The goal is to design a dynamic data structure that can be efficiently updated upon revealing the next symbol, while maintaining the answer to the query on whether the word consisting of symbols revealed so far is accepted by the automaton. We provide complexity bounds for this dynamic acceptance problem for timed automata that process symbols interleaved with time spans. The main contribution is a dynamic data structure that maintains acceptance of a fixed oneclock timed automaton A with amortized update time Exp(O(A)) per input symbol.

▹  Journal paper with Inference from visible information and background knowledge ACM Transactions on Computational Logic
volume Pdf Bibtex Abstract We provide a wideranging study of the scenario where a subset of the relations in a relational vocabulary is 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—that 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 concerned with is denoted as the 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.

▹  Conference paper with Dynamic data structures for timed automata acceptance Proceedings of the 16th International Symposium on Parameterized and Exact Computation (IPEC)
Pdf Bibtex Abstract We study a variant of the classical membership problem in automata theory, which consists of deciding whether a given input word is accepted by a given automaton. We do so through the lenses of parameterized dynamic data structures: we assume that the automaton is fixed and its size is the parameter, while the input word is revealed as in a stream, one symbol at a time following the natural order on positions. The goal is to design a dynamic data structure that can be efficiently updated upon revealing the next symbol, while maintaining the answer to the query on whether the word consisting of symbols revealed so far is accepted by the automaton. We provide complexity bounds for this dynamic acceptance problem for timed automata that process symbols interleaved with time spans. The main contribution is a dynamic data structure that maintains acceptance of a fixed oneclock timed automaton A with amortized update time Exp(O(A)) per input symbol.

▹  Conference paper with Oneway Resynchronizability of Word Transducers Proceedings of the 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS)
Pdf Bibtex Abstract The origin semantics for transducers was proposed in 2014, and it led to various characterizations and decidability results that are in contrast with the classical semantics. In this paper we add a further decidability result for characterizing transducers that are close to oneway transducers in the origin semantics. We show that it is decidable whether a nondeterministic twoway word transducer can be resynchronized by a bounded, regular resynchronizer into an originequivalent oneway transducer. The result is in contrast with the usual semantics, where it is undecidable to know if a nondeterministic twoway transducer is equivalent to some oneway transducer.

▹  Conference paper with On Synthesis of Resynchronizers for Transducers Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science (MFCS)
Pdf Bibtex Abstract We 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 finitevalued, oneway transducers, and undecidable for relational oneway transducers. In the twoway setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous twoway transducers. For larger classes of twoway transducers, the decidability status is open.

▹  Conference paper with Equivalence of finitevalued streaming string transducers is decidable Proceedings of the 46th International Colloquium on Automata, Languages, and Programming (ICALP)
Pdf Bibtex Slides Abstract In this paper we provide a positive answer to a question left open by Alur and and Deshmukh in 2011 by showing that equivalence of finitevalued copyless streaming string transducers is decidable.

▹  Conference paper with The many facets of string transducers (invited paper) 36th International Symposium on Theoretical Aspects of Computer Science (STACS)
Pdf Bibtex Abstract Regular 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 Originequivalence of twoway word transducers is in PSPACE Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
Pdf Bibtex Abstract We consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by nondeterministic 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 twoway word transducers in the origin semantics are PSPACEcomplete. We also consider a variant of the containment problem where twoway 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 An algebraic approach to MSOdefinability on countable linear orderings Journal of Symbolic Logic
volume Pdf Bibtex Abstract 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ère, Carton, and Sénizergues.

▹  Conference paper with Resynchronizing Classes of Word Relations Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP)
Pdf Bibtex Abstract A natural approach to defining binary word relations over a finite alphabet A is through twotape 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 ilabelled letters. While this formalism defines the wellstudied class of Rational relations (a.k.a. nondeterministic finite state transducers), enforcing restrictions on the reading regime from the tapes, that we call synchronization, yields various subclasses 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 lengthpreserving 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 resynchronize languages from {1,2} x A preserving the denoted relation whenever the inclusion holds.

▹  Journal paper with Oneway definability of twoway word transducers Logical Methods in Computer Science
volume Pdf Bibtex Abstract 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.

▹  Conference paper with Untwisting twoway transducers in elementary time Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
pages Pdf Bibtex Slides Abstract 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.

▹  Conference paper with On the decomposition of finitevalued streaming string transducers Proceedings of the 34th International Symposium on Theoretical Aspects of Computer Science (STACS)
Pdf Bibtex Slides Abstract We prove the following decomposition theorem: every 1register streaming string transducer that associates a uniformly bounded number of outputs with each input can be effectively decomposed as a finite union of functional 1register 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 Minimizing resources of sweeping and streaming string transducers Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP)
Pdf Bibtex Slides Abstract We consider minimization problems for natural parameters of word transducers: the number of passes performed by twoway 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 (worstcase 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 concatenationfree streaming transducers, we derive a minimization procedure for the number of registers of concatenationfree streaming transducers.

▹  Conference paper with Querying Visible and Invisible Information Proceedings of the 31st Annual IEEE Symposium on Logic in Computer Science (LICS)
pages Pdf Bibtex Abstract We provide a wideranging 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 instancelevel version of the problem, where both the query and the visible instance are given, as well as the schemalevel 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 Bounded Repairability for Regular Tree Languages ACM Transactions on Database Systems
volume Pdf Bibtex Abstract We 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: bottomup 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 bottomup automata, the problem is coNEXPTIMEcomplete. The problem remains coNEXPTIMEcomplete even if we use deterministic nonrecursive 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 PSPACEcomplete for nonrecursive DTDs and coNPcomplete for deterministic nonrecursive DTDs. Finally, when the restriction tree language R is universal, we show that the bounded repairability problem becomes EXPTIMEcomplete if the target language is specified by an arbitrary bottomup tree automaton and becomes tractable (PTIMEcomplete, in fact) when a deterministic bottomup automaton is used.

▹  Journal paper with Walking on Data Words Theory of Computing Systems
volume Pdf Bibtex Abstract Data 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 nondeterministic Data Walking Automata has decidable emptiness, universality, and containment problems. We also prove that deterministic Data Walking Automata are strictly less expressive than nondeterministic Data Walking Automata, which in turn are captured by Class Memory Automata.

▹  Conference paper with Oneway definability of sweeping transducers Proceedings of the 35th IARCS Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
Pdf Bibtex Slides Abstract Twoway finitestate transducers on words are strictly more expressive than oneway transducers. It has been shown recently how to decide if a twoway functional transducer has an equivalent oneway transducer, and the complexity of the algorithm is nonelementary. 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 oneway transducer of doubly exponential size. We also show that the bound on the size of the transducer is tight, and that the oneway definability problem is undecidable for (sweeping) nonfunctional transducers.

▹  Journal paper with A decidable weakening of Compass Logic based on coneshaped cardinal directions Logical Methods in Computer Science
volume Pdf Bibtex Abstract We 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 coneshaped cardinal directions. Cone Logic can be seen as a weakening of Venema's Compass Logic. We prove that, unlike Compass Logic and other projectionbased spatial logics, its satisfiability problem is decidable (precisely, PSPACEcomplete). 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 The complexity of higherorder queries Information and Computation
volume Pdf Bibtex Abstract Higherorder transformations are ubiquitous within data management. In relational databases, higherorder queries appear in numerous aspects including query rewriting and query specification. This work investigates languages that combine higherorder 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 higherorder queries is closely connected to the evaluation and containment problems for nonrecursive Datalog.

▹  Journal paper with Logics with Rigidly Guarded Data Tests Logical Methods in Computer Science
volume Pdf Bibtex Abstract 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.

▹  with Games, Automata, Logics, and Formal Verification (GandALF 2013) Special issue of Information and Computation
volume Pdf Bibtex 
▹  Journal paper with Which XML schemas are streaming bounded repairable? Theory of Computing Systems
volume Pdf Bibtex Abstract In 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 Decidability of the Interval Temporal Logic AA*BB* Over the Rationals Proceedings of the 39th International Symposium on Mathematical Foundations of Computer Science (MFCS)
volume Pdf Bibtex Abstract The 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 Dedekindcomplete linear orders. We then prove that the logic is decidable over Q and over the class of all linear orders.

▹  Journal paper with The Percharacter Cost of Repairing Word Languages Theoretical Computer Science
volume Pdf Bibtex Abstract We 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 meanpayoff games. In this case, we show that the optimal streaming editor can be produced in polynomial time.

▹  Editorship with Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification, GandALF'13 Pdf Bibtex Abstract 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.

▹  Journal paper with Bounded Repairability of Word Languages Journal of Computer and System Sciences
volume Pdf Bibtex Abstract What 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 lettertoletter transducer.

▹  Conference paper with Walking on Data Words Proceedings of the 8th International Computer Science Symposium in Russia (CSR)
pages Pdf Bibtex Slides Abstract We 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 nondeterministic DWA, that the former subclass is closed under all boolean operations, and that the latter class enjoys a decidable containment problem.

▹  Conference paper with Which DTDs are Streaming Bounded Repairable? Proceedings of the 16th International Conference on Database Theory (ICDT)
pages Pdf Bibtex Abstract Integrity 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 Bounded Repairability for Regular Tree Languages Proceedings of the 15th International Conference on Database Theory (ICDT)
pages Pdf Bibtex Slides Abstract We 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., nondeterministic 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 On the Use of Guards for Logics with Data Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS)
Pdf Bibtex Slides Abstract 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 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 firstorder 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 nondeterministic finite memory automata.

▹  Conference paper with The Cost of Traveling between Languages Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP)
Pdf Bibtex Abstract We 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 meanpayoff games. We show that the optimal streaming editor can be produced in polynomial time.

▹  Conference paper with Regular Languages of Words over Countable Linear Orderings Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP)
Pdf Bibtex Slides Abstract We 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 secondorder (MSO) logic. The proofs also imply the first known collapse result for MSO logic over countable linear orderings.

▹  Conference paper with Regular Repair of Specifications Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS)
pages Pdf Bibtex Slides Abstract What 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 nonstreaming, as well as within variants of the streaming problem.

▹  Conference paper with Automata vs. Logics on Data Words Proceedings of the 19th Annual Conference on Computer Science Logic (CSL)
Pdf Bibtex Abstract The 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 firstorder logic with label tests and the order relation, and for firstorder 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 firstorder 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 firstorder logic with local data comparisons  an analog of firstorder logic with successor. We also show instances of the problem for richer classes of firstorder logic that are decidable.

▹  Conference paper with Maximal Decidable Fragments of Halpern and Shoham's Modal Logic of Intervals Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP)
Pdf Bibtex Abstract In 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 What You Must Remember When Processing Data Words Proceedings of the 4th Alberto Mendelzon International Workshop on Foundations of Data Management (AMW)
Pdf Bibtex Abstract We provide a MyhillNerodelike theorem that characterizes the class of data languages recognized by deterministic finitememory automata (DMA). As a byproduct of this characterization result, we obtain a canonical representation for any DMArecognizable 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 Positive Higherorder Queries Proceedings of the 29th ACM SIGMODSIGACTSIGART Symposium on Principles of Database Systems (PODS)
pages Pdf Bibtex Abstract We investigate a higherorder query language that embeds operators of the positive relational algebra within the simplytyped lambda calculus. Our language allows one to succinctly define ordinary positive relational algebra queries (conjunctive queries and unions of conjunctive queries) and, in addition, secondorder query functionals, which allow the transformation of CQs and UCQs in a generic (i.e., syntaxindependent) 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 Pdf Bibtex Abstract This 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 finitestate automaton. Intuitively, a finitestate 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 automatonbased approaches that ease the representation of and the reasoning on properties of infinite complex systems. The most simple notion of finitestate automaton, is that of singlestring 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 singlestring 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 leftbounded 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 singlestring 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 quasiperiodic 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 Decidability of the Interval Temporal Logic ABB* Over the Natural Numbers Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science (STACS)
Pdf Bibtex Abstract In 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 pointbased 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 EXPSPACEcompleteness of the problem.

▹  Conference paper with A Decidable Spatial Logic with Coneshaped Cardinal Directions Proceedings of the 18th Annual Conference on Computer Science Logic (CSL)
Pdf Bibtex Slides Abstract We introduce a spatial modal logic based on coneshaped cardinal directions over the rational plane and we prove that, unlike projectionbased ones, such as, for instance, Compass Logic, its satisfiability problem is decidable (PSPACEcomplete). 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 A Theory of Ultimately Periodic Languages and Automata With an Application to Time Granularity Acta Informatica
volume Pdf Bibtex Abstract In this paper, we develop a theory of regular omegalanguages that consist of ultimately periodic words only and we provide it with an automatonbased 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 knowledgebased 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 Contraction Method to Decide MSO Theories of Deterministic Trees Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS)
pages Pdf Bibtex Slides Other slides Abstract In 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 On the Equivalence of AutomatonBased Representations of Time Granularities Proceedings of the 14th International Symposium on Temporal Representation and Reasoning (TIME)
pages Pdf Bibtex Slides Abstract A 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 automatonbased approach to the management of time granularity that compactly represents time granularities as singlestring 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 singlestring 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 NPcomplete, we have that the RLA equivalence problem is in coNP.

▹  Journal paper with Compact and Tractable Automatonbased Representations for Time Granularities Theoretical Computer Science
volume Pdf Bibtex Abstract Most approaches to time granularity proposed in the literature are based on algebraic and logical formalisms [11]. Here we follow an alternative automatonbased 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 automatonbased 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 On the Relationships Between Theories of Time Granularity and the Monadic Secondorder Theory of One Successor Journal of Applied NonClassical Logics
volume Pdf Bibtex Abstract In this paper we explore the connections between the monadic secondorder theory of one successor (MSO for short) and the theories of omegalayered structures for time granularity. We first prove that the decision problem for MSO and that for a suitable firstorder theory of the upward unbounded layered structure are interreducible. 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 Decidability of the Theory of the Totally Unbounded omegaLayered Structure Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME)
pages Pdf Bibtex Slides Abstract In this paper, we address the decision problem for a system of monadic secondorder logic interpreted over an omegalayered temporal structure devoid of both a finest layer and a coarsest one (we call such a structure totally unbounded). We propose an automatontheoretic 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 vertexcolored 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 Decidability of MSO Theories of Tree Structures Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
Pdf Bibtex Slides Abstract In this paper we provide an automatonbased solution to the decision problem for a large set of monadic secondorder 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 Time Granularities and Ultimately Periodic Automata Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA)
Pdf Bibtex Slides Abstract The 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, stringbased, and automatonbased approaches. In this paper, we focus our attention on the automatonbased 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 Towards Compact and Tractable Automatonbased Representations of Time Granularity Proceedings of the 8th International Conference on Theoretical Computer Science (ICTCS)
Pdf Bibtex Slides Abstract Different approaches to time granularity have been proposed in the database literature to formalize the notion of calendar, based on algebraic, logical, and stringbased 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 automatonbased 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.

2022  present  Associate Professor at Udine University 
2019  2022  Tenuretrack researcher at Udine University 
2012  2019  Tenured CNRS researcher at LaBRI, Bordeaux 
2009  2012  Postdoc at Oxford University 
2006  2008  Postdoc at Udine University 
2002  2006  Doctorand in Computer Science at Udine University 
2016 
Logical Foundations of Databases (with Diego Figueira)
ESSLLI  European Summer School in Logic, Language and Information Slides
part 1part 2part 3part 4part 5

2015 
Introduction to Logical Foundations of Databases (with Diego Figueira)
ECI  Escuela de Ciencias Informáticas Slides
part 1part 2part 3part 4part 5

2015 
Techniques for Verification of Infinite State Systems
Dept. of Mathematics, Computer Science, and Physics of Udine University Slides
part 1part 2part 3part 4part 5part 6

2006 
Verification of Infinite State Systems ESSLLI  European Summer School in Logic, Language and Information Slides
part 1part 2part 3part 4part 5part 6part 7

▹ 
Distributed Systems 

2023  2024 
Slides Link to Microsoft Teams


2022  2023 
Slides Link to Microsoft Teams


2021  2022 
Slides Link to Microsoft Teams


2020  2021 
Slides Link to Microsoft Teams


2019  2020  Slides  
▹ 
Algorithms and Data Structures 

2023  2024  Link to Moodle 

2022  2023  Link to Moodle 

2021  2022  Link to Moodle 

2020  2021  Link to Moodle 

2019  2020  Link to Moodle 

▹ 
Verification and Validation techniques in AI and Cybersecurity 

2023  2024 
Slides Link to Microsoft Teams


2022  2023 
Slides Link to Microsoft Teams


2021  2022 
Slides Link to Microsoft Teams


2020  2021 
Slides Link to Microsoft Teams


▹ 
Introduction to Distributed Systems 

2022  2023 
Slides Link to Microsoft Teams


▹ 
Automatic verification of systems: theory and applications 

2019  2020 
Slides Link to Microsoft Teams


2021  Dagstuhl seminar
Unambiguity in automata theory Slides 
2019  Workshop
Trends in Transformations Slides 
2018  Workshop The theory of regular cost functions and beyond 
2015  Workshop
ACTS  Automata, Concurrency and Timed Systems Slides 
2015  Conference
FRec  Frontiers of Recognizability Slides 
2023 
Member of the organizing committee of the 3rd edition of the summer school on
Formal Methods for CyberPhysical Systems

2023 
Member of the organizing committee of
GandALF14th international symposium on Games, Automata, Logics, and Formal Verification 
2022 
Member of the organizing committee of
AIxIA21st international conference of the Italian Association for Artificial Intelligence 
2019 
Member of the organizing committee of
GandALF10th international symposium on Games, Automata, Logics, and Formal verification 
2016 
Member of the organizing committee of
EDBT/ICDT19th international conference on Extending Database Technology and 19th International Conference on Database Theory 
2009 
Member of the organizing committee of
GAMESInternational workshop of the ESF Research Networking Programme on Games for design and verification 
2023 
PC member of
GandALF

2022 
PC member of
RP

2022 
PC member of
ICTCS

2021 
PC member of
MOVEP

2021 
PC member of
OVERLAY

2020 
PC member of
MFCS

2020 
PC member of
Highlights

2019 
PC member of
ICLA

2017 
PC member of
ICDT

2014 
PC member of
PODS

2014 
PC member of
TIME

2013 
PC cochair, with Tiziano Villa, of
GandALF

2013 
PC member of
WoLLIC

2012 
PC member of
GandALF

2011 
PC member of
GandALF

2010 
PC member of
GandALF

2019  2023 
Member of the research project
QUIDResearch project on Efficient Querying for Incomplete and Inconsistent Data, funded by ANR  Agence Nationale de la Recherche 
2016  2020 
Member of the research project
DeLTAResearch project on Défis pour la Logique, les Transducteurs et les Automates, funded by ANR  Agence Nationale de la Recherche 
2014  2018 
Member of the research project
ExStreamResearch project on Extensions of Stream processing, funded by ANR  Agence Nationale de la Recherche 
2015  2017 
Member of the research project
FoGResearch project on Foundations of Graph Structured Data, funded by STICAmSud (cooperation programme between France and South American countries) 
2012  2014 
Member of the research project
FRecResearch project on Frontiers of Recognizability, funded by ANR  Agence Nationale de la Recherche 