Search results for "decidability"
showing 10 items of 46 documents
One-Counter Verifiers for Decidable Languages
2013
Condon and Lipton (FOCS 1989) showed that the class of languages having a space-bounded interactive proof system (IPS) is a proper subset of decidable languages, where the verifier is a probabilistic Turing machine. In this paper, we show that if we use architecturally restricted verifiers instead of restricting the working memory, i.e. replacing the working tape(s) with a single counter, we can define some IPS’s for each decidable language. Such verifiers are called two-way probabilistic one-counter automata (2pca’s). Then, we show that by adding a fixed-size quantum memory to a 2pca, called a two-way one-counter automaton with quantum and classical states (2qcca), the protocol can be spac…
FO^2 with one transitive relation is decidable
2013
We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.
A note on renewal systems
1992
Abstract A renewal system is a symbolic dynamical system generated by free concatenations of a finite set of words. In this paper we prove that, given two systems which are both renewal and Markov systems, it is decidable whether they are topologically conjugate. The proof makes use of the methods and the techniques of formal language theory.
A decidable word problem without equivalent canonical term rewriting system
1989
We present a weak associative single-axiom system having the following property: the word problem is decidable with an efficient algorithm even though there does not exist any finite equivalent canonical term rewriting system.
Forbidden words in symbolic dynamics
2000
AbstractWe introduce an equivalence relation≃between functions from N to N. By describing a symbolic dynamical system in terms of forbidden words, we prove that the≃-equivalence class of the function that counts the minimal forbidden words of a system is a topological invariant of the system. We show that the new invariant is independent from previous ones, but it is not characteristic. In the case of sofic systems, we prove that the≃-equivalence of the corresponding functions is a decidable question. As a more special application, we show, by using the new invariant, that two systems associated to Sturmian words having “different slope” are not conjugate.
Simulation is decidable for one-counter nets
1998
We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of sim…
Querying the Guarded Fragment with Transitivity
2016
We study the problem of answering a union of Boolean conjunctive queries q against a database Δ, and a logical theory φ which falls in the guarded fragment with transitive guards (GF + TG). We trace the frontier between decidability and undecidability of the problem under consideration. Surprisingly, we show that query answering under GF2 + TG, i.e., the two-variable fragment of GF + TG, is already undecidable (even without equality), whereas its monadic fragment is decidable; in fact, it is 2exptime-complete in combined complexity and coNP-complete in data complexity. We also show that for a restricted class of queries, query answering under GF+TG is decidable. © 2013 Springer-Verlag.
Quantum Finite State Automata over Infinite Words
2010
The study of finite state automata working on infinite words was initiated by Buchi [1]. Buchi discovered connection between formulas of the monadic second order logic of infinite sequences (S1S) and ω-regular languages, the class of languages over infinite words accepted by finite state automata. Few years later, Muller proposed an alternative definition of finite automata on infinite words [4]. McNaughton proved that with Muller’s definition, deterministic automata recognize all ω-regular languages [2]. Later, Rabin extended decidability result of Buchi for S1S to the monadic second order of the infinite binary tree (S2S) [5]. Rabin theorem can be used to settle a number of decision probl…
Decidability of bisimulation equivalences for parallel timer processes
1993
In this paper an abstract model of parallel timer processes (PTPs), allowing specification of temporal quantitative constraints on the behaviour of real time systems, is introduced. The parallel timer processes are defined in a dense time domain and are able to model both concurrent (with delay intervals overlapping on the time axis) and infinite behaviour. Both the strong and weak (abstracted from internal actions) bisimulation equivalence problems for PTPs are proved decidable. It is proved also that, if one provides the PTP model additionally with memory cells for moving timer value information along the time axis, the bisimulation equivalence (and even the vertex reachability) problems …
Nondeterministic operations on finite relational structures
1998
Abstract This article builds on a tutorial introduction to universal algebra for language theory (Courcelle, Theoret. Comput. Sci. 163 (1996) 1–54) and extends it in two directions. First, nondeterministic operations are considered, i.e., operations which give a set of results instead of a single one. Most of their properties concerning recognizability and equational definability carry over from the ordinary case with minor modifications. Second, inductive sets of evaluations are studied in greater detail. It seems that they are handled most naturally in the framework presented here. We consider the analogues of top-down and bottom-up tree transducers. Again, most of their closure propertie…