Search

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.

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.

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.

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 $\omega$-words with decidable monadic second order theories is $\Sigma_3$-complete. (b) Known characterisations of the $\omega$-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.

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., Comment: 41 pages

We consider simulation games played between Spoiler and Duplicator on two B\"uchi 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)., Comment: In Proceedings GandALF 2016, arXiv:1609.03648

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., Comment: In Proceedings Cassting'16/SynCoP'16, arXiv:1608.00177

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 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.

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 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 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.

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 $\Sigma^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 ($\Pi^0_1$-complete, resp,) for height 1 (2, resp.), (ii) $\Pi^1_1$-hard and in $\Pi^1_2$ for height 3, and (iii) $\Pi^1_{n-3}$- and $\Sigma^1_{n-3}$-hard and in $\Pi^1_{2n-4}$ (assuming CH) for all n > 3. All proofs are elementary and do not rely on theorems from set theory.

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 $\Sigma^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 $\Pi^0_1$ (first universal level of the arithmetical hierarchy). (ii) The isomorphism problem for automatic trees of height $n \geq 2$ is $\Pi^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.

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.

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., Comment: 26 pages

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.