1,042 research outputs found
Efficient Algorithms for Morphisms over Omega-Regular Languages
No full textMorphisms 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
Testing Simon's congruence
No full textPiecewise testable languages are a subclass of the regular languages. There are many equivalent ways of defining them; Simon's congruence ~_k is one of the most classical approaches. Two words are ~_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 ~_k-classes.
For each equivalence class of ~_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 ~_k. We present an algorithm for computing the canonical representative of the ~_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 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 ~_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 ~_k-equivalent (with k being part of the input)
The Intersection Problem for Finite Monoids
No full textWe 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 Thérien
Fragments of First-Order Logic over Infinite Words
No full textWe give topological and algebraic characterizations as well as language theoretic descriptions of the following subclasses of first-order logic for -languages: , , (and by duality ), and . 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 (1998) and Boja{\'n}czyk (2008) and is therefore not our main focus. The paper is about the interplay of algebraic, topological, and language theoretic properties
Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable
No full textWe 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 for a given regular language and a non-negative integer~ it is decidable 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] quantifier alternation hierarchy
Solutions of Word Equations Over Partially Commutative Structures
No full textWe give NSPACE(n*log(n)) algorithms solving the following decision problems. Satisfiability: Is the given equation over a free partially commutative monoid with involution (resp. a free partially commutative group) solvable? Finiteness: Are there only finitely many solutions of such an equation? PSPACE algorithms with worse complexities for the first problem are known, but so far, a PSPACE algorithm for the second problem was out of reach. Our results are much stronger: Given such an equation, its solutions form an EDT0L language effectively representable in NSPACE(n*log(n)). In particular, we give an effective description of the set of all solutions for equations with constraints in free partially commutative monoids and groups
Efficient algorithms for morphisms over omega-regular languages
No full text© Lukas Fleischer and Manfred Kufleitner;. Morphisms to finite semigroups can be used for recognizing omega-regular languages. The socalled 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
Ehrenfeucht-Fraïssé Games on Omega-Terms
No full textFragments 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]
First-order Fragments with Successor over Infinite Words
No full textWe 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 Sigma_2 = Sigma_2[<,+1] and FO^2 = FO^2[<,+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 is in FO^2 cap Sigma_2 if and only if is the interior of an FO^2 language. Symmetrically, a language is in FO^2 cap Pi_2 if and only if it is the topological closure of an FO^2 language. The fragment Delta_2 = Sigma_2 cap Pi_2 contains exactly the clopen languages in FO^2. In particular, over infinite words Delta_2 is a strict subclass of FO^2. 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 Glasser and Schmitz in STACS 2000, and decidability of the membership problem for FO^2 over infinite words was shown 1998 by Wilke in his habilitation thesis whereas decidability of Sigma_2 over infinite words is new
Solutions of word equations over partially commutative structures
No full text© Volker Diekert, Artur Jez, and Manfred Kufleitner. We give NSPACE(n log n) algorithms solving the following decision problems. Satisfiability: Is the given equation over a free partially commutative monoid with involution (resp. a free partially commutative group) solvable? Finiteness: Are there only finitely many solutions of such an equation? PSPACE algorithms with worse complexities for the first problem are known, but so far, a PSPACE algorithm for the second problem was out of reach. Our results are much stronger: Given such an equation, its solutions form an EDT0L language effectively representable in NSPACE(n log n). In particular, we give an effective description of the set of all solutions for equations with constraints in free partially commutative monoids and groups
- …
