This paper studies decision problems for Boolean combinations of ω-rational trace languages. The complexities of these decision problems (emptiness, regularity, rationality) are classified depending on properties of the independence alphabets and of the Boolean combinations allowed. For any of the problems, we obtain a trichotomy ranging from decidable over a low level of the arithmetical hierarchy to a low level of the analytical hierarchy.

We consider the reachability relation of pushdown systems whose pushdown holds a Mazurkiewicz trace instead of just a word as in classical systems. Under two natural conditions on the transition structure of such systems, we prove that the reachability relation is lc-rational, a new notion that restricts the class of rational trace relations. We also develop the theory of these lc-rational relations to the point where they allow to infer that forwards-reachability of a trace-pushdown system preserves the rationality and backwards-reachability the recognizability of sets of configurations. As a consequence it is decidable whether one recognizable set of configurations can be reached from some rational set of configurations. All our constructions are polynomial (assuming the dependence alphabet to be fixed). These findings generalize results by Caucal on classical pushdown systems (namely the rationality of the reachability relation of such systems), complement results by Zetzsche (namely the decidability for arbitrary transition structures under severe restrictions on the dependence alphabet), and extend results from our conference papers [1] and [2] .

A cooperating multi-pushdown system consists of a tuple of pushdown systems that can delegate the execution of recursive procedures to sub-tuples; control returns to the calling tuple once all sub-tuples finished their task. This allows the concurrent execution since disjoint sub-tuples can perform their task independently. Because of the concrete form of recursive descent into sub-tuples, the content of the multi-pushdown does not form an arbitrary tuple of words, but can be understood as a Mazurkiewicz trace. For such systems, we prove that the backwards reachability relation efficiently preserves recognizability, generalizing a result and proof technique by Bouajjani et al. for single-pushdown systems. It follows that the reachability relation is decidable for cooperating multi-pushdown systems in polynomial time and the same holds, e.g., for safety and liveness properties given by recognizable sets of configurations.

Is it possible to write significantly smaller formulae when using Boolean operators other than those of the De Morgan basis (and, or, not, and the constants)? For propositional logic, a negative answer was given by Pratt: formulae over one set of operators can always be translated into an equivalent formula over any other complete set of operators with only polynomial increase in size. Surprisingly, for modal logic the picture is different: we show that elimination of bi-implication is only possible at the cost of an exponential number of occurrences of the modal operator $\lozenge$ and therefore of an exponential increase in formula size, i.e., the De Morgan basis and its extension by bi-implication differ in succinctness. Moreover, we prove that any complete set of Boolean operators agrees in succinctness with the De Morgan basis or with its extension by bi-implication. More precisely, these results are shown for the modal logic $\mathrm{T}$ (and therefore for $\mathrm{K}$). We complement them showing that the modal logic $\mathrm{S5}$ behaves as propositional logic: the choice of Boolean operators has no significant impact on the size of formulae.

Abstract This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of first-order logic by threshold counting quantifiers. The main result shows that the two-variable fragment of this logic can be decided in twofold exponential alternating time with linearly many alternations (and therefore in particular in twofold exponential space as announced in the conference version (Kuske and Schwarz, in: MFCS’20, Leibniz International Proceedings in Informatics (LIPIcs) vol. 170, pp 56:1–56:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020) of this paper) provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent in the space bound. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalises the procedure by Karandikar and Schnoebelen for first-order logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.

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\"artig quantifier results in an undecidable theory.

This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of first-order logic by threshold counting quantifiers. The main result shows that the two-variable fragment of this logic can be decided in two-fold exponential space provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalizes the procedure by Karandikar and Schnoebelen for first-order logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.

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 where only the language of all words without the cover relation and fragments of first-order logic were considered.

Automatic structures are structures that admit a finite presentation via automata. Their most prominent feature is that their theories are decidable. In the literature, one finds automatic structures with non-elementary theory (e.g., the complete binary tree with equal-level predicate) and automatic structures whose theories are at most 3-fold exponential (e.g., Presburger arithmetic or infinite automatic graphs of bounded degree). This observation led Durand-Gasselin to the question whether there are automatic structures of arbitrary high elementary complexity. We give a positive answer to this question. Namely, we show that for every h >=0 the forest of (infinitely many copies of) all finite trees of height at most h+2 is automatic and it's theory is complete for STA(*, exp_h(n, poly(n)), poly(n)), an alternating complexity class between h-fold exponential time and space. This exact determination of the complexity of the theory of these forests might be of independent interest.

We consider the extension of first-order logic FO by unary counting quantifiers and generalise the notion of Gaifman normal form from FO to this setting. For formulas that use only ultimately periodic counting quantifiers, we provide an algorithm that computes equivalent formulas in Gaifman normal form. We also show that this is not possible for formulas using at least one quantifier that is not ultimately periodic. Now let d be a degree bound. We show that for any formula phi with arbitrary counting quantifiers, there is a formula gamma in Gaifman normal form that is equivalent to phi on all finite structures of degree <= d. If the quantifiers of phi are decidable (decidable in elementary time, ultimately periodic), gamma can be constructed effectively (in elementary time, in worst-case optimal 3-fold exponential time). For the setting with unrestricted degree we show that by using our Gaifman normal form for formulas with only ultimately periodic counting quantifiers, a known fixed-parameter tractability result for FO on classes of structures of bounded local tree-width can be lifted to the extension of FO with ultimately periodic counting quantifiers (a logic equally expressive as FO+MOD, i.e., first-oder logic with modulo-counting quantifiers).

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 study the existence of Hanf normal forms for extensions FO(Q) of first-order logic by sets Q ⊆ P(N) of unary counting quantifiers. A formula is in Hanf normal form if it is a Boolean combination of formulas ζ(x) describing the isomorphism type of a local neighbourhood around its free variables x and statements of the form "the number of witnesses y of ψ(y) belongs to (Q+k)" where Q ∈ Q, k ∈ N, and ψ describes the isomorphism type of a local neighbourhood around its unique free variable y.

We study word structures of the form (D,<=,P) where D is either N or Z, <= is a linear ordering on D and P in D is a predicate on D. In particular we show: (a) The set of recursive omega-words with decidable monadic second order theories is Sigma_3-complete. (b) We characterise those sets P subset of Z that yield bi-infinite words (Z,<=,P) with decidable monadic second order theories. (c) We show that such "tame" predicates P exist in every Turing degree. (d) We determine, for P subset of Z, the number of predicates Q subset of Z such that (Z,<=,P) and (Z,<=,Q) are indistinguishable. Through these results we demonstrate similarities and differences between logical properties of infinite and bi-infinite words.

We consider the linear-time model checking problem for boolean concurrent programs with recursive procedure calls. While sequential recursive programs are usually modeled as pushdown automata, concurrent recursive programs involve several processes and can be naturally abstracted as pushdown automata with multiple stacks. Their behavior can be understood as words with multiple nesting relations, each relation connecting a procedure call with its corresponding return. To reason about multiply nested words, we consider the class of all temporal logics as defined in the book by Gabbay, Hodkinson, and Reynolds (1994). The unifying feature of these temporal logics is that their modalities are defined in monadic second-order (MSO) logic. In particular, this captures numerous temporal logics over concurrent and/or recursive programs that have been defined so far. Since the general model checking problem is undecidable, we restrict attention to phase bounded executions as proposed by La Torre, Madhusudan, and Parlato (LICS 2007). While the MSO model checking problem in this case is non-elementary, our main result states that the model checking (and satisfiability) problem for all MSO-definable temporal logics is decidable in elementary time. More precisely, it is solvable in (n + 2)-EXPTIME where n is the maximal level of the MSO modalities in the monadic quantifier alternation hierarchy. We complement this result and provide, for each level n, a temporal logic whose model checking problem is n-EXPSPACE-hard.

This paper's main result presents a 3-fold exponential algorithm that transforms a first-order formula φ together with a number d into a formula in Gaifman normal form that is equivalent to φ on the class of structures of degree at most d. For structures of polynomial growth, we even get a 2-fold exponential algorithm. These results are complemented by matching lower bounds: We show that for structures of degree 2, a 2-fold exponential blow-up in the size of formulas cannot be avoided. And for structures of degree 3, a 3-fold exponential blow-up is unavoidable. As a result of independent interest we obtain a 1-fold exponential algorithm which transforms a given first-order sentence φ of a very restricted shape into a sentence in Gaifman normal form that is equivalent to φ on all structures.

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 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 [28] by improving both the lower and the upper bounds.

Several new undecidability results on isomorphism problems for automatic structures are shown: (i) The isomorphism problem for automatic equivalence relations is Π10-complete, (ii) The isomorphism problem for automatic trees of height n ≥ 2 is Π2n-30-complete, (iii) The isomorphism problem for automatic linear orders is not arithmetical.

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.

Abstract For automatic and recursive graphs, we investigate the following problems: (A) existence of a Hamiltonian path and existence of an infinite path in a tree (B) existence of an Euler path, bounding the number of ends, and bounding the number of infinite branches in a tree (C) existence of an infinite clique and an infinite version of set cover The complexity of these problems is determined for automatic graphs and. supplementing results from the literature, for recursive graphs. Our results show that these problems (A) are equally complex for automatic and for recursive graphs ( -complete). (B) are moderately less complex for automatic than for recursive graphs (complete for different levels of the arithmetic hierarchy), (C) are much simpler for automatic than for recursive graphs (decidable and -complete, resp.).

Abstract The logic extends first-order logic by a generalized form of counting quantifiers (“the number of elements satisfying … belongs to the setC”). This logic is investigated for structures with an injectivelyω-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [6]. It is shown that, as in the case of automatic structures [21], also modulo-counting quantifiers as well as infinite cardinality quantifiers (“there are many elements satisfying …”) lead to decidable theories. For a structure of bounded degree with injectiveω-automatic presentation, the fragment of that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (ω-automaticity and bounded degree) are necessary for this result to hold.

Logical properties of iterations of relational structures are studied and these decidability results are applied to the model checking of a powerful extension of pushdown systems. It is shown that the monadic chain theory of the iteration of a structure A (in the sense of Shelah and Stupp) is decidable in case the first-order theory of the structure A is decidable. This result fails if Muchnik's clone-predicate is added. A model of pushdown automata, where the stack alphabet is given by an arbitrary (possibly infinite) relational structure, is introduced. If the stack structure has a decidable first-order theory with regular reachability predicates, then the same holds for the configuration graph of this pushdown automaton. This result follows from our decidability result for the monadic chain theory of the iteration

We define the class of divisibility monoids that arise as quotients of the free monoid Σ* modulo certain equations of the form ab = cd. These form a much larger class than free partially commutative monoids, and we show, under certain assumptions, that the recognizable languages in these divisibility monoids coincide with c-rational languages. The proofs rely on Ramsey's theorem, distributive lattice theory and on Hashigushi's rank function generalized to these monoids. We obtain Ochmański's theorem on recognizable languages in free partially commutative monoids as a consequence.

Under the assumption that the Polynomial-Time Hierarchy does not collapse we show for a regular language L: the unbalanced polynomial-time leaf language class determined by L equals iff L is existentially but not quantifierfree definable in FO[<, min, max, +1, −1]. Furthermore, no such class lies properly between NP and co-1-NP or NP⊕co-NP. The proofs rely on a result of Pin and Weil characterizing the automata of existentially first-order definable languages.