Showing 1–43 of 43 results for author: Kufleitner, M

The Word Problem for $(ω- 1)$-Terms over $\mathrm{DAb}$

Authors: Jorge Almeida, Manfred Kufleitner, Jan Philipp Wächter

Abstract: We give a ranker-based description using finite-index congruences for the variety $\boldsymbol{\mathrm{DAb}}$ of finite monoids whose regular $\mathcal{D}$-classes form Abelian groups. This combinatorial description yields a normal form for general pseudowords over $\boldsymbol{\mathrm{DAb}}$. For $(ω- 1)$-terms, this normal form is computable, which yields an algorithm for the word problem for… ▽ More We give a ranker-based description using finite-index congruences for the variety $\boldsymbol{\mathrm{DAb}}$ of finite monoids whose regular $\mathcal{D}$-classes form Abelian groups. This combinatorial description yields a normal form for general pseudowords over $\boldsymbol{\mathrm{DAb}}$. For $(ω- 1)$-terms, this normal form is computable, which yields an algorithm for the word problem for $(ω- 1)$-terms of $\boldsymbol{\mathrm{DAb}}$. △ Less

Submitted 13 November, 2024; originally announced November 2024.

MSC Class: 20M07; 20M35; 68Q45 ACM Class: F.4.3

Yet another proof of Parikh's Theorem

Authors: Manfred Kufleitner

Abstract: Parikh's Theorem says that the Parikh image of a context-free language is semilinear. We give a short proof of Parikh's Theorem using the formulation of Verma, Seidl, and Schwentick in terms of Presburger arithmetic. The proof relies on an Eulerian property of derivation trees of context-free languages and was inspired by Hierholzer's algorithm; it does not use the Chomsky normal form. Parikh's Theorem says that the Parikh image of a context-free language is semilinear. We give a short proof of Parikh's Theorem using the formulation of Verma, Seidl, and Schwentick in terms of Presburger arithmetic. The proof relies on an Eulerian property of derivation trees of context-free languages and was inspired by Hierholzer's algorithm; it does not use the Chomsky normal form. △ Less

Submitted 6 October, 2022; originally announced October 2022.

Reachability Games and Parity Games

Authors: Volker Diekert, Manfred Kufleitner

Abstract: Parity games are positionally determined. This is a fundamental and classical result. In 2010, Calude et al. showed a breakthrough result for finite parity games: the winning regions and their positional winning strategies can be computed in quasi-polynomial time. In the present paper we give a self-contained and detailed proofs for both results. The results in this paper are not meant to be ori… ▽ More Parity games are positionally determined. This is a fundamental and classical result. In 2010, Calude et al. showed a breakthrough result for finite parity games: the winning regions and their positional winning strategies can be computed in quasi-polynomial time. In the present paper we give a self-contained and detailed proofs for both results. The results in this paper are not meant to be original. The positional determinacy result is shown for possibly infinite parity games using the ideas of Zielonka which he published in 1998. In order to show quasi-polynomial time, we follow Lehtinen's register games, which she introduced in 2018. Although the time complexity of Lehtinen's algorithm is not optimal, register games are conceptually simple and interesting in their own right. Various of our proofs are either new or simplifications of the original proofs. The topics in this paper include the definition and the computation of optimal attractors for reachability games, too. △ Less

Submitted 22 August, 2022; originally announced August 2022.

The Inclusion Problem for Forest Languages under Substitutions

Authors: Marcial Gaißert, Manfred Kufleitner

Abstract: We consider algorithms and lower bounds for various problems over forest languages; as input models we allow forest algebras, deterministic forest automata and nondeterministic forest automata. For the equivalence problem, we give an almost-linear-time algorithm for both forest algebras and deterministic forest automata; this is complemented by a polynomial time hardness result. The emptiness prob… ▽ More We consider algorithms and lower bounds for various problems over forest languages; as input models we allow forest algebras, deterministic forest automata and nondeterministic forest automata. For the equivalence problem, we give an almost-linear-time algorithm for both forest algebras and deterministic forest automata; this is complemented by a polynomial time hardness result. The emptiness problem is complete for polynomial time over each of the three models. Additionally, we consider the emptiness of intersection problem for forest algebras and deterministic forest automata; this problem turns out to be complete for exponential time. It is well-known that the corresponding problems for word languages are complete for nondeterministic logarithmic space and for polynomial space, respectively. Equipped with this toolbox of algorithms and lower bounds, we consider various inclusion problems for regular forest languages under substitutions. The substitutions in this paper replace leaf variables by forest languages. Depending on the direction of the inclusion, the problem for a given substitution is either complete for polynomial time or for exponential time; in particular, the equivalence problem under substitutions is complete for exponential time and, hence, more difficult than the equivalence problem for forest languages without substitutions. If we ask whether there exists a substitution such that a given inclusion holds, then this problem is either complete for NP or exponential time, depending on whether we consider inclusion or equivalence; moreover, the problem is undecidable if the substitution is applied on both sides. △ Less

Submitted 4 June, 2021; originally announced June 2021.

MSC Class: 68Q45 (Primary) 68Q70; 68Q17 (Secondary) ACM Class: F.2.2; F.4.3

Conelikes and Ranker Comparisons

Authors: Viktor Henriksson, Manfred Kufleitner

Abstract: For every fixed class of regular languages, there is a natural hierarchy of increasingly more general problems: Firstly, the membership problem asks whether a given language belongs to the fixed class of languages. Secondly, the separation problem asks for two given languages whether they can be separated by a language from the fixed class. And thirdly, the covering problem is a generalization of… ▽ More For every fixed class of regular languages, there is a natural hierarchy of increasingly more general problems: Firstly, the membership problem asks whether a given language belongs to the fixed class of languages. Secondly, the separation problem asks for two given languages whether they can be separated by a language from the fixed class. And thirdly, the covering problem is a generalization of separation problem to more than two given languages. Most instances of such problems were solved by the connection of regular languages and finite monoids. Both the membership problem and the separation problem were also extended to ordered monoids. The computation of pointlikes can be interpreted as the algebraic counterpart of the covering problem. In this paper, we consider the extension the computation of pointlikes to ordered monoids. This leads to the notion of conelikes for the corresponding algebraic framework. We apply this framework to the Trotter-Weil hierarchy and both the full and the half levels of the $\text{FO}^2$ quantifier alternation hierarchy. As a consequence, we solve the covering problem for the resulting subvarieties of $\mathbf{DA}$. An important combinatorial tool are uniform ranker characterizations for all subvarieties under consideration; these characterizations stem from order comparisons of ranker positions. △ Less

Submitted 30 September, 2021; v1 submitted 19 May, 2021; originally announced May 2021.

MSC Class: 68Q45 (Primary) 03D05; 06F05; 68Q70 (Secondary) ACM Class: F.4.1; F.4.3

Deciding FO2 Alternation for Automata over Finite and Infinite Words

Authors: Viktor Henriksson, Manfred Kufleitner

Abstract: We consider two-variable first-order logic $\text{FO}^2$ and its quantifier alternation hierarchies over both finite and infinite words. Our main results are forbidden patterns for deterministic automata (finite words) and for Carton-Michel automata (infinite words). In order to give concise patterns, we allow the use of subwords on paths in finite graphs. This concept is formalized as subword-pat… ▽ More We consider two-variable first-order logic $\text{FO}^2$ and its quantifier alternation hierarchies over both finite and infinite words. Our main results are forbidden patterns for deterministic automata (finite words) and for Carton-Michel automata (infinite words). In order to give concise patterns, we allow the use of subwords on paths in finite graphs. This concept is formalized as subword-patterns. For certain types of subword-patterns there exists a non-deterministic logspace algorithm to decide their presence or absence in a given automaton. In particular, this leads to $\mathbf{NL}$ algorithms for deciding the levels of the $\text{FO}^2$ quantifier alternation hierarchies. This applies to both full and half levels, each over finite and infinite words. Moreover, we show that these problems are $\mathbf{NL}$-hard and, hence, $\mathbf{NL}$-complete. △ Less

Submitted 1 September, 2021; v1 submitted 19 May, 2021; originally announced May 2021.

MSC Class: 68Q45 (Primary) 03D05; 68Q17 (Secondary) ACM Class: F.4.1; F.4.3

Nesting negations in FO2 over infinite words

Authors: Viktor Henriksson, Manfred Kufleitner

Abstract: We consider two-variable first-order logic FO2 over infinite words. Restricting the number of nested negations defines an infinite hierarchy; its levels are often called the half-levels of the FO2 quantifier alternation hierarchy. For every level of this hierarchy, we give an effective characterization. For the lower levels, this characterization is a combination of an algebraic and a topological… ▽ More We consider two-variable first-order logic FO2 over infinite words. Restricting the number of nested negations defines an infinite hierarchy; its levels are often called the half-levels of the FO2 quantifier alternation hierarchy. For every level of this hierarchy, we give an effective characterization. For the lower levels, this characterization is a combination of an algebraic and a topological property. For the higher levels, algebraic properties turn out to be sufficient. Within two-variable first-order logic, each algebraic property is a single ordered identity of omega-terms. The topological properties are the same as for the lower half-levels of the quantifier alternation hierarchy without the two-variable restriction (i.e., the Cantor topology and the alphabetic topology). Our result generalizes the corresponding result for finite words. The proof uses novel techniques and is based on a refinement of Mal'cev products for ordered monoids. △ Less

Submitted 2 December, 2020; originally announced December 2020.

MSC Class: 03D05; 68Q45; 68Q70 ACM Class: F.4.1; F.4.3

Testing Simon's congruence

Authors: Lukas Fleischer, Manfred Kufleitner

Abstract: Piecewise testable languages are a subclass of the regular languages. There are many equivalent ways of defining them; Simon's congruence $\sim_k$ is one of the most classical approaches. Two words are $\sim_k$-equivalent if they have the same set of (scattered) subwords of length at most k. A language L is piecewise testable if there exists some k such that L is a union of $\sim_k$-classes. For e… ▽ More Piecewise testable languages are a subclass of the regular languages. There are many equivalent ways of defining them; Simon's congruence $\sim_k$ is one of the most classical approaches. Two words are $\sim_k$-equivalent if they have the same set of (scattered) subwords of length at most k. A language L is piecewise testable if there exists some k such that L is a union of $\sim_k$-classes. For each equivalence class of $\sim_k$, one can define a canonical representative in shortlex normal form, that is, the minimal word with respect to the lexicographic order among the shortest words in $\sim_k$. We present an algorithm for computing the canonical representative of the $\sim_k$-class of a given word $w \in A^*$ of length n. The running time of our algorithm is in O(|A|n) even if $k \le n$ is part of the input. This is surprising since the number of possible subwords grows exponentially in k. The case $k > n$ is not interesting since then, the equivalence class of w is a singleton. If the alphabet is fixed, the running time of our algorithm is linear in the size of the input word. Moreover, for fixed alphabet, we show that the computation of shortlex normal forms for $\sim_k$ is possible in deterministic logarithmic space. One of the consequences of our algorithm is that one can check with the same complexity whether two words are $\sim_k$-equivalent (with k being part of the input). △ Less

Submitted 27 April, 2018; originally announced April 2018.

ACM Class: F.2.2; F.4.3

The Intersection Problem for Finite Monoids

Authors: Lukas Fleischer, Manfred Kufleitner

Abstract: We investigate the intersection problem for finite monoids, which asks for a given set of regular languages, represented by recognizing morphisms to finite monoids from a variety V, whether there exists a word contained in their intersection. Our main result is that the problem is PSPACE-complete if V is contained in DS and NP-complete if V is non-trivial and contained in DO. Our NP-algorithm for… ▽ More We investigate the intersection problem for finite monoids, which asks for a given set of regular languages, represented by recognizing morphisms to finite monoids from a variety V, whether there exists a word contained in their intersection. Our main result is that the problem is PSPACE-complete if V is contained in DS and NP-complete if V is non-trivial and contained in DO. Our NP-algorithm for the case that V is contained in DO uses novel methods, based on compression techniques and combinatorial properties of DO. We also show that the problem is log-space reducible to the intersection problem for deterministic finite automata (DFA) and that a variant of the problem is log-space reducible to the membership problem for transformation monoids. In light of these reductions, our hardness results can be seen as a generalization of both a classical result by Kozen and a theorem by Beaudry, McKenzie and Therien. △ Less

Submitted 2 February, 2018; v1 submitted 23 November, 2017; originally announced November 2017.

Comments: Extended version of a paper accepted to STACS 2018

ACM Class: F.2.2; F.4.3

Nilpotency and strong nilpotency for finite semigroups

Authors: J. Almeida, M. Kufleitner, M. H. Shahzamanian

Abstract: Nilpotent semigroups in the sense of Mal'cev are defined by semigroup identities. Finite nilpotent semigroups constitute a pseudovariety, $\mathsf{MN}$, which has finite rank. The semigroup identities that define nilpotent semigroups, lead us to define strongly Mal'cev nilpotent semigroups. Finite strongly Mal'cev nilpotent semigroups constitute a non-finite rank pseudovariety, $\mathsf{SMN}$. The… ▽ More Nilpotent semigroups in the sense of Mal'cev are defined by semigroup identities. Finite nilpotent semigroups constitute a pseudovariety, $\mathsf{MN}$, which has finite rank. The semigroup identities that define nilpotent semigroups, lead us to define strongly Mal'cev nilpotent semigroups. Finite strongly Mal'cev nilpotent semigroups constitute a non-finite rank pseudovariety, $\mathsf{SMN}$. The pseudovariety $\mathsf{SMN}$ is strictly contained in the pseudovariety $\mathsf{MN}$ but all finite nilpotent groups are in $\mathsf{SMN}$. We show that the pseudovariety $\mathsf{MN}$ is the intersection of the pseudovariety $\mathsf{BG_{nil}}$ with a pseudovariety defined by a $κ$-identity. We further compare the pseudovarieties $\mathsf{MN}$ and $\mathsf{SMN}$ with the Mal'cev product of the pseudovarieties $\mathsf{J}$ and $\mathsf{G_{nil}}$. △ Less

Submitted 21 July, 2017; originally announced July 2017.

Journal ref: Q. J. Math. 70 (2019), no. 2, 619-648

Green's Relations in Finite Transformation Semigroups

Authors: Lukas Fleischer, Manfred Kufleitner

Abstract: We consider the complexity of Green's relations when the semigroup is given by transformations on a finite set. Green's relations can be defined by reachability in the (right/left/two-sided) Cayley graph. The equivalence classes then correspond to the strongly connected components. It is not difficult to show that, in the worst case, the number of equivalence classes is in the same order of magnit… ▽ More We consider the complexity of Green's relations when the semigroup is given by transformations on a finite set. Green's relations can be defined by reachability in the (right/left/two-sided) Cayley graph. The equivalence classes then correspond to the strongly connected components. It is not difficult to show that, in the worst case, the number of equivalence classes is in the same order of magnitude as the number of elements. Another important parameter is the maximal length of a chain of components. Our main contribution is an exponential lower bound for this parameter. There is a simple construction for an arbitrary set of generators. However, the proof for constant alphabet is rather involved. Our results also apply to automata and their syntactic semigroups. △ Less

Submitted 15 March, 2017; originally announced March 2017.

Comments: Full version of a paper submitted to CSR 2017 on 2016-12-15

Operations on Weakly Recognizing Morphisms

Authors: Lukas Fleischer, Manfred Kufleitner

Abstract: Weakly recognizing morphisms from free semigroups onto finite semigroups are a classical way for defining the class of omega-regular languages, i.e., a set of infinite words is weakly recognizable by such a morphism if and only if it is accepted by some Büchi automaton. We consider the descriptional complexity of various constructions for weakly recognizing morphisms. This includes the conversion… ▽ More Weakly recognizing morphisms from free semigroups onto finite semigroups are a classical way for defining the class of omega-regular languages, i.e., a set of infinite words is weakly recognizable by such a morphism if and only if it is accepted by some Büchi automaton. We consider the descriptional complexity of various constructions for weakly recognizing morphisms. This includes the conversion from and to Büchi automata, the conversion into strongly recognizing morphisms, and complementation. For some problems, we are able to give more precise bounds in the case of binary alphabets or simple semigroups. △ Less

Submitted 27 April, 2016; v1 submitted 17 March, 2016; originally announced March 2016.

ACM Class: F.4.3; F.2.2

Solutions of Word Equations over Partially Commutative Structures

Authors: Volker Diekert, Artur Jeż, Manfred Kufleitner, Alexander Thumm

Abstract: Let $M(A,I)$ be a free partially commutative monoid with involution and $G(A,I)$ be its quotient group, e.g. a right-angled Artin or Coxeter group. Given a system of word equations over $M(A,I)$ with recognizable constraints with input size $n$ we show the structural result about the solution set of the system: the set of all solutions in $M(A,I)$ or in the group $G(A,I)$ is an EDT0L language. Tha… ▽ More Let $M(A,I)$ be a free partially commutative monoid with involution and $G(A,I)$ be its quotient group, e.g. a right-angled Artin or Coxeter group. Given a system of word equations over $M(A,I)$ with recognizable constraints with input size $n$ we show the structural result about the solution set of the system: the set of all solutions in $M(A,I)$ or in the group $G(A,I)$ is an EDT0L language. That is, it is given by an NFA $\mathcal{A}$ recognizing endomorphisms over some extended monoid. Moreover, $\mathcal{A}$ is effectively constructible by an NSPACE($n \log n$)-transducer. This implies that Satisfiability: `Is the system is solvable?' and Finiteness: `Are there infinitely many solutions?' can be decided in NSPACE($n \log n$). In the uniform version, these problems are PSPACE-complete, but for a suitable subclass of constraints we have more precise complexities and we conjecture that the decision problems above are NP-complete in this setting. Our results apply also to word equation over free monoids in the classical case where the involution is reading words right-to-left. This allows to specify that solutions are restricted to be palindromes. △ Less

Submitted 10 June, 2025; v1 submitted 9 March, 2016; originally announced March 2016.

Comments: 83 pages

MSC Class: 03D05; 20F65; 20F70; 68Q25; 68Q45 ACM Class: F.2.2; F.4.2; F.4.3

Efficient Algorithms for Morphisms over Omega-Regular Languages

Authors: Lukas Fleischer, Manfred Kufleitner

Abstract: Morphisms to finite semigroups can be used for recognizing omega-regular languages. The so-called strongly recognizing morphisms can be seen as a deterministic computation model which provides minimal objects (known as the syntactic morphism) and a trivial complementation procedure. We give a quadratic-time algorithm for computing the syntactic morphism from any given strongly recognizing morphism… ▽ More Morphisms to finite semigroups can be used for recognizing omega-regular languages. The so-called strongly recognizing morphisms can be seen as a deterministic computation model which provides minimal objects (known as the syntactic morphism) and a trivial complementation procedure. We give a quadratic-time algorithm for computing the syntactic morphism from any given strongly recognizing morphism, thereby showing that minimization is easy as well. In addition, we give algorithms for efficiently solving various decision problems for weakly recognizing morphisms. Weakly recognizing morphism are often smaller than their strongly recognizing counterparts. Finally, we describe the language operations needed for converting formulas in monadic second-order logic (MSO) into strongly recognizing morphisms, and we give some experimental results. △ Less

Submitted 9 November, 2015; v1 submitted 21 September, 2015; originally announced September 2015.

Comments: Full version of a paper accepted to FSTTCS 2015

ACM Class: F.4.1; F.4.3

Level Two of the Quantifier Alternation Hierarchy over Infinite Words

Authors: Manfred Kufleitner, Tobias Walter

Abstract: The study of various decision problems for logic fragments has a long history in computer science. This paper is on the membership problem for a fragment of first-order logic over infinite words; the membership problem asks for a given language whether it is definable in some fixed fragment. The alphabetic topology was introduced as part of an effective characterization of the fragment $Σ_2$ over… ▽ More The study of various decision problems for logic fragments has a long history in computer science. This paper is on the membership problem for a fragment of first-order logic over infinite words; the membership problem asks for a given language whether it is definable in some fixed fragment. The alphabetic topology was introduced as part of an effective characterization of the fragment $Σ_2$ over infinite words. Here, $Σ_2$ consists of the first-order formulas with two blocks of quantifiers, starting with an existential quantifier. Its Boolean closure is $\mathbb{B}Σ_2$. Our first main result is an effective characterization of the Boolean closure of the alphabetic topology, that is, given an $ω$-regular language $L$, it is decidable whether $L$ is a Boolean combination of open sets in the alphabetic topology. This is then used for transferring Place and Zeitoun's recent decidability result for $\mathbb{B}Σ_2$ from finite to infinite words. △ Less

Submitted 21 September, 2015; originally announced September 2015.

The Word Problem for Omega-Terms over the Trotter-Weil Hierarchy

Authors: Manfred Kufleitner, Jan Philipp Wächter

Abstract: For two given $ω$-terms $α$ and $β$, the word problem for $ω$-terms over a variety $\boldsymbol{\mathrm{V}}$ asks whether $α=β$ in all monoids in $\boldsymbol{\mathrm{V}}$. We show that the word problem for $ω$-terms over each level of the Trotter-Weil Hierarchy is decidable. More precisely, for every fixed variety in the Trotter-Weil Hierarchy, our approach yields an algorithm in nondeterministic… ▽ More For two given $ω$-terms $α$ and $β$, the word problem for $ω$-terms over a variety $\boldsymbol{\mathrm{V}}$ asks whether $α=β$ in all monoids in $\boldsymbol{\mathrm{V}}$. We show that the word problem for $ω$-terms over each level of the Trotter-Weil Hierarchy is decidable. More precisely, for every fixed variety in the Trotter-Weil Hierarchy, our approach yields an algorithm in nondeterministic logarithmic space (NL). In addition, we provide deterministic polynomial time algorithms which are more efficient than straightforward translations of the NL-algorithms. As an application of our results, we show that separability by the so-called corners of the Trotter-Weil Hierarchy is witnessed by $ω$-terms (this property is also known as $ω$-reducibility). In particular, the separation problem for the corners of the Trotter-Weil Hierarchy is decidable. △ Less

Submitted 16 May, 2017; v1 submitted 17 September, 2015; originally announced September 2015.

ACM Class: F.4.1; F.4.3

Two-Variable Ehrenfeucht-Fraisse Games over Omega-Terms

Authors: Manfred Kufleitner, Jan Philipp Wächter

Abstract: Fragments of first-order logic over words can often be characterized in terms of finite monoids, and identities of omega-terms are an effective mechanism for specifying classes of monoids. Huschenbett and the first author have shown how to use infinite Ehrenfeucht-Fraisse games on linear orders for showing that some given fragment satisfies an identity of omega-terms (STACS 2014). After revisiting… ▽ More Fragments of first-order logic over words can often be characterized in terms of finite monoids, and identities of omega-terms are an effective mechanism for specifying classes of monoids. Huschenbett and the first author have shown how to use infinite Ehrenfeucht-Fraisse games on linear orders for showing that some given fragment satisfies an identity of omega-terms (STACS 2014). After revisiting this result, we show that for two-variable logic one can use simpler linear orders. △ Less

Submitted 3 November, 2014; originally announced November 2014.

ACM Class: F.4.1; F.4.3

A Survey on the Local Divisor Technique

Authors: Volker Diekert, Manfred Kufleitner

Abstract: Local divisors allow a powerful induction scheme on the size of a monoid. We survey this technique by giving several examples of this proof method. These applications include linear temporal logic, rational expressions with Kleene stars restricted to prefix codes with bounded synchronization delay, Church-Rosser congruential languages, and Simon's Factorization Forest Theorem. We also introduce th… ▽ More Local divisors allow a powerful induction scheme on the size of a monoid. We survey this technique by giving several examples of this proof method. These applications include linear temporal logic, rational expressions with Kleene stars restricted to prefix codes with bounded synchronization delay, Church-Rosser congruential languages, and Simon's Factorization Forest Theorem. We also introduce the notion of localizable language class as a new abstract concept which unifies some of the proofs for the results above. The current arXiv-version includes some additional material about codes of bounded synchronization delay as well as some updates concerning related literature. △ Less

Submitted 16 March, 2023; v1 submitted 22 October, 2014; originally announced October 2014.

Comments: 20 pages,

MSC Class: 68Q42; 68Q45; 68Q70; 20M3 ACM Class: F.4.1; F.4.3

Journal ref: Theoretical Computer Science , Vol. 610:13--23 (2016)

Star-free languages and local divisors

Authors: Manfred Kufleitner

Abstract: A celebrated result of Schützenberger says that a language is star-free if and only if it is is recognized by a finite aperiodic monoid. We give a new proof for this theorem using local divisors. A celebrated result of Schützenberger says that a language is star-free if and only if it is is recognized by a finite aperiodic monoid. We give a new proof for this theorem using local divisors. △ Less

Submitted 12 August, 2014; originally announced August 2014.

Comments: This is a prior version of an invited contribution at the 16th International Workshop on Descriptional Complexity of Formal Systems (DCFS 2014) in Turku, Finland. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-09704-6_3

MSC Class: 68Q45; 68Q70; 20M3 ACM Class: F.4.3

Journal ref: In H. Jürgensen, J. Karhumäki, and A. Okhotin, editors, Proceedings of DCFS 2014. LNCS vol. 8614, pp. 23-28, 2014

One Quantifier Alternation in First-Order Logic with Modular Predicates

Authors: Manfred Kufleitner, Tobias Walter

Abstract: Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[<,MOD] with order comparison $x<y$ and predicates for $x \equiv i \mod n$ has been investigated by Barrington, Compton, Straubing and Therien. The study of FO[<,MOD]-fragments was initiated by Chaubard, Pin and Straubing. More recently, Dartois and Paperman showed that definability in t… ▽ More Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[<,MOD] with order comparison $x<y$ and predicates for $x \equiv i \mod n$ has been investigated by Barrington, Compton, Straubing and Therien. The study of FO[<,MOD]-fragments was initiated by Chaubard, Pin and Straubing. More recently, Dartois and Paperman showed that definability in the two-variable fragment FO2[<,MOD] is decidable. In this paper we continue this line of work. We give an effective algebraic characterization of the word languages in Sigma2[<,MOD]. The fragment Sigma2 consists of first-order formulas in prenex normal form with two blocks of quantifiers starting with an existential block. In addition we show that Delta2[<,MOD], the largest subclass of Sigma2[<,MOD] which is closed under negation, has the same expressive power as two-variable logic FO2[<,MOD]. This generalizes the result FO2[<] = Delta2[<] of Therien and Wilke to modular predicates. As a byproduct, we obtain another decidable characterization of FO2[<,MOD]. △ Less

Submitted 1 July, 2014; v1 submitted 18 October, 2013; originally announced October 2013.

ACM Class: F.4.1; F.4.3

Ehrenfeucht-Fraisse Games on Omega-Terms

Authors: Martin Huschenbett, Manfred Kufleitner

Abstract: Fragments of first-order logic over words can often be characterized in terms of finite monoids or finite semigroups. Usually these algebraic descriptions yield decidability of the question whether a given regular language is definable in a particular fragment. An effective algebraic characterization can be obtained from identities of so-called omega-terms. In order to show that a given fragment s… ▽ More Fragments of first-order logic over words can often be characterized in terms of finite monoids or finite semigroups. Usually these algebraic descriptions yield decidability of the question whether a given regular language is definable in a particular fragment. An effective algebraic characterization can be obtained from identities of so-called omega-terms. In order to show that a given fragment satisfies some identity of omega-terms, one can use Ehrenfeucht-Fraisse games on word instances of the omega-terms. The resulting proofs often require a significant amount of book-keeping with respect to the constants involved. In this paper we introduce Ehrenfeucht-Fraisse games on omega-terms. To this end we assign a labeled linear order to every omega-term. Our main theorem shows that a given fragment satisfies some identity of omega-terms if and only if Duplicator has a winning strategy for the game on the resulting linear orders. This allows to avoid the book-keeping. As an application of our main result, we show that one can decide in exponential time whether all aperiodic monoids satisfy some given identity of omega-terms, thereby improving a result of McCammond (Int. J. Algebra Comput., 2001). △ Less

Submitted 11 October, 2013; originally announced October 2013.

ACM Class: F.4.1; F.4.3

On the index of Simon's congruence for piecewise testability

Authors: Prateek Karandikar, Manfred Kufleitner, Philippe Schnoebelen

Abstract: Simon's congruence, denoted \sim_n, relates words having the same subwords of length up to n. We show that, over a k-letter alphabet, the number of words modulo \sim_n is in 2^{Θ(n^{k-1} log n)}. Simon's congruence, denoted \sim_n, relates words having the same subwords of length up to n. We show that, over a k-letter alphabet, the number of words modulo \sim_n is in 2^{Θ(n^{k-1} log n)}. △ Less

Submitted 22 September, 2014; v1 submitted 3 October, 2013; originally announced October 2013.

Journal ref: Information Processing Letters, 115(4):515-519, 2015

Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable

Authors: Manfred Kufleitner, Alexander Lauser

Abstract: We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which… ▽ More We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with the FO^2[<,suc] alternation hierarchy. △ Less

Submitted 28 December, 2012; originally announced December 2012.

Comments: Accepted at STACS 2013

ACM Class: F.4.1; F.4.3

On logical hierarchies within FO^2-definable languages

Authors: Manfred Kufleitner, Pascal Weil

Abstract: We consider the class of languages defined in the 2-variable fragment of the first-order logic of the linear order. Many interesting characterizations of this class are known, as well as the fact that restricting the number of quantifier alternations yields an infinite hierarchy whose levels are varieties of languages (and hence admit an algebraic characterization). Using this algebraic approach,… ▽ More We consider the class of languages defined in the 2-variable fragment of the first-order logic of the linear order. Many interesting characterizations of this class are known, as well as the fact that restricting the number of quantifier alternations yields an infinite hierarchy whose levels are varieties of languages (and hence admit an algebraic characterization). Using this algebraic approach, we show that the quantifier alternation hierarchy inside FO^{2}[<] is decidable within one unit. For this purpose, we relate each level of the hierarchy with decidable varieties of languages, which can be defined in terms of iterated deterministic and co-deterministic products. A crucial notion in this process is that of condensed rankers, a refinement of the rankers of Weis and Immerman and the turtle languages of Schwentick, Thérien and Vollmer. △ Less

Submitted 14 August, 2012; v1 submitted 3 August, 2012; originally announced August 2012.

Comments: arXiv admin note: text overlap with arXiv:0904.2894

ACM Class: F.4.3; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (August 14, 2012) lmcs:1212

The Join of the Varieties of R-trivial and L-trivial Monoids via Combinatorics on Words

Authors: Manfred Kufleitner, Alexander Lauser

Abstract: The join of two varieties is the smallest variety containing both. In finite semigroup theory, the varieties of R-trivial and L-trivial monoids are two of the most prominent classes of finite monoids. Their join is known to be decidable due to a result of Almeida and Azevedo. In this paper, we give a new proof for Almeida and Azevedo's effective characterization of the join of R-trivial and L-triv… ▽ More The join of two varieties is the smallest variety containing both. In finite semigroup theory, the varieties of R-trivial and L-trivial monoids are two of the most prominent classes of finite monoids. Their join is known to be decidable due to a result of Almeida and Azevedo. In this paper, we give a new proof for Almeida and Azevedo's effective characterization of the join of R-trivial and L-trivial monoids. This characterization is a single identity of omega-terms using three variables. △ Less

Submitted 27 June, 2012; v1 submitted 24 April, 2012; originally announced April 2012.

Journal ref: Discrete Mathematics & Theoretical Computer Science, Volume 14 No 1, pages 141-146, 2012

The Join Levels of the Trotter-Weil Hierarchy are Decidable

Authors: Manfred Kufleitner, Alexander Lauser

Abstract: The variety DA of finite monoids has a huge number of different characterizations, ranging from two-variable first-order logic FO^2 to unambiguous polynomials. In order to study the structure of the subvarieties of DA, Trotter and Weil considered the intersection of varieties of finite monoids with bands, i.e., with idempotent monoids. The varieties of idempotent monoids are very well understood a… ▽ More The variety DA of finite monoids has a huge number of different characterizations, ranging from two-variable first-order logic FO^2 to unambiguous polynomials. In order to study the structure of the subvarieties of DA, Trotter and Weil considered the intersection of varieties of finite monoids with bands, i.e., with idempotent monoids. The varieties of idempotent monoids are very well understood and fully classified. Trotter and Weil showed that for every band variety V there exists a unique maximal variety W inside DA such that the intersection with bands yields the given band variety V. These maximal varieties W define the Trotter-Weil hierarchy. This hierarchy is infinite and it exhausts DA; induced by band varieties, it naturally has a zigzag shape. In their paper, Trotter and Weil have shown that the corners and the intersection levels of this hierarchy are decidable. In this paper, we give a single identity of omega-terms for every join level of the Trotter-Weil hierarchy; this yields decidability. Moreover, we show that the join levels and the subsequent intersection levels do not coincide. Almeida and Azevedo have shown that the join of R-trivial and L-trivial finite monoids is decidable; this is the first non-trivial join level of the Trotter-Weil hierarchy. We extend this result to the other join levels of the Trotter-Weil hierarchy. At the end of the paper, we give two applications. First, we show that the hierarchy of deterministic and codeterministic products is decidable. And second, we show that the direction alternation depth of unambiguous interval logic is decidable. △ Less

Submitted 20 April, 2012; originally announced April 2012.

The FO^2 alternation hierarchy is decidable

Authors: Manfred Kufleitner, Pascal Weil

Abstract: We consider the two-variable fragment FO^2[<] of first-order logic over finite words. Numerous characterizations of this class are known. Thérien and Wilke have shown that it is decidable whether a given regular language is definable in FO^2[<]. From a practical point of view, as shown by Weis, FO^2[<] is interesting since its satisfiability problem is in NP. Restricting the number of quantifier a… ▽ More We consider the two-variable fragment FO^2[<] of first-order logic over finite words. Numerous characterizations of this class are known. Thérien and Wilke have shown that it is decidable whether a given regular language is definable in FO^2[<]. From a practical point of view, as shown by Weis, FO^2[<] is interesting since its satisfiability problem is in NP. Restricting the number of quantifier alternations yields an infinite hierarchy inside the class of FO^2[<]-definable languages. We show that each level of this hierarchy is decidable. For this purpose, we relate each level of the hierarchy with a decidable variety of finite monoids. Our result implies that there are many different ways of climbing up the FO^2[<]-quantifier alternation hierarchy: deterministic and co-deterministic products, Mal'cev products with definite and reverse definite semigroups, iterated block products with J-trivial monoids, and some inductively defined omega-term identities. A combinatorial tool in the process of ascension is that of condensed rankers, a refinement of the rankers of Weis and Immerman and the turtle programs of Schwentick, Thérien, and Vollmer. △ Less

Submitted 28 March, 2012; originally announced March 2012.

Journal ref: Proceedings of Computer Science Logic (CSL 2012), P. Cegielski, A. Durand eds., Leibniz International Proceedings in Informatics (LIPIcs) 16, 2012, 426-439

Lattices of Logical Fragments over Words

Authors: Manfred Kufleitner, Alexander Lauser

Abstract: This paper introduces an abstract notion of fragments of monadic second-order logic. This concept is based on purely syntactic closure properties. We show that over finite words, every logical fragment defines a lattice of languages with certain closure properties. Among these closure properties are residuals and inverse C-morphisms. Here, depending on certain closure properties of the fragment, C… ▽ More This paper introduces an abstract notion of fragments of monadic second-order logic. This concept is based on purely syntactic closure properties. We show that over finite words, every logical fragment defines a lattice of languages with certain closure properties. Among these closure properties are residuals and inverse C-morphisms. Here, depending on certain closure properties of the fragment, C is the family of arbitrary, non-erasing, length-preserving, length-multiplying, or length-reducing morphisms. In particular, definability in a certain fragment can often be characterized in terms of the syntactic morphism. This work extends a result of Straubing in which he investigated certain restrictions of first-order logic formulae. In contrast to Straubing's model-theoretic approach, our notion of a logical fragment is purely syntactic and it does not rely on Ehrenfeucht-Fraisse games. As motivating examples, we present (1) a fragment which captures the stutter-invariant part of piecewise-testable languages and (2) an acyclic fragment of Sigma_2. As it turns out, the latter has the same expressive power as two-variable first-order logic FO^2. △ Less

Submitted 9 March, 2012; v1 submitted 15 February, 2012; originally announced February 2012.

Report number: TR no. 2012/03 ACM Class: F.4.0; F.4.3

Regular Languages are Church-Rosser Congruential

Authors: Volker Diekert, Manfred Kufleitner, Klaus Reinhardt, Tobias Walter

Abstract: This paper proves a long standing conjecture in formal language theory. It shows that all regular languages are Church-Rosser congruential. The class of Church-Rosser congruential languages was introduced by McNaughton, Narendran, and Otto in 1988. A language L is Church-Rosser congruential, if there exists a finite confluent, and length-reducing semi-Thue system S such that L is a finite union of… ▽ More This paper proves a long standing conjecture in formal language theory. It shows that all regular languages are Church-Rosser congruential. The class of Church-Rosser congruential languages was introduced by McNaughton, Narendran, and Otto in 1988. A language L is Church-Rosser congruential, if there exists a finite confluent, and length-reducing semi-Thue system S such that L is a finite union of congruence classes modulo S. It was known that there are deterministic linear context-free languages which are not Church-Rosser congruential, but on the other hand it was strongly believed that all regular language are of this form. Actually, this paper proves a more general result. △ Less

Submitted 6 February, 2012; originally announced February 2012.

MSC Class: 68Q42 (Primary) 68Q45; 68Q70 (Secondary) ACM Class: F.4.2; F.4.3

Star-Free Languages are Church-Rosser Congruential

Authors: Volker Diekert, Manfred Kufleitner, Pascal Weil

Abstract: The class of Church-Rosser congruential languages has been introduced by McNaughton, Narendran, and Otto in 1988. A language L is Church-Rosser congruential (belongs to CRCL), if there is a finite, confluent, and length-reducing semi-Thue system S such that L is a finite union of congruence classes modulo S. To date, it is still open whether every regular language is in CRCL. In this paper, we sho… ▽ More The class of Church-Rosser congruential languages has been introduced by McNaughton, Narendran, and Otto in 1988. A language L is Church-Rosser congruential (belongs to CRCL), if there is a finite, confluent, and length-reducing semi-Thue system S such that L is a finite union of congruence classes modulo S. To date, it is still open whether every regular language is in CRCL. In this paper, we show that every star-free language is in CRCL. In fact, we prove a stronger statement: For every star-free language L there exists a finite, confluent, and subword-reducing semi-Thue system S such that the total number of congruence classes modulo S is finite and such that L is a union of congruence classes modulo S. The construction turns out to be effective. △ Less

Submitted 18 November, 2011; originally announced November 2011.

Journal ref: Theoretical Computer Science 454 (2012) 129-135

The Krohn-Rhodes Theorem and Local Divisors

Authors: Volker Diekert, Manfred Kufleitner, Benjamin Steinberg

Abstract: We give a new proof of the Krohn-Rhodes Theorem using local divisors. The proof provides nearly as good a decomposition in terms of size as the holonomy decomposition of Eilenberg, avoids induction on the size of the state set, and works exclusively with monoids with the base case of the induction being that of a group. We give a new proof of the Krohn-Rhodes Theorem using local divisors. The proof provides nearly as good a decomposition in terms of size as the holonomy decomposition of Eilenberg, avoids induction on the size of the state set, and works exclusively with monoids with the base case of the induction being that of a group. △ Less

Submitted 7 November, 2011; originally announced November 2011.

MSC Class: 20M10; 20M20; 20M35; 68Q45; 68Q70 ACM Class: F.4.3

Around Dot-depth One

Authors: Manfred Kufleitner, Alexander Lauser

Abstract: The dot-depth hierarchy is a classification of star-free languages. It is related to the quantifier alternation hierarchy of first-order logic over finite words. We consider fragments of languages with dot-depth 1/2 and dot-depth 1 obtained by prohibiting the specification of prefixes or suffixes. As it turns out, these language classes are in one-to-one correspondence with fragments of existentia… ▽ More The dot-depth hierarchy is a classification of star-free languages. It is related to the quantifier alternation hierarchy of first-order logic over finite words. We consider fragments of languages with dot-depth 1/2 and dot-depth 1 obtained by prohibiting the specification of prefixes or suffixes. As it turns out, these language classes are in one-to-one correspondence with fragments of existential first-order logic without min- or max-predicate. For all fragments, we obtain effective algebraic characterizations. Moreover, we give new combinatorial proofs for the decidability of the membership problem for dot-depth 1/2 and dot-depth 1. △ Less

Submitted 7 March, 2011; originally announced March 2011.

Report number: Technical report no. 2011/03, University of Stuttgart, Computer Science MSC Class: 68Q45 ACM Class: F.4.1; F.4.3

Regular Ideal Languages and Their Boolean Combinations

Authors: Franz Jahn, Manfred Kufleitner, Alexander Lauser

Abstract: We consider ideals and Boolean combinations of ideals. For the regular languages within these classes we give expressively complete automaton models. In addition, we consider general properties of regular ideals and their Boolean combinations. These properties include effective algebraic characterizations and lattice identities. In the main part of this paper we consider the following determinis… ▽ More We consider ideals and Boolean combinations of ideals. For the regular languages within these classes we give expressively complete automaton models. In addition, we consider general properties of regular ideals and their Boolean combinations. These properties include effective algebraic characterizations and lattice identities. In the main part of this paper we consider the following deterministic one-way automaton models: unions of flip automata, weak automata, and Staiger-Wagner automata. We show that each of these models is expressively complete for regular Boolean combination of right ideals. Right ideals over finite words resemble the open sets in the Cantor topology over infinite words. An omega-regular language is a Boolean combination of open sets if and only if it is recognizable by a deterministic Staiger-Wagner automaton; and our result can be seen as a finitary version of this classical theorem. In addition, we also consider the canonical automaton models for right ideals, prefix-closed languages, and factorial languages. In the last section, we consider a two-way automaton model which is known to be expressively complete for two-variable first-order logic. We show that the above concepts can be adapted to these two-way automata such that the resulting languages are the right ideals (resp. prefix-closed languages, resp. Boolean combinations of right ideals) definable in two-variable first-order logic. △ Less

Submitted 25 May, 2012; v1 submitted 24 February, 2011; originally announced February 2011.

Comments: Presented at CIAA 2012

MSC Class: 68Q45 ACM Class: F.1.1; F.4.1

Languages of Dot-depth One over Infinite Words

Authors: Manfred Kufleitner, Alexander Lauser

Abstract: Over finite words, languages of dot-depth one are expressively complete for alternation-free first-order logic. This fragment is also known as the Boolean closure of existential first-order logic. Here, the atomic formulas comprise order, successor, minimum, and maximum predicates. Knast (1983) has shown that it is decidable whether a language has dot-depth one. We extend Knast's result to infinit… ▽ More Over finite words, languages of dot-depth one are expressively complete for alternation-free first-order logic. This fragment is also known as the Boolean closure of existential first-order logic. Here, the atomic formulas comprise order, successor, minimum, and maximum predicates. Knast (1983) has shown that it is decidable whether a language has dot-depth one. We extend Knast's result to infinite words. In particular, we describe the class of languages definable in alternation-free first-order logic over infinite words, and we give an effective characterization of this fragment. This characterization has two components. The first component is identical to Knast's algebraic property for finite words and the second component is a topological property, namely being a Boolean combination of Cantor sets. As an intermediate step we consider finite and infinite words simultaneously. We then obtain the results for infinite words as well as for finite words as special cases. In particular, we give a new proof of Knast's Theorem on languages of dot-depth one over finite words. △ Less

Submitted 1 April, 2011; v1 submitted 21 January, 2011; originally announced January 2011.

Comments: Presented at LICS 2011

MSC Class: 03D05; 68Q45 ACM Class: F.4.1; F.4.3

First-order Fragments with Successor over Infinite Words

Authors: Jakub Kallas, Manfred Kufleitner, Alexander Lauser

Abstract: We consider fragments of first-order logic and as models we allow finite and infinite words simultaneously. The only binary relations apart from equality are order comparison < and the successor predicate +1. We give characterizations of the fragments Sigma2 = Sigma2[<,+1] and FO2 = FO2[<,+1] in terms of algebraic and topological properties. To this end we introduce the factor topology over infini… ▽ More We consider fragments of first-order logic and as models we allow finite and infinite words simultaneously. The only binary relations apart from equality are order comparison < and the successor predicate +1. We give characterizations of the fragments Sigma2 = Sigma2[<,+1] and FO2 = FO2[<,+1] in terms of algebraic and topological properties. To this end we introduce the factor topology over infinite words. It turns out that a language L is in the intersection of FO2 and Sigma2 if and only if L is the interior of an FO2 language. Symmetrically, a language is in the intersection of FO2 and Pi2 if and only if it is the topological closure of an FO2 language. The fragment Delta2, which by definition is the intersection of Sigma2 and Pi2 contains exactly the clopen languages in FO2. In particular, over infinite words Delta2 is a strict subclass of FO2. Our characterizations yield decidability of the membership problem for all these fragments over finite and infinite words; and as a corollary we also obtain decidability for infinite words. Moreover, we give a new decidable algebraic characterization of dot-depth 3/2 over finite words. Decidability of dot-depth 3/2 over finite words was first shown by Glaßer and Schmitz in STACS 2000, and decidability of the membership problem for FO2 over infinite words was shown 1998 by Wilke in his habilitation thesis whereas decidability of Sigma2 over infinite words was not known before. △ Less

Submitted 30 December, 2010; originally announced January 2011.

Comments: Presented at STACS 2011

Report number: Technical report no. 2010/08, Formal Methods in Computer Science (FMI), University of Stuttgart, Germany ACM Class: F.4.1; F.4.3

Partially Ordered Two-way Büchi Automata

Authors: Manfred Kufleitner, Alexander Lauser

Abstract: We introduce partially ordered two-way Büchi automata and characterize their expressive power in terms of fragments of first-order logic FO[<]. Partially ordered two-way Büchi automata are Büchi automata which can change the direction in which the input is processed with the constraint that whenever a state is left, it is never re-entered again. Nondeterministic partially ordered two-way Büchi aut… ▽ More We introduce partially ordered two-way Büchi automata and characterize their expressive power in terms of fragments of first-order logic FO[<]. Partially ordered two-way Büchi automata are Büchi automata which can change the direction in which the input is processed with the constraint that whenever a state is left, it is never re-entered again. Nondeterministic partially ordered two-way Büchi automata coincide with the first-order fragment Sigma2. Our main contribution is that deterministic partially ordered two-way Büchi automata are expressively complete for the first-order fragment Delta2. As an intermediate step, we show that deterministic partially ordered two-way Büchi automata are effectively closed under Boolean operations. A small model property yields coNP-completeness of the emptiness problem and the inclusion problem for deterministic partially ordered two-way Büchi automata. △ Less

Submitted 25 August, 2011; v1 submitted 14 June, 2010; originally announced June 2010.

Comments: The results of this paper were presented at CIAA 2010; University of Stuttgart, Computer Science

Report number: TR no. 2010/03 MSC Class: 68Q45 ACM Class: F.1.1; F.4.1

Rankers over Infinite Words

Authors: Luc Dartois, Manfred Kufleitner, Alexander Lauser

Abstract: We consider the four fragments FO2, the intersection of Sigma2 and FO2, the intersection of Pi2 and FO2, and Delta2 of first-order logic FO[<] over finite and infinite words. For all four fragments, we give characterizations in terms of rankers. In particular, we generalize the notion of a ranker to infinite words in two possible ways. Both extensions are natural in the sense that over finite word… ▽ More We consider the four fragments FO2, the intersection of Sigma2 and FO2, the intersection of Pi2 and FO2, and Delta2 of first-order logic FO[<] over finite and infinite words. For all four fragments, we give characterizations in terms of rankers. In particular, we generalize the notion of a ranker to infinite words in two possible ways. Both extensions are natural in the sense that over finite words, they coincide with classical rankers and over infinite words, they both have the full expressive power of FO2. Moreover, the first extension of rankers admits a characterization of the intersection of Sigma2 and FO2 while the other leads to a characterization of the intersection of Pi2 and FO2. Both versions of rankers yield characterizations of the fragment Delta2. As a byproduct, we also obtain characterizations based on unambiguous temporal logic and unambiguous interval temporal logic. △ Less

Submitted 4 May, 2010; originally announced May 2010.

Comments: To be presented at the 14th Int. Conference on Developments in Language Theory (DLT 2010).

Report number: TR no. 2010/01, University of Stuttgart, Computer Science MSC Class: 68Q45 ACM Class: F.4.1; F.4.3

On Bijective Variants of the Burrows-Wheeler Transform

Authors: Manfred Kufleitner

Abstract: The sort transform (ST) is a modification of the Burrows-Wheeler transform (BWT). Both transformations map an arbitrary word of length n to a pair consisting of a word of length n and an index between 1 and n. The BWT sorts all rotation conjugates of the input word, whereas the ST of order k only uses the first k letters for sorting all such conjugates. If two conjugates start with the same pref… ▽ More The sort transform (ST) is a modification of the Burrows-Wheeler transform (BWT). Both transformations map an arbitrary word of length n to a pair consisting of a word of length n and an index between 1 and n. The BWT sorts all rotation conjugates of the input word, whereas the ST of order k only uses the first k letters for sorting all such conjugates. If two conjugates start with the same prefix of length k, then the indices of the rotations are used for tie-breaking. Both transforms output the sequence of the last letters of the sorted list and the index of the input within the sorted list. In this paper, we discuss a bijective variant of the BWT (due to Scott), proving its correctness and relations to other results due to Gessel and Reutenauer (1993) and Crochemore, Desarmenien, and Perrin (2005). Further, we present a novel bijective variant of the ST. △ Less

Submitted 3 August, 2009; originally announced August 2009.

Comments: 15 pages, presented at the Prague Stringology Conference 2009 (PSC 2009)

ACM Class: E.4; F.2.2

Fragments of first-order logic over infinite words

Authors: Volker Diekert, Manfred Kufleitner

Abstract: We give topological and algebraic characterizations as well as language theoretic descriptions of the following subclasses of first-order logic FO[<] for omega-languages: Sigma_2, FO^2, the intersection of FO^2 and Sigma_2, and Delta_2 (and by duality Pi_2 and the intersection of FO^2 and Pi_2). These descriptions extend the respective results for finite words. In particular, we relate the above… ▽ More We give topological and algebraic characterizations as well as language theoretic descriptions of the following subclasses of first-order logic FO[<] for omega-languages: Sigma_2, FO^2, the intersection of FO^2 and Sigma_2, and Delta_2 (and by duality Pi_2 and the intersection of FO^2 and Pi_2). These descriptions extend the respective results for finite words. In particular, we relate the above fragments to language classes of certain (unambiguous) polynomials. An immediate consequence is the decidability of the membership problem of these classes, but this was shown before by Wilke and Bojanczyk and is therefore not our main focus. The paper is about the interplay of algebraic, topological, and language theoretic properties. △ Less

Submitted 2 October, 2009; v1 submitted 16 June, 2009; originally announced June 2009.

Comments: Conference version presented at 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009

ACM Class: F.4.3; F.4.1

On Smoothed Analysis of Quicksort and Hoare's Find

Authors: Mahmoud Fouz, Manfred Kufleitner, Bodo Manthey, Nima Zeini Jahromi

Abstract: We provide a smoothed analysis of Hoare's find algorithm and we revisit the smoothed analysis of quicksort. Hoare's find algorithm - often called quickselect - is an easy-to-implement algorithm for finding the k-th smallest element of a sequence. While the worst-case number of comparisons that Hoare's find needs is quadratic, the average-case number is linear. We analyze what happens between t… ▽ More We provide a smoothed analysis of Hoare's find algorithm and we revisit the smoothed analysis of quicksort. Hoare's find algorithm - often called quickselect - is an easy-to-implement algorithm for finding the k-th smallest element of a sequence. While the worst-case number of comparisons that Hoare's find needs is quadratic, the average-case number is linear. We analyze what happens between these two extremes by providing a smoothed analysis of the algorithm in terms of two different perturbation models: additive noise and partial permutations. Moreover, we provide lower bounds for the smoothed number of comparisons of quicksort and Hoare's find for the median-of-three pivot rule, which usually yields faster algorithms than always selecting the first element: The pivot is the median of the first, middle, and last element of the sequence. We show that median-of-three does not yield a significant improvement over the classic rule: the lower bounds for the classic rule carry over to median-of-three. △ Less

Submitted 25 April, 2009; v1 submitted 24 April, 2009; originally announced April 2009.

Comments: To be presented at the 15th Int. Computing and Combinatorics Conference (COCOON 2009)

ACM Class: F.2.2

On FO2 quantifier alternation over words

Authors: Manfred Kufleitner, Pascal Weil

Abstract: We show that each level of the quantifier alternation hierarchy within FO^2[<] -- the 2-variable fragment of the first order logic of order on words -- is a variety of languages. We then use the notion of condensed rankers, a refinement of the rankers defined by Weis and Immerman, to produce a decidable hierarchy of varieties which is interwoven with the quantifier alternation hierarchy -- and c… ▽ More We show that each level of the quantifier alternation hierarchy within FO^2[<] -- the 2-variable fragment of the first order logic of order on words -- is a variety of languages. We then use the notion of condensed rankers, a refinement of the rankers defined by Weis and Immerman, to produce a decidable hierarchy of varieties which is interwoven with the quantifier alternation hierarchy -- and conjecturally equal to it. It follows that the latter hierarchy is decidable within one unit: given a formula alpha in FO^2[<], one can effectively compute an integer m such that alpha is equivalent to a formula with at most m+1 alternating blocks of quantifiers, but not to a formula with only m-1 blocks. This is a much more precise result than what is known about the quantifier alternation hierarchy within FO[<], where no decidability result is known beyond the very first levels. △ Less

Submitted 19 April, 2009; originally announced April 2009.

Journal ref: Mathematical Foundations of Computer Science 2009, slovaque, République (2009)

On the lattice of sub-pseudovarieties of DA

Authors: Manfred Kufleitner, Pascal Weil

Abstract: The wealth of information that is available on the lattice of varieties of bands, is used to illuminate the structure of the lattice of sub-pseudovarieties of DA, a natural generalization of bands which plays an important role in language theory and in logic. The main result describes a hierarchy of decidable sub-pseudovarieties of DA in terms of iterated Mal'cev products with the pseudovarieties… ▽ More The wealth of information that is available on the lattice of varieties of bands, is used to illuminate the structure of the lattice of sub-pseudovarieties of DA, a natural generalization of bands which plays an important role in language theory and in logic. The main result describes a hierarchy of decidable sub-pseudovarieties of DA in terms of iterated Mal'cev products with the pseudovarieties of definite and reverse definite semigroups. △ Less

Submitted 1 July, 2010; v1 submitted 19 April, 2009; originally announced April 2009.

Journal ref: Semigroup Forum 81 (2010) 243-254

A Proof of the Factorization Forest Theorem

Authors: Manfred Kufleitner

Abstract: We show that for every homomorphism $Γ^+ \to S$ where $S$ is a finite semigroup there exists a factorization forest of height $\leq 3 \abs{S}$. The proof is based on Green's relations. We show that for every homomorphism $Γ^+ \to S$ where $S$ is a finite semigroup there exists a factorization forest of height $\leq 3 \abs{S}$. The proof is based on Green's relations. △ Less

Submitted 26 October, 2007; originally announced October 2007.

Comments: 4 pages

ACM Class: F.4.3