-
On Presburger arithmetic extended with non-unary counting quantifiers
Authors:
Peter Habermehl,
Dietrich Kuske
Abstract:
We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers, all applied to tuples of variables (here, residues are given as terms while moduli and thresholds are given explicitly). Our main result shows that satisfaction for this logic is decidable in two-fold exponential space…
▽ More
We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers, all applied to tuples of variables (here, residues are given as terms while moduli and thresholds are given explicitly). Our main result shows that satisfaction for this logic is decidable in two-fold exponential space. If only threshold- and exact-counting quantifiers are allowed, we prove an upper bound of alternating two-fold exponential time with linearly many alternations. This latter result almost matches Berman's exact complexity of first-order logic without counting quantifiers.
To obtain these results, we first translate threshold- and exact-counting quantifiers into classical first-order logic in polynomial time (which already proves the second result). To handle the remaining modulo-counting quantifiers for tuples, we first reduce them in doubly exponential time to modulo-counting quantifiers for single elements. For these quantifiers, we provide a quantifier elimination procedure similar to Reddy and Loveland's procedure for first-order logic and analyse the growth of coefficients, constants, and moduli appearing in this process. The bounds obtained this way allow to restrict quantification in the original formula to integers of bounded size which then implies the first result mentioned above.
Our logic is incomparable with the logic considered by Chistikov et al. in 2022. They allow more general counting operations in quantifiers, but only unary quantifiers. The move from unary to non-unary quantifiers is non-trivial, since, e.g., the non-unary version of the Härtig quantifier results in an undecidable theory.
△ Less
Submitted 11 July, 2023; v1 submitted 8 April, 2022;
originally announced April 2022.
-
Languages ordered by the subword order
Authors:
Dietrich Kuske,
Georg Zetzsche
Abstract:
We consider a language together with the subword relation, the cover relation, and regular predicates. For such structures, we consider the extension of first-order logic by threshold- and modulo-counting quantifiers. Depending on the language, the used predicates, and the fragment of the logic, we determine four new combinations that yield decidable theories. These results extend earlier ones whe…
▽ More
We consider a language together with the subword relation, the cover relation, and regular predicates. For such structures, we consider the extension of first-order logic by threshold- and modulo-counting quantifiers. Depending on the language, the used predicates, and the fragment of the logic, we determine four new combinations that yield decidable theories. These results extend earlier ones where only the language of all words without the cover relation and fragments of first-order logic were considered.
△ Less
Submitted 8 January, 2019;
originally announced January 2019.
-
Infinite and Bi-infinite Words with Decidable Monadic Theories
Authors:
Dietrich Kuske,
Jiamou Liu,
Anastasia Moskvina
Abstract:
We study word structures of the form $(D,<,P)$ where $D$ is either $\mathbb{N}$ or $\mathbb{Z}$, $<$ is the natural linear ordering on $D$ and $P\subseteq D$ is a predicate on $D$. In particular we show:
(a) The set of recursive $ω$-words with decidable monadic second order theories is $Σ_3$-complete.
(b) Known characterisations of the $ω$-words with decidable monadic second order theories are…
▽ More
We study word structures of the form $(D,<,P)$ where $D$ is either $\mathbb{N}$ or $\mathbb{Z}$, $<$ is the natural linear ordering on $D$ and $P\subseteq D$ is a predicate on $D$. In particular we show:
(a) The set of recursive $ω$-words with decidable monadic second order theories is $Σ_3$-complete.
(b) Known characterisations of the $ω$-words with decidable monadic second order theories are transfered to the corresponding question for bi-infinite words.
(c) We show that such "tame" predicates $P$ exist in every Turing degree.
(d) We determine, for $P\subseteq\mathbb{Z}$, the number of predicates $Q\subseteq\mathbb{Z}$ such that $(\mathbb{Z},\le,P)$ and $(\mathbb{Z},\le,Q)$ are indistinguishable.
Through these results we demonstrate similarities and differences between logical properties of infinite and bi-infinite words.
△ Less
Submitted 17 August, 2018; v1 submitted 11 December, 2017;
originally announced December 2017.
-
First-Order Logic with Counting: At Least, Weak Hanf Normal Forms Always Exist and Can Be Computed!
Authors:
Dietrich Kuske,
Nicole Schweikardt
Abstract:
We introduce the logic FOCN(P) which extends first-order logic by counting and by numerical predicates from a set P, and which can be viewed as a natural generalisation of various counting logics that have been studied in the literature.
We obtain a locality result showing that every FOCN(P)-formula can be transformed into a formula in Hanf normal form that is equivalent on all finite structures…
▽ More
We introduce the logic FOCN(P) which extends first-order logic by counting and by numerical predicates from a set P, and which can be viewed as a natural generalisation of various counting logics that have been studied in the literature.
We obtain a locality result showing that every FOCN(P)-formula can be transformed into a formula in Hanf normal form that is equivalent on all finite structures of degree at most d. A formula is in Hanf normal form if it is a Boolean combination of formulas describing the neighbourhood around its tuple of free variables and arithmetic sentences with predicates from P over atomic statements describing the number of realisations of a type with a single centre. The transformation into Hanf normal form can be achieved in time elementary in $d$ and the size of the input formula. From this locality result, we infer the following applications: (*) The Hanf-locality rank of first-order formulas of bounded quantifier alternation depth only grows polynomially with the formula size. (*) The model checking problem for the fragment FOC(P) of FOCN(P) on structures of bounded degree is fixed-parameter tractable (with elementary parameter dependence). (*) The query evaluation problem for fixed queries from FOC(P) over fully dynamic databases of degree at most d can be solved efficiently: there is a dynamic algorithm that can enumerate the tuples in the query result with constant delay, and that allows to compute the size of the query result and to test if a given tuple belongs to the query result within constant time after every database update.
△ Less
Submitted 3 March, 2017;
originally announced March 2017.
-
Multi-Buffer Simulations for Trace Language Inclusion
Authors:
Milka Hutagalung,
Norbert Hundeshagen,
Dietrich Kuske,
Martin Lange,
Etienne Lozes
Abstract:
We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study…
▽ More
We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win the game (with unbounded buffers).
△ Less
Submitted 13 September, 2016;
originally announced September 2016.
-
Two-Buffer Simulation Games
Authors:
Milka Hutagalung,
Norbert Hundeshagen,
Dietrich Kuske,
Martin Lange,
Etienne Lozes
Abstract:
We consider simulation games played between Spoiler and Duplicator on two Buchi automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers before she executes them on her structure. Previous work on such games using a single buffer has shown that they are useful to approximate language inclusion problems. We study the decidability and complexity and show t…
▽ More
We consider simulation games played between Spoiler and Duplicator on two Buchi automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers before she executes them on her structure. Previous work on such games using a single buffer has shown that they are useful to approximate language inclusion problems. We study the decidability and complexity and show that games with two buffers can be used to approximate corresponding problems on finite transducers, i.e. the inclusion problem for rational relations over infinite words.
△ Less
Submitted 1 August, 2016;
originally announced August 2016.
-
The trace monoids in the queue monoid and in the direct product of two free monoids
Authors:
Dietrich Kuske,
Olena Prianychnykova
Abstract:
We prove that a trace monoid embeds into the queue monoid if and only if it embeds into the direct product of two free monoids. We also give a decidable characterization of these trace monoids.
We prove that a trace monoid embeds into the queue monoid if and only if it embeds into the direct product of two free monoids. We also give a decidable characterization of these trace monoids.
△ Less
Submitted 23 March, 2016;
originally announced March 2016.
-
The monoid of queue actions
Authors:
Martin Huschenbett,
Dietrich Kuske,
Georg Zetzsche
Abstract:
We investigate the monoid of transformations that are induced by sequences of writing to and reading from a queue storage. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties, e.g., conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem…
▽ More
We investigate the monoid of transformations that are induced by sequences of writing to and reading from a queue storage. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties, e.g., conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem is NL-complete. Furthermore, we present an algebraic characterization of this monoid's recognizable subsets. Finally, we prove that it is not Thurston-automatic.
△ Less
Submitted 22 April, 2014;
originally announced April 2014.
-
Isomorphisms of scattered automatic linear orders
Authors:
Dietrich Kuske
Abstract:
We prove that the isomorphism of scattered tree automatic linear orders as well as the existence of automorphisms of scattered word automatic linear orders are undecidable. For the existence of automatic automorphisms of word automatic linear orders, we determine the exact level of undecidability in the arithmetical hierarchy.
We prove that the isomorphism of scattered tree automatic linear orders as well as the existence of automorphisms of scattered word automatic linear orders are undecidable. For the existence of automatic automorphisms of word automatic linear orders, we determine the exact level of undecidability in the arithmetical hierarchy.
△ Less
Submitted 25 April, 2012;
originally announced April 2012.
-
An optimal construction of Hanf sentences
Authors:
Benedikt Bollig,
Dietrich Kuske
Abstract:
We give the first elementary construction of equivalent formulas in Hanf normal form. The triply exponential upper bound is complemented by a matching lower bound.
We give the first elementary construction of equivalent formulas in Hanf normal form. The triply exponential upper bound is complemented by a matching lower bound.
△ Less
Submitted 6 June, 2011; v1 submitted 27 May, 2011;
originally announced May 2011.
-
Propositional Dynamic Logic for Message-Passing Systems
Authors:
Benedikt Bollig,
Dietrich Kuske,
Ingmar Meinecke
Abstract:
We examine a bidirectional propositional dynamic logic (PDL) for finite and infinite message sequence charts (MSCs) extending LTL and TLC-. By this kind of multi-modal logic we can express properties both in the entire future and in the past of an event. Path expressions strengthen the classical until operator of temporal logic. For every formula defining an MSC language, we construct a communica…
▽ More
We examine a bidirectional propositional dynamic logic (PDL) for finite and infinite message sequence charts (MSCs) extending LTL and TLC-. By this kind of multi-modal logic we can express properties both in the entire future and in the past of an event. Path expressions strengthen the classical until operator of temporal logic. For every formula defining an MSC language, we construct a communicating finite-state machine (CFM) accepting the same language. The CFM obtained has size exponential in the size of the formula. This synthesis problem is solved in full generality, i.e., also for MSCs with unbounded channels. The model checking problem for CFMs and HMSCs turns out to be in PSPACE for existentially bounded MSCs. Finally, we show that, for PDL with intersection, the semantics of a formula cannot be captured by a CFM anymore.
△ Less
Submitted 7 September, 2010; v1 submitted 27 July, 2010;
originally announced July 2010.
-
The Isomorphism Problem for omega-Automatic Trees
Authors:
Dietrich Kuske,
Jiamou Liu,
Markus Lohrey
Abstract:
The main result of this paper is that the isomorphism for omega-automatic trees of finite height is at least has hard as second-order arithmetic and therefore not analytical. This strengthens a recent result by Hjorth, Khoussainov, Montalban, and Nies showing that the isomorphism problem for omega-automatic structures is not $Σ^1_2$. Moreover, assuming the continuum hypothesis CH, we can show that…
▽ More
The main result of this paper is that the isomorphism for omega-automatic trees of finite height is at least has hard as second-order arithmetic and therefore not analytical. This strengthens a recent result by Hjorth, Khoussainov, Montalban, and Nies showing that the isomorphism problem for omega-automatic structures is not $Σ^1_2$. Moreover, assuming the continuum hypothesis CH, we can show that the isomorphism problem for omega-automatic trees of finite height is recursively equivalent with second-order arithmetic. On the way to our main results, we show lower and upper bounds for the isomorphism problem for omega-automatic trees of every finite height: (i) It is decidable ($Π^0_1$-complete, resp,) for height 1 (2, resp.), (ii) $Π^1_1$-hard and in $Π^1_2$ for height 3, and (iii) $Π^1_{n-3}$- and $Σ^1_{n-3}$-hard and in $Π^1_{2n-4}$ (assuming CH) for all n > 3. All proofs are elementary and do not rely on theorems from set theory.
△ Less
Submitted 5 April, 2010;
originally announced April 2010.
-
The Isomorphism Problem On Classes of Automatic Structures
Authors:
Dietrich Kuske,
Jiamou Liu,
Markus Lohrey
Abstract:
Automatic structures are finitely presented structures where the universe and all relations can be recognized by finite automata. It is known that the isomorphism problem for automatic structures is complete for $Σ^1_1$; the first existential level of the analytical hierarchy. Several new results on isomorphism problems for automatic structures are shown in this paper: (i) The isomorphism proble…
▽ More
Automatic structures are finitely presented structures where the universe and all relations can be recognized by finite automata. It is known that the isomorphism problem for automatic structures is complete for $Σ^1_1$; the first existential level of the analytical hierarchy. Several new results on isomorphism problems for automatic structures are shown in this paper: (i) The isomorphism problem for automatic equivalence relations is complete for $Π^0_1$ (first universal level of the arithmetical hierarchy). (ii) The isomorphism problem for automatic trees of height $n \geq 2$ is $Π^0_{2n-3}$-complete. (iii) The isomorphism problem for automatic linear orders is not arithmetical. This solves some open questions of Khoussainov, Rubin, and Stephan.
△ Less
Submitted 13 January, 2010;
originally announced January 2010.
-
Is Ramsey's theorem omega-automatic?
Authors:
Dietrich Kuske
Abstract:
We study the existence of infinite cliques in omega-automatic (hyper-)graphs. It turns out that the situation is much nicer than in general uncountable graphs, but not as nice as for automatic graphs.
More specifically, we show that every uncountable omega-automatic graph contains an uncountable co-context-free clique or anticlique, but not necessarily a context-free (let alone regular) clique…
▽ More
We study the existence of infinite cliques in omega-automatic (hyper-)graphs. It turns out that the situation is much nicer than in general uncountable graphs, but not as nice as for automatic graphs.
More specifically, we show that every uncountable omega-automatic graph contains an uncountable co-context-free clique or anticlique, but not necessarily a context-free (let alone regular) clique or anticlique. We also show that uncountable omega-automatic ternary hypergraphs need not have uncountable cliques or anticliques at all.
△ Less
Submitted 3 February, 2010; v1 submitted 14 December, 2009;
originally announced December 2009.
-
Automatic structures of bounded degree revisited
Authors:
Dietrich Kuske,
Markus Lohrey
Abstract:
The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be…
▽ More
The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be optimal since we also present a string automatic structure of bounded degree whose first-order theory is hard for 2EXPSPACE. We prove similar results also for tree automatic structures. These findings close the gaps left open in a previous paper of the second author by improving both, the lower and the upper bounds.
△ Less
Submitted 28 October, 2008;
originally announced October 2008.
-
Compatibility of Shelah and Stupp's and Muchnik's iteration with fragments of monadic second order logic
Authors:
Dietrich Kuske
Abstract:
We investigate the relation between the theory of the iterations in the sense of Shelah-Stupp and of Muchnik, resp., and the theory of the base structure for several logics. These logics are obtained from the restriction of set quantification in monadic second order logic to certain subsets like, e.g., finite sets, chains, and finite unions of chains. We show that these theories of the Shelah-St…
▽ More
We investigate the relation between the theory of the iterations in the sense of Shelah-Stupp and of Muchnik, resp., and the theory of the base structure for several logics. These logics are obtained from the restriction of set quantification in monadic second order logic to certain subsets like, e.g., finite sets, chains, and finite unions of chains. We show that these theories of the Shelah-Stupp iteration can be reduced to corresponding theories of the base structure. This fails for Muchnik's iteration.
△ Less
Submitted 20 February, 2008;
originally announced February 2008.
