-
Regular languages defined by first-order formulas without quantifier alternation
Authors:
Andreas Krebs,
Howard Straubing
Abstract:
We give a simple new proof that regular languages defined by first-order sentences with no quantifier alteration can be defined by such sentences in which only regular atomic formulas appear. Earlier proofs of this fact relied on arguments from circuit complexity or algebra. Our proof is much more elementary, and uses only the most basic facts about finite automata.
We give a simple new proof that regular languages defined by first-order sentences with no quantifier alteration can be defined by such sentences in which only regular atomic formulas appear. Earlier proofs of this fact relied on arguments from circuit complexity or algebra. Our proof is much more elementary, and uses only the most basic facts about finite automata.
△ Less
Submitted 22 August, 2022;
originally announced August 2022.
-
Wreath Products of Distributive Forest Algebras
Authors:
Michael Hahn,
Andreas Krebs,
Howard Straubing
Abstract:
It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al.,(2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decid…
▽ More
It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al.,(2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decidability of PDL. We solve this problem in the case k=2: All languages recognized by forest algebras satisfying a 2-fold iterated distributive law are in PDL. Furthermore, we show that this class is decidable. This provides a novel nontrivial decidable subclass of PDL, and demonstrates the viability of the proposed approach to deciding PDL in general.
△ Less
Submitted 8 November, 2019;
originally announced November 2019.
-
Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership
Authors:
Andreas Krebs,
Kamal Lodaya,
Paritosh K. Pandya,
Howard Straubing
Abstract:
We study two extensions of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, "the letter $a$ appears between positions $x$ and $y$" and "the factor $u$ appears between positions $x$ and $y$". These are, in a sense, the simplest properties that are not expressible using…
▽ More
We study two extensions of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, "the letter $a$ appears between positions $x$ and $y$" and "the factor $u$ appears between positions $x$ and $y$". These are, in a sense, the simplest properties that are not expressible using only two variables.
We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We give effective conditions, in terms of the syntactic monoid of a regular language, for a property to be expressible in these logics. This algebraic analysis allows us to prove, among other things, that our new logics have strictly less expressive power than full first-order logic FO[<]. Our proofs required the development of novel techniques concerning factorizations of words.
△ Less
Submitted 7 September, 2020; v1 submitted 13 February, 2019;
originally announced February 2019.
-
Difference hierarchies and duality with an application to formal languages
Authors:
Célia Borlido,
Mai Gehrke,
Andreas Krebs,
Howard Straubing
Abstract:
The notion of a difference hierarchy, first introduced by Hausdorff, plays an important role in many areas of mathematics, logic and theoretical computer science such as descriptive set theory, complexity theory, and the theory of regular languages and automata. From a lattice theoretic point of view, the difference hierarchy over a bounded distributive lattice stratifies the Boolean algebra gener…
▽ More
The notion of a difference hierarchy, first introduced by Hausdorff, plays an important role in many areas of mathematics, logic and theoretical computer science such as descriptive set theory, complexity theory, and the theory of regular languages and automata. From a lattice theoretic point of view, the difference hierarchy over a bounded distributive lattice stratifies the Boolean algebra generated by it according to the minimum length of difference chains required to describe the Boolean elements. While each Boolean element is given by a finite difference chain, there is no canonical such writing in general. We show that, relative to the filter completion, or equivalently, the lattice of closed upsets of the dual Priestley space, each Boolean element over the lattice has a canonical minimum length decomposition into a Hausdorff difference. As a corollary each Boolean element over a (co-)Heyting algebra has a canonical difference chain. With a further generalization of this result involving a directed family of adjunctions with meet-semilattices, we give an elementary proof of the fact that a regular language is given by a Boolean combination of purely universal sentences using arbitrary numerical predicates if and only if it is given by a Boolean combination of purely universal sentences using only regular numerical predicates.
△ Less
Submitted 5 December, 2018;
originally announced December 2018.
-
Analysis of visitors' mobility patterns through random walk in the Louvre museum
Authors:
Yuji Yoshimura,
Roberta Sinatra,
Anne Krebs,
Carlo Ratti
Abstract:
This paper proposes a random walk model to analyze visitors' mobility patterns in a large museum. Visitors' available time makes their visiting styles different, resulting in dissimilarity in the order and number of visited places and in path sequence length. We analyze all this by comparing a simulation model and observed data, which provide us the strength of the visitors' mobility patterns. The…
▽ More
This paper proposes a random walk model to analyze visitors' mobility patterns in a large museum. Visitors' available time makes their visiting styles different, resulting in dissimilarity in the order and number of visited places and in path sequence length. We analyze all this by comparing a simulation model and observed data, which provide us the strength of the visitors' mobility patterns. The obtained results indicate that shorter stay-type visitors exhibit stronger patterns than those with the longer stay-type, confirming that the former are more selective than the latter in terms of their visitation type.
△ Less
Submitted 7 November, 2018;
originally announced November 2018.
-
Visibly Pushdown Languages and Free Profinite Algebras
Authors:
Silke Czarnetzki,
Andreas Krebs,
Klaus-Jörn Lange
Abstract:
We build a notion of algebraic recognition for visibly pushdown languages by finite algebraic objects. These come with a typical Eilenberg relationship, now between classes of visibly pushdown languages and classes of finite algebras. Building on that algebraic foundation, we further construct a topological object with one purpose being the possibility to derive a notion of equations, through whic…
▽ More
We build a notion of algebraic recognition for visibly pushdown languages by finite algebraic objects. These come with a typical Eilenberg relationship, now between classes of visibly pushdown languages and classes of finite algebras. Building on that algebraic foundation, we further construct a topological object with one purpose being the possibility to derive a notion of equations, through which it is possible to prove that some given visibly pushdown language is not part of a certain class (or to even show decidability of the membership-problem of the class in some cases). In particular, we obtain a special instance of Reiterman's theorem for pseudo-varieties. These findings are then employed on two subclasses of the visibly pushdown languages, for which we derive concrete sets of equations. For some showcase languages, these equations are utilised to prove non-membership to the previously described classes.
△ Less
Submitted 30 October, 2018;
originally announced October 2018.
-
Team Semantics for the Specification and Verification of Hyperproperties
Authors:
Andreas Krebs,
Arne Meier,
Jonni Virtema,
Martin Zimmermann
Abstract:
We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and mod…
▽ More
We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.
△ Less
Submitted 25 June, 2018; v1 submitted 25 September, 2017;
originally announced September 2017.
-
Diminishable Parameterized Problems and Strict Polynomial Kernelization
Authors:
Henning Fernau,
Till Fluschnik,
Danny Hermelin,
Andreas Krebs,
Hendrik Molter,
Rolf Niedermeier
Abstract:
Kernelization---a mathematical key concept for provably effective polynomial-time preprocessing of NP-hard problems---plays a central role in parameterized complexity and has triggered an extensive line of research. This is in part due to a lower bounds framework that allows to exclude polynomial-size kernels under the assumption of NP $\nsubseteq$ coNP$/$poly. In this paper we consider a restrict…
▽ More
Kernelization---a mathematical key concept for provably effective polynomial-time preprocessing of NP-hard problems---plays a central role in parameterized complexity and has triggered an extensive line of research. This is in part due to a lower bounds framework that allows to exclude polynomial-size kernels under the assumption of NP $\nsubseteq$ coNP$/$poly. In this paper we consider a restricted yet natural variant of kernelization, namely strict kernelization, where one is not allowed to increase the parameter of the reduced instance (the kernel) by more than an additive constant.
Building on earlier work of Chen, Flum, and Müller [Theory Comput. Syst. 2011] and develo** a general and remarkably simple framework, we show that a variety of FPT problems does not admit strict polynomial kernels under the weaker assumption of P $\neq$ NP. In particular, we show that various (multicolored) graph problems and Turing machine computation problems do not admit strict polynomial kernels unless P $=$ NP. To this end, a key concept we use are diminishable problems; these are parameterized problems that allow to decrease the parameter of the input instance by at least one in polynomial time, thereby outputting an equivalent problem instance. Finally, we study a relaxation of the notion of strict kernels and reveal its limitations.
△ Less
Submitted 25 August, 2017; v1 submitted 11 November, 2016;
originally announced November 2016.
-
On the Complexity of Bounded Context Switching
Authors:
Peter Chini,
Jonathan Kolberg,
Andreas Krebs,
Roland Meyer,
Prakash Saivasan
Abstract:
Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS.
The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of t…
▽ More
Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS.
The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of the memory (m) in O*(m^(cs)2^(cs)). This is achieved by creating instances of the easier problem Shuff which we solve via fast subset convolution. We also present a lower bound for BCS of the form m^o(cs / log(cs)), based on the exponential time hypothesis. Interestingly, closing the gap means settling a conjecture that has been open since FOCS'07. Further, we prove that BCS admits no polynomial kernel.
Next, we introduce a measure, called scheduling dimension, that captures the complexity of schedules. We study BCS parameterized by the scheduling dimension (sdim) and show that it can be solved in O*((2m)^(4sdim)4^t)$, where t is the number of threads. We consider variants of the problem for which we obtain (matching) upper and lower bounds.
△ Less
Submitted 24 April, 2017; v1 submitted 30 September, 2016;
originally announced September 2016.
-
An analysis of visitors' length of stay through noninvasive Bluetooth monitoring in the Louvre Museum
Authors:
Yuji Yoshimura,
Anne Krebs,
Carlo Ratti
Abstract:
Art Museums traditionally employ observations and surveys to enhance their knowledge of visitors' behavior and experience. However, these approaches often produce spatially and temporally limited empirical evidence and measurements. Only recently has the ubiquity of digital technologies revolutionized the ability to collect data on human behavior. Consequently, the greater availability of large-sc…
▽ More
Art Museums traditionally employ observations and surveys to enhance their knowledge of visitors' behavior and experience. However, these approaches often produce spatially and temporally limited empirical evidence and measurements. Only recently has the ubiquity of digital technologies revolutionized the ability to collect data on human behavior. Consequently, the greater availability of large-scale datasets based on quantifying visitors' behavior provides new opportunities to apply computational and comparative analytical techniques. In this paper, we attempt to analyze visitors' behavior in the Louvre Museum from anonymized longitudinal datasets collected from noninvasive Bluetooth sensors. We examine visitors' length of stay in the museum and consider this relationship with occupation density around artwork. This data analysis increases the knowledge and understanding of museum professionals related to the experience of visitors.
△ Less
Submitted 30 April, 2016;
originally announced May 2016.
-
Two-variable Logic with a Between Predicate
Authors:
Andreas Krebs,
Kamal Lodaya,
Paritosh Pandya,
Howard Straubing
Abstract:
We study an extension of FO^2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, `the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables.
We present several logics, both first-order and…
▽ More
We study an extension of FO^2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, `the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables.
We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We also give an effective necessary condition, in terms of the syntactic monoid of a regular language, for a property to be expressible in this logic. We show that this condition is also sufficient for words over a two-letter alphabet. This algebraic analysis allows us us to prove, among other things, that our new logic has strictly less expressive power than full first-order logic FO[<].
△ Less
Submitted 17 March, 2016;
originally announced March 2016.
-
Using Duality in Circuit Complexity
Authors:
Silke Czarnetzki,
Andreas Krebs
Abstract:
We investigate in a method for proving separation results for abstract classes of languages. A well established method to characterize varieties of regular languages are identities. We use a recently established generalization of these identities to non-regular languages by Gehrke, Grigorieff, and Pin: so called equations, which are capable of describing arbitrary Boolean algebras of languages.…
▽ More
We investigate in a method for proving separation results for abstract classes of languages. A well established method to characterize varieties of regular languages are identities. We use a recently established generalization of these identities to non-regular languages by Gehrke, Grigorieff, and Pin: so called equations, which are capable of describing arbitrary Boolean algebras of languages.
While the main concern of their result is the existence of these equations, we investigate in a general method that could allow to find equations for language classes in an inductive manner.
Thereto we extend an important tool -- the block product or substitution principle -- known from logic and algebra, to non-regular language classes. Furthermore, we abstract this concept by defining it directly as an operation on (non-regular) language classes. We show that this principle can be used to obtain equations for certain circuit classes, given equations for the gate types.
Concretely, we demonstrate the applicability of this method by obtaining a description via equations for all languages recognized by circuit families that contain a constant number of (inner) gates, given a description of the gate types via equations.
△ Less
Submitted 16 October, 2015;
originally announced October 2015.
-
Value Automata with Filters
Authors:
Michaël Cadilhac,
Andreas Krebs,
Nutan Limaye
Abstract:
We propose to study value automata with filters, a natural generalization of regular cost automata to nondeterminism. Models such as weighted automata and Parikh automata appear naturally as specializations. Results on the expressiveness of this model offer a general understanding of the behavior of the models that arise as special cases. A landscape of such restrictions is drawn.
We propose to study value automata with filters, a natural generalization of regular cost automata to nondeterminism. Models such as weighted automata and Parikh automata appear naturally as specializations. Results on the expressiveness of this model offer a general understanding of the behavior of the models that arise as special cases. A landscape of such restrictions is drawn.
△ Less
Submitted 8 October, 2015;
originally announced October 2015.
-
A Team Based Variant of CTL
Authors:
Andreas Krebs,
Arne Meier,
Jonni Virtema
Abstract:
We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prov…
▽ More
We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prove a PSPACE-completeness for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics.
△ Less
Submitted 14 July, 2015; v1 submitted 8 May, 2015;
originally announced May 2015.
-
The model checking fingerprints of CTL operators
Authors:
Andreas Krebs,
Arne Meier,
Martin Mundhenk
Abstract:
The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.
The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.
△ Less
Submitted 20 July, 2015; v1 submitted 18 April, 2015;
originally announced April 2015.
-
EF+EX Forest Algebras
Authors:
Andreas Krebs,
Howard Straubing
Abstract:
We examine languages of unranked forests definable using the temporal operators EF and EX. We characterize the languages definable in this logic, and various fragments thereof, using the syntactic forest algebras introduced by Bojanczyk and Walukiewicz. Our algebraic characterizations yield efficient algorithms for deciding when a given language of forests is definable in this logic. The proofs ar…
▽ More
We examine languages of unranked forests definable using the temporal operators EF and EX. We characterize the languages definable in this logic, and various fragments thereof, using the syntactic forest algebras introduced by Bojanczyk and Walukiewicz. Our algebraic characterizations yield efficient algorithms for deciding when a given language of forests is definable in this logic. The proofs are based on understanding the wreath product closures of a few small algebras, for which we introduce a general ideal theory for forest algebras. This combines ideas from the work of Bojanczyk and Walukiewicz for the analogous logics on binary trees and from early work of Stiffler on wreath product of finite semigroups.
△ Less
Submitted 4 August, 2014;
originally announced August 2014.
-
Universal covers, color refinement, and two-variable counting logic: Lower bounds for the depth
Authors:
Andreas Krebs,
Oleg Verbitsky
Abstract:
Given a connected graph $G$ and its vertex $x$, let $U_x(G)$ denote the universal cover of $G$ obtained by unfolding $G$ into a tree starting from $x$. Let $T=T(n)$ be the minimum number such that, for graphs $G$ and $H$ with at most $n$ vertices each, the isomorphism of $U_x(G)$ and $U_y(H)$ surely follows from the isomorphism of these rooted trees truncated at depth $T$. Motivated by application…
▽ More
Given a connected graph $G$ and its vertex $x$, let $U_x(G)$ denote the universal cover of $G$ obtained by unfolding $G$ into a tree starting from $x$. Let $T=T(n)$ be the minimum number such that, for graphs $G$ and $H$ with at most $n$ vertices each, the isomorphism of $U_x(G)$ and $U_y(H)$ surely follows from the isomorphism of these rooted trees truncated at depth $T$. Motivated by applications in theory of distributed computing, Norris [Discrete Appl. Math. 1995] asks if $T(n)\le n$. We answer this question in the negative by establishing that $T(n)=(2-o(1))n$. Our solution uses basic tools of finite model theory such as a bisimulation version of the Immerman-Lander 2-pebble counting game.
The graphs $G_n$ and $H_n$ we construct to prove the lower bound for $T(n)$ also show some other tight lower bounds. Both having $n$ vertices, $G_n$ and $H_n$ can be distinguished in 2-variable counting logic only with quantifier depth $(1-o(1))n$. It follows that color refinement, the classical procedure used in isomorphism testing and other areas for computing the coarsest equitable partition of a graph, needs $(1-o(1))n$ rounds to achieve color stabilization on each of $G_n$ and $H_n$. Somewhat surprisingly, this number of rounds is not enough for color stabilization on the disjoint union of $G_n$ and $H_n$, where $(2-o(1))n$ rounds are needed.
△ Less
Submitted 29 January, 2015; v1 submitted 11 July, 2014;
originally announced July 2014.
-
Small Depth Proof Systems
Authors:
Andreas Krebs,
Nutan Limaye,
Meena Mahajan,
Karteek Sreenivasaiah
Abstract:
A proof system for a language L is a function f such that Range(f) is exactly L. In this paper, we look at proofsystems from a circuit complexity point of view and study proof systems that are computationally very restricted. The restriction we study is: they can be computed by bounded fanin circuits of constant depth (NC^0), or of O(log log n) depth but with O(1) alternations (polylog AC^0). Each…
▽ More
A proof system for a language L is a function f such that Range(f) is exactly L. In this paper, we look at proofsystems from a circuit complexity point of view and study proof systems that are computationally very restricted. The restriction we study is: they can be computed by bounded fanin circuits of constant depth (NC^0), or of O(log log n) depth but with O(1) alternations (polylog AC^0). Each output bit depends on very few input bits; thus such proof systems correspond to a kind of local error-correction on a theorem-proof pair.
We identify exactly how much power we need for proof systems to capture all regular languages. We show that all regular language have polylog AC^0 proof systems, and from a previous result (Beyersdorff et al, MFCS 2011, where NC^0 proof systems were first introduced), this is tight. Our technique also shows that MAJ has polylog AC^0 proof system. We explore the question of whether TAUT has NC^0 proof systems. Addressing this question about 2TAUT, and since 2TAUT is closely related to reachability in graphs, we ask the same question about Reachability. We show that both Undirected Reachability and Directed UnReachability have NC^0 proof systems, but Directed Reachability is still open.
In the context of how much power is needed for proof systems for languages in NP, we observe that proof systems for a good fraction of languages in NP do not need the full power of AC^0; they have SAC^0 or coSAC^0 proof systems.
△ Less
Submitted 18 July, 2013;
originally announced July 2013.
-
Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy
Authors:
Christoph Berkholz,
Andreas Krebs,
Oleg Verbitsky
Abstract:
Given two structures $G$ and $H$ distinguishable in $\fo k$ (first-order logic with $k$ variables), let $A^k(G,H)$ denote the minimum alternation depth of a $\fo k$ formula distinguishing $G$ from $H$. Let $A^k(n)$ be the maximum value of $A^k(G,H)$ over $n$-element structures. We prove the strictness of the quantifier alternation hierarchy of $\fo 2$ in a strong quantitative form, namely…
▽ More
Given two structures $G$ and $H$ distinguishable in $\fo k$ (first-order logic with $k$ variables), let $A^k(G,H)$ denote the minimum alternation depth of a $\fo k$ formula distinguishing $G$ from $H$. Let $A^k(n)$ be the maximum value of $A^k(G,H)$ over $n$-element structures. We prove the strictness of the quantifier alternation hierarchy of $\fo 2$ in a strong quantitative form, namely $A^2(n)\ge n/8-2$, which is tight up to a constant factor. For each $k\ge2$, it holds that $A^k(n)>\log_{k+1}n-2$ even over colored trees, which is also tight up to a constant factor if $k\ge3$. For $k\ge 3$ the last lower bound holds also over uncolored trees, while the alternation hierarchy of $\fo 2$ collapses even over all uncolored graphs.
We also show examples of colored graphs $G$ and $H$ on $n$ vertices that can be distinguished in $\fo 2$ much more succinctly if the alternation number is increased just by one: while in $Σ_{i}$ it is possible to distinguish $G$ from $H$ with bounded quantifier depth, in $Π_{i}$ this requires quantifier depth $Ω(n^2)$. The quadratic lower bound is best possible here because, if $G$ and $H$ can be distinguished in $\fo k$ with $i$ quantifier alternations, this can be done with quantifier depth $n^{2k-2}$.
△ Less
Submitted 8 August, 2013; v1 submitted 12 December, 2012;
originally announced December 2012.
-
Streaming algorithms for recognizing nearly well-parenthesized expressions
Authors:
Andreas Krebs,
Nutan Limaye,
Srikanth Srinivasan
Abstract:
We study the streaming complexity of the membership problem of 1-turn-Dyck2 and Dyck2 when there are a few errors in the input string.
1-turn-Dyck2 with errors: We prove that there exists a randomized one-pass algorithm that given x checks whether there exists a string x' in 1-turn-Dyck2 such that x is obtained by flip** at most $k$ locations of x' using:
- O(k log n) space, O(k log n) rando…
▽ More
We study the streaming complexity of the membership problem of 1-turn-Dyck2 and Dyck2 when there are a few errors in the input string.
1-turn-Dyck2 with errors: We prove that there exists a randomized one-pass algorithm that given x checks whether there exists a string x' in 1-turn-Dyck2 such that x is obtained by flip** at most $k$ locations of x' using:
- O(k log n) space, O(k log n) randomness, and poly(k log n) time per item and with error at most 1/poly(n). - O(k^{1+epsilon} + log n) space for every 0 <= epsilon <= 1, O(log n) randomness, O(polylog(n) + poly(k)) time per item, with error at most 1/8.
Here, we also prove that any randomized one-pass algorithm that makes error at most k/n requires at least Omega(k log(n/k)) space to accept strings which are exactly k-away from strings in 1-turn-Dyck2 and to reject strings which are exactly (k+2)-away from strings in 1-turn-Dyck2. Since 1-turn-Dyck2 and the Hamming Distance problem are closely related we also obtain new upper and lower bounds for this problem.
Dyck2 with errors: We prove that there exists a randomized one-pass algorithm that given x checks whether there exists a string x' in Dyck2 such that x is obtained from x' by changing (in some restricted manner) at most k positions using:
- O(k log n + sqrt(n log n)) space, O(k log n) randomness, poly(k log n) time per element and with error at most 1/poly(n). - O(k^(1+epsilon)+ sqrt(n log n)) space for every 0 <= epsilon <= 1, O(log n) randomness, O(polylog(n) + poly(k)) time per element, with error at most 1/8.
△ Less
Submitted 1 June, 2012;
originally announced June 2012.
-
An effective characterization of the alternation hierarchy in two-variable logic
Authors:
Andreas Krebs,
Howard Straubing
Abstract:
We characterize the languages in the individual levels of the quantifier alternation hierarchy of first-order logic with two variables by identities. This implies decidability of the individual levels. More generally we show that the two-sided semidirect product of a decidable variety with the variety J is decidable.
We characterize the languages in the individual levels of the quantifier alternation hierarchy of first-order logic with two variables by identities. This implies decidability of the individual levels. More generally we show that the two-sided semidirect product of a decidable variety with the variety J is decidable.
△ Less
Submitted 22 May, 2012;
originally announced May 2012.
-
Non-definability of languages by generalized first-order formulas over (N,+)
Authors:
Andreas Krebs,
A. V. Sreejith
Abstract:
We consider first-order logic with monoidal quantifiers over words. We show that all languages with a neutral letter, definable using the addition numerical predicate are also definable with the order predicate as the only numerical predicate. Let S be a subset of monoids.
Let LS be the logic closed under quantification over the monoids in S and N be the class of neutral letter languages. Then w…
▽ More
We consider first-order logic with monoidal quantifiers over words. We show that all languages with a neutral letter, definable using the addition numerical predicate are also definable with the order predicate as the only numerical predicate. Let S be a subset of monoids.
Let LS be the logic closed under quantification over the monoids in S and N be the class of neutral letter languages. Then we show that: LS[<,+] cap N = LS[<] Our result can be interpreted as the Crane Beach conjecture to hold for the logic LS[<,+]. As a corollary of our result we get the result of Roy and Straubing that FO+MOD[<,+] collapses to FO+MOD[<].
For cyclic groups, we answer an open question of Roy and Straubing, proving that MOD[<,+] collapses to MOD[<]. Our result also shows that multiplication is necessary for Barrington's theorem to hold.
All these results can be viewed as separation results for very uniform circuit classes. For example we separate FO[<,+]-uniform CC0 from FO[<,+]-uniform ACC0.
△ Less
Submitted 4 May, 2012; v1 submitted 27 April, 2012;
originally announced April 2012.
