05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
5 results
Search Results
Item Open Access Formal language theory of logic fragments(2014) Lauser, Alexander; Diekert, Volker (Prof. Dr.)The present thesis consists of two parts. Based on syntactic closure axioms of formula sets, the first part gives a formal definition of logic fragments. It also shows the versatileness of this notion of logic fragments, inter alia, giving, C-variety descriptions of logic fragments and abstractly investigating the influence of certain predicates on the expressiveness of logic fragments. The second part considers two-variable first-order logic FO2. A combinatorial description in terms of so-called rankers is given for all full levels as well as all half levels of the quantifier alternation hierarchy of FO2 over the order predicate, both with and without the successor predicate. Also in the second part, effective algebraic criteria describing all full levels as well as all half levels of the quantifier alternation hierarchy of FO2 over several signatures are given, yielding in particular decidability of the definability problem.Item Open Access First-order fragments with successor over infinite words(2010) Kallas, Jakub; Kufleitner, Manfred; Lauser, AlexanderWe consider fragments of first-order logic and as models we allow finite andinfinite words simultaneously. The only binary relations apart from equalityare order comparison < and the successor predicate +1. We givecharacterizations of the fragments Sigma2 = Sigma2[<,+1] and FO2 = FO2[<,+1] interms of algebraic and topological properties. To this end we introduce thefactor topology over infinite words. It turns out that a language L is in theintersection of FO2 and Sigma2 if and only if L is the interior of an FO2language. Symmetrically, a language is in the intersection of FO2 and Pi2 ifand only if it is the topological closure of an FO2 language. The fragmentDelta2, which by definition is the intersection Sigma2 and Pi2 contains exactlythe clopen languages in FO2. In particular, over infinite words Delta2 is astrict subclass of FO2. Our characterizations yield decidability of themembership problem for all these fragments over finite and infinite words; andas a corollary we also obtain decidability for infinite words. Moreover, wegive a new decidable algebraic characterization of dot-depth 3/2 over finitewords. Decidability of dot-depth 3/2 over finite words was first shown by Glaßer andSchmitz in STACS 2000, and decidability of the membership problem for FO2 overinfinite words was shown 1998 by Wilke in his habilitation thesis whereasdecidability of Sigma2 over infinite words was not known before.Item Open Access Rankers over infinite words(2010) Dartois, Luc; Kufleitner, Manfred; Lauser, AlexanderWe consider the 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.Item Open Access Partially ordered two-way Büchi automata(2010) Kufleitner, Manfred; Lauser, AlexanderWe introduce partially ordered two-way Büchi automata over infinite words. As for finite words, the nondeterministic variant recognizes the fragment Sigma2 of first-order logic FO[<] and the deterministic version yields the Delta2-definable omega-languages. As a byproduct of our results, we show that deterministic partially ordered two-way Büchi automata are effectively closed under Boolean operations. In addition, we have coNP-completeness results for the emptiness problem and the inclusion problem over deterministic partially ordered two-way Büchi automata.Item Open Access Around dot-depth one(2011) Kufleitner, Manfred; Lauser, AlexanderThe 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.