10 Search Results for "Kufleitner, Manfred"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.130
The Theory of Concatenation over Finite Models

Authors: Dominik D. Freydenberger and Liat Peterfreund

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We propose FC, a new logic on words that combines finite model theory with the theory of concatenation - a first-order logic that is based on word equations. Like the theory of concatenation, FC is built around word equations; in contrast to it, its semantics are defined to only allow finite models, by limiting the universe to a word and all its factors. As a consequence of this, FC has many of the desirable properties of FO on finite models, while being far more expressive than FO[<]. Most noteworthy among these desirable properties are sufficient criteria for efficient model checking, and capturing various complexity classes by adding operators for transitive closures or fixed points. Not only does FC allow us to obtain new insights and techniques for expressive power and efficient evaluation of document spanners, but it also provides a general framework for logic on words that also has potential applications in other areas.
Cite as

Dominik D. Freydenberger and Liat Peterfreund. The Theory of Concatenation over Finite Models. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 130:1-130:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{freydenberger_et_al:LIPIcs.ICALP.2021.130,
  author =	{Freydenberger, Dominik D. and Peterfreund, Liat},
  title =	{{The Theory of Concatenation over Finite Models}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{130:1--130:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.130},
  URN =		{urn:nbn:de:0030-drops-141997},
  doi =		{10.4230/LIPIcs.ICALP.2021.130},
  annote =	{Keywords: finite model theory, word equations, descriptive complexity, model checking, document spanners}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.62
Testing Simon's congruence

Authors: Lukas Fleischer and Manfred Kufleitner

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
Piecewise 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 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 ~_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).
Cite as

Lukas Fleischer and Manfred Kufleitner. Testing Simon's congruence. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 62:1-62:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fleischer_et_al:LIPIcs.MFCS.2018.62,
  author =	{Fleischer, Lukas and Kufleitner, Manfred},
  title =	{{Testing Simon's congruence}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{62:1--62:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.62},
  URN =		{urn:nbn:de:0030-drops-96445},
  doi =		{10.4230/LIPIcs.MFCS.2018.62},
  annote =	{Keywords: regular language, scattered subword, piecewise testability, string algorithm}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.30
The Intersection Problem for Finite Monoids

Authors: Lukas Fleischer and Manfred Kufleitner

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

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

Lukas Fleischer and Manfred Kufleitner. The Intersection Problem for Finite Monoids. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 30:1-30:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fleischer_et_al:LIPIcs.STACS.2018.30,
  author =	{Fleischer, Lukas and Kufleitner, Manfred},
  title =	{{The Intersection Problem for Finite Monoids}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{30:1--30:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.30},
  URN =		{urn:nbn:de:0030-drops-85079},
  doi =		{10.4230/LIPIcs.STACS.2018.30},
  annote =	{Keywords: intersection problem, finite monoid, recognizing morphism, complexity}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.127
Solutions of Word Equations Over Partially Commutative Structures

Authors: Volker Diekert, Artur Jez, and Manfred Kufleitner

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
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.
Cite as

Volker Diekert, Artur Jez, and Manfred Kufleitner. Solutions of Word Equations Over Partially Commutative Structures. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 127:1-127:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{diekert_et_al:LIPIcs.ICALP.2016.127,
  author =	{Diekert, Volker and Jez, Artur and Kufleitner, Manfred},
  title =	{{Solutions of Word Equations Over Partially Commutative Structures}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{127:1--127:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.127},
  URN =		{urn:nbn:de:0030-drops-62624},
  doi =		{10.4230/LIPIcs.ICALP.2016.127},
  annote =	{Keywords: Word equations, EDT0L language, trace monoid, right-angled Artin group, partial commutation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.112
Efficient Algorithms for Morphisms over Omega-Regular Languages

Authors: Lukas Fleischer and Manfred Kufleitner

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

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, 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.
Cite as

Lukas Fleischer and Manfred Kufleitner. Efficient Algorithms for Morphisms over Omega-Regular Languages. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 112-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fleischer_et_al:LIPIcs.FSTTCS.2015.112,
  author =	{Fleischer, Lukas and Kufleitner, Manfred},
  title =	{{Efficient Algorithms for Morphisms over Omega-Regular Languages}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{112--124},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.112},
  URN =		{urn:nbn:de:0030-drops-56200},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.112},
  annote =	{Keywords: B\"{u}chi automata, omega-regular language, syntactic semigroup, recognizing morphism, MSO}
}
Document
DOI: 10.4230/LIPIcs.STACS.2014.374
Ehrenfeucht-Fraïssé Games on Omega-Terms

Authors: Martin Huschenbett and Manfred Kufleitner

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

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 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].
Cite as

Martin Huschenbett and Manfred Kufleitner. Ehrenfeucht-Fraïssé Games on Omega-Terms. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 374-385, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{huschenbett_et_al:LIPIcs.STACS.2014.374,
  author =	{Huschenbett, Martin and Kufleitner, Manfred},
  title =	{{Ehrenfeucht-Fra\"{i}ss\'{e} Games on Omega-Terms}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{374--385},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.374},
  URN =		{urn:nbn:de:0030-drops-44729},
  doi =		{10.4230/LIPIcs.STACS.2014.374},
  annote =	{Keywords: regular language, first-order logic, finite monoid, Ehrenfeucht-Fra\"{i}ss\'{e} games, pseudoidentity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2013.305
Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable

Authors: Manfred Kufleitner and Alexander Lauser

Published in: LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)

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 for a given regular language and a non-negative integer~$m$ 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.
Cite as

Manfred Kufleitner and Alexander Lauser. Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 305-316, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{kufleitner_et_al:LIPIcs.STACS.2013.305,
  author =	{Kufleitner, Manfred and Lauser, Alexander},
  title =	{{Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable}},
  booktitle =	{30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)},
  pages =	{305--316},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-50-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{20},
  editor =	{Portier, Natacha and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.305},
  URN =		{urn:nbn:de:0030-drops-39438},
  doi =		{10.4230/LIPIcs.STACS.2013.305},
  annote =	{Keywords: automata theory, semigroups, regular languages, first-order logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.426
The FO2 alternation hierarchy is decidable

Authors: Manfred Kufleitner and Pascal Weil

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We consider the two-variable fragment FO2[<] of first-order logic over finite words. Numerous characterizations of this class are known. Therien and Wilke have shown that it is decidable whether a given regular language is definable in FO2[<]. From a practical point of view, as shown by Weis, FO2[<] is interesting since its satisfiability problem is in NP. Restricting the number of quantifier alternations yields an infinite hierarchy inside the class of FO2[<]-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 FO2[<]-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, Therien, and Vollmer.
Cite as

Manfred Kufleitner and Pascal Weil. The FO2 alternation hierarchy is decidable. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 426-439, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kufleitner_et_al:LIPIcs.CSL.2012.426,
  author =	{Kufleitner, Manfred and Weil, Pascal},
  title =	{{The FO2 alternation hierarchy is decidable}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{426--439},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.426},
  URN =		{urn:nbn:de:0030-drops-36888},
  doi =		{10.4230/LIPIcs.CSL.2012.426},
  annote =	{Keywords: first-order logic, regular language, automata theory, semigroup, ranker}
}
Document
DOI: 10.4230/LIPIcs.STACS.2011.356
First-order Fragments with Successor over Infinite Words

Authors: Jakub Kallas, Manfred Kufleitner, and Alexander Lauser

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

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 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 $L$ is in FO^2 cap Sigma_2 if and only if $L$ 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.
Cite as

Jakub Kallas, Manfred Kufleitner, and Alexander Lauser. First-order Fragments with Successor over Infinite Words. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 356-367, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kallas_et_al:LIPIcs.STACS.2011.356,
  author =	{Kallas, Jakub and Kufleitner, Manfred and Lauser, Alexander},
  title =	{{First-order Fragments with Successor over Infinite Words}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{356--367},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.356},
  URN =		{urn:nbn:de:0030-drops-30267},
  doi =		{10.4230/LIPIcs.STACS.2011.356},
  annote =	{Keywords: infinite words, regular languages, first-order logic, automata theory, semi-groups, topology}
}
Document
DOI: 10.4230/LIPIcs.STACS.2009.1818
Fragments of First-Order Logic over Infinite Words

Authors: Volker Diekert and Manfred Kufleitner

Published in: LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

Abstract
We give topological and algebraic characterizations as well as language theoretic descriptions of the following subclasses of first-order logic $\mathrm{FO}[<]$ for $\omega$-languages: $\Sigma_2$, $\Delta_2$, $\mathrm{FO}^2 \cap \Sigma_2$ (and by duality $\mathrm{FO}^2 \cap \Pi_2$), and $\mathrm{FO}^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 (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.
Cite as

Volker Diekert and Manfred Kufleitner. Fragments of First-Order Logic over Infinite Words. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 325-336, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{diekert_et_al:LIPIcs.STACS.2009.1818,
  author =	{Diekert, Volker and Kufleitner, Manfred},
  title =	{{Fragments of First-Order Logic over Infinite Words}},
  booktitle =	{26th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{325--336},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-09-5},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{3},
  editor =	{Albers, Susanne and Marion, Jean-Yves},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1818},
  URN =		{urn:nbn:de:0030-drops-18185},
  doi =		{10.4230/LIPIcs.STACS.2009.1818},
  annote =	{Keywords: Infinite words, Regular languages, First-order logic, Automata theory, Semigroups, Topology}
}
  • Refine by Author
  • 9 Kufleitner, Manfred
  • 3 Fleischer, Lukas
  • 2 Diekert, Volker
  • 2 Lauser, Alexander
  • 1 Freydenberger, Dominik D.
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Combinatorics on words
  • 1 Theory of computation → Database query languages (principles)
  • 1 Theory of computation → Finite Model Theory
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic and databases

  • Refine by Keyword
  • 4 first-order logic
  • 3 automata theory
  • 3 regular language
  • 2 finite monoid
  • 2 recognizing morphism
  • Show More...

  • Refine by Type
  • 10 document

  • Refine by Publication Year
  • 2 2018
  • 1 2009
  • 1 2011
  • 1 2012
  • 1 2013
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact