-
Finite-valued Streaming String Transducers
Authors:
Emmanuel Filiot,
Ismaël Jecker,
Christof Löding,
Anca Muscholl,
Gabriele Puppis,
Sarah Winter
Abstract:
A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way 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 finite-valued transducers very attractive. For classical transducers, it is also known that fini…
▽ More
A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way 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 finite-valued transducers very attractive. For classical transducers, it is also known that finite valuedness is decidable and that any k-valued finite transducer can be decomposed as a union of k single-valued 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 one-way transducers via additional variables that store partial outputs. We prove that any k-valued SST can be effectively decomposed as a union of k (single-valued) deterministic SSTs. As a corollary, we obtain equivalence of SSTs and two-way transducers in the finite-valued case (those two models are incomparable in general). Another corollary is an elementary upper bound for checking equivalence of finite-valued 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.
△ Less
Submitted 12 May, 2025; v1 submitted 13 May, 2024;
originally announced May 2024.
-
The Logic of Prefixes and Suffixes is Elementary under Homogeneity
Authors:
Dario Della Monica,
Angelo Montanari,
Gabriele Puppis,
Pietro Sala
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…
▽ More
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 non-elementary, and the PSPACE-complete interval logic D of the sub-interval (a.k.a. "During") relation. BE was shown to be EXPSPACE-hard, 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 EXPSPACE-complete. We do so by devising an equi-satisfiable 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.
△ Less
Submitted 22 April, 2023;
originally announced April 2023.
-
One-way resynchronizability of word transducers
Authors:
Sougata Bose,
S. N. Krishna,
Anca Muscholl,
Gabriele Puppis
Abstract:
The origin semantics for transducers was proposed in 2014, and 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 one-way transducers in the origin semantics. We show that it is decidable whether a non-deterministic two-way word transducer ca…
▽ More
The origin semantics for transducers was proposed in 2014, and 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 one-way transducers in the origin semantics. We show that it is decidable whether a non-deterministic two-way word transducer can be resynchronized by a bounded, regular resynchronizer into an origin-equivalent one-way transducer. The result is in contrast with the usual semantics, where it is undecidable to know if a non-deterministic two-way transducer is equivalent to some one-way transducer.
△ Less
Submitted 20 January, 2021;
originally announced January 2021.
-
The monitoring problem for timed automata
Authors:
Alejandro Grez,
Filip Mazowiecki,
Michał Pilipczuk,
Gabriele Puppis,
Cristian Riveros
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 under a different perspective, that is, we consider a dynamic version of the problem, called monitoring problem, where the automaton is fixed and the input is revealed as in a stream, one symbol at a time following the natural o…
▽ More
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 under a different perspective, that is, we consider a dynamic version of the problem, called monitoring problem, where the automaton is fixed and the input is revealed as in a stream, one symbol at a time following the natural order on positions. The goal here is to design a dynamic data structure that can be queried about whether the word consisting of symbols revealed so far is accepted by the automaton, and that can be efficiently updated when the next symbol is revealed. We provide complexity bounds for this monitoring problem, by considering timed automata that process symbols interleaved with timestamps. The main contribution is that monitoring of a one-clock timed automaton, with all its components but the clock constants fixed, can be done in amortised constant time per input symbol.
△ Less
Submitted 17 February, 2020;
originally announced February 2020.
-
On Synthesis of Resynchronizers for Transducers
Authors:
Sougata Bose,
Shankara Narayanan Krishna,
Anca Muscholl,
Vincent Penelle,
Gabriele Puppis
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 s…
▽ More
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 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.
△ Less
Submitted 24 June, 2019; v1 submitted 20 June, 2019;
originally announced June 2019.
-
Equivalence of finite-valued streaming string transducers is decidable
Authors:
Anca Muscholl,
Gabriele Puppis
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 finite-valued copyless streaming string transducers is decidable.
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 finite-valued copyless streaming string transducers is decidable.
△ Less
Submitted 30 April, 2019; v1 submitted 19 February, 2019;
originally announced February 2019.
-
Origin-equivalence of two-way word transducers is in PSPACE
Authors:
Sougata Bose,
Anca Muscholl,
Vincent Penelle,
Gabriele Puppis
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 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, call…
▽ More
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 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.
△ Less
Submitted 5 October, 2018; v1 submitted 20 July, 2018;
originally announced July 2018.
-
One-way definability of two-way word transducers
Authors:
Félix Baschenis,
Olivier Gauwin,
Anca Muscholl,
Gabriele Puppis
Abstract:
Functional transductions realized by two-way transducers (or, equally, by streaming transducers or MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown in 2013 that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algorithm of different…
▽ More
Functional transductions realized by two-way transducers (or, equally, by streaming transducers or MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown in 2013 that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algorithm of different flavor solving the above question, that has doubly exponential space complexity. In the special case of sweeping transducers the complexity is one exponential less. We also show how to construct an equivalent one-way transducer, whenever it exists, in doubly or triply exponential time, again depending on whether the input transducer is sweeping or two-way. In the sweeping case our construction is shown to be optimal.
△ Less
Submitted 6 December, 2018; v1 submitted 6 June, 2017;
originally announced June 2017.
-
An algebraic approach to MSO-definability on countable linear orderings
Authors:
Olivier Carton,
Thomas Colcombet,
Gabriele Puppis
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 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…
▽ More
We develop an algebraic notion of recognizability for languages of words indexed by countable linear orderings. We prove that this notion is effectively equivalent to definability in monadic second-order (MSO) logic. We also provide three logical applications. First, we establish the first known collapse result for the quantifier alternation of MSO logic over countable linear orderings. Second, we solve an open problem posed by Gurevich and Rabinovich, concerning the MSO-definability of sets of rational numbers using the reals in the background. Third, we establish the MSO-definability of the set of yields induced by an MSO-definable set of trees, confirming a conjecture posed by Bruy{è}re, Carton, and S{é}nizergues.
△ Less
Submitted 29 May, 2018; v1 submitted 17 February, 2017;
originally announced February 2017.
-
Untwisting two-way transducers in elementary time
Authors:
Félix Baschenis,
Olivier Gauwin,
Anca Muscholl,
Gabriele Puppis
Abstract:
Functional transductions realized by two-way transducers (equivalently, by streaming transducers and by MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown recently (LICS'13) that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algori…
▽ More
Functional transductions realized by two-way transducers (equivalently, by streaming transducers and by MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown recently (LICS'13) that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algorithm of different flavor solving the above question, that has double exponential space complexity. We further apply our technique to decide whether the transduction realized by a two-way transducer can be implemented by a sweeping transducer, with either known or unknown number of passes.
△ Less
Submitted 10 January, 2017;
originally announced January 2017.
-
A decidable weakening of Compass Logic based on cone-shaped cardinal directions
Authors:
Angelo Montanari,
Gabriele Puppis,
Pietro Sala
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 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 spat…
▽ More
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 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.
△ Less
Submitted 9 December, 2015; v1 submitted 12 October, 2015;
originally announced October 2015.
-
Inference From Visible Information And Background Knowledge
Authors:
Michael Benedikt,
Pierre Bourhis,
Balder ten Cate,
Gabriele Puppis,
Michael Vanden Boom
Abstract:
We provide a wide-ranging study of the scenario where a subset of the relations in a relational vocabulary are visible to a user --- that is, their complete contents are known --- while the remaining relations are invisible. We also have a background theory --- invariants given by logical sentences --- which may relate the visible relations to invisible ones, and also may constrain both the visibl…
▽ More
We provide a wide-ranging study of the scenario where a subset of the relations in a relational vocabulary are visible to a user --- that is, their complete contents are known --- while the remaining relations are invisible. We also have a background theory --- invariants given by logical sentences --- which may relate the visible relations to invisible ones, and also may constrain both the visible and invisible relations in isolation. We want to determine whether some other information, given as a positive existential formula, can be inferred using only the visible information and the background theory. This formula whose inference we are concered with is denoted as the \emph{query}. We consider whether positive information about the query can be inferred, and also whether negative information -- the sentence does not hold -- can be inferred. We further consider both the instance-level version of the problem, where both the query and the visible instance are given, and the schema-level version, where we want to know whether truth or falsity of the query can be inferred in some instance of the schema.
△ Less
Submitted 11 May, 2018; v1 submitted 5 September, 2015;
originally announced September 2015.
-
Logics with rigidly guarded data tests
Authors:
Gabriele Puppis,
Thomas Colcombet,
Clemens Ley
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 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 Sc…
▽ More
The notion of orbit finite data monoid was recently introduced by Bojanczyk as an algebraic object for defining recognizable languages of data words. Following Buchi's approach, we introduce a variant of monadic second-order logic with data equality tests that captures precisely the data languages recognizable by orbit finite data monoids. We also establish, following this time the approach of Schutzenberger, McNaughton and Papert, that the first-order fragment of this logic defines exactly the data languages recognizable by aperiodic orbit finite data monoids. Finally, we consider another variant of the logic that can be interpreted over generic structures with data. The data languages defined in this variant are also recognized by unambiguous finite memory automata.
△ Less
Submitted 16 September, 2015; v1 submitted 8 October, 2014;
originally announced October 2014.
-
Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification
Authors:
Gabriele Puppis,
Tiziano Villa
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 conferen…
▽ More
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.
△ Less
Submitted 16 July, 2013;
originally announced July 2013.
-
Decidability of the interval temporal logic ABBar over the natural numbers
Authors:
A. Montanari,
G. Puppis,
P. Sala,
G. Sciavicco
Abstract:
In this paper, we focus our attention on the interval temporal logic of the Allen's relations "meets", "begins", and "begun by" (ABBar 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…
▽ More
In this paper, we focus our attention on the interval temporal logic of the Allen's relations "meets", "begins", and "begun by" (ABBar 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 ABBar 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
△ Less
Submitted 3 February, 2010; v1 submitted 17 December, 2009;
originally announced December 2009.
