Complexity of Weak Bisimilarity and Regularity for BPA and BPP

It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP have been demonstrated by Stribrna. Mayr achieved recently a result, saying that weak bisimilarity for BPP is Π^p₂-hard. We improve this lower bound to PSPACE, moreover for the restricted class of normed BPP.Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a Π^p₂-hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and co-NP-hardness.In each of the bisimulation/regularity problems we consider also the classes of normed processes.Note: full version of the paper appears as [18].     

Deciding probabilistic bisimilarity over infinite-state probabilistic systems

We prove that probabilistic bisimilarity is decidable over probabilistic extensions of BPA and BPP processes. For normed subclasses of probabilistic BPA and BPP processes we obtain polynomial-time algorithms. Further, we show that probabilistic bisimilarity between probabilistic pushdown automata and finite-state systems is decidable in exponential time. If the number of control states in PDA is bounded by a fixed constant, then the algorithm needs only polynomial time. The work has been supported by the research centre Institute for Theoretical Computer Science (ITI), project No. 1M0545.     

Refining the Undecidability Border of Weak Bisimilarity

Weak bisimilarity is one of the most studied behavioural equivalences. This equivalence is undecidable for pushdown processes (PDA), process algebras (PA), and multiset automata (MSA, also known as parallel pushdown processes, PPDA). Its decidability is an open question for basic process algebras (BPA) and basic parallel processes (BPP). We move the undecidability border towards these classes by showing that the equivalence remains undecidable for weakly extended versions of BPA and BPP. In fact, we show that the weak bisimulation equivalence problem is undecidable even for normed subclasses of BPA and BPP extended with a finite constraint system.     

Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes and normed basic parallel processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.     

Comparing expressibility of normed BPA and normed BPP processes

We present an exact characterization of those transition systems which can be equivalently (up to bisimilarity) defined by the syntax of normed BPA and normed BPP processes. We give such a characterization for the subclasses of normed BPA and normed BPP processes as well. Next we demonstrate the decidability of the problem whether for a given normed BPA process there is some unspecified normed BPP process such that and are bisimilar. The algorithm is polynomial. Furthermore, we show that if the answer to the previous question is positive, then (an example of) the process is effectively constructible. Analogous algorithms are provided for normed BPP processes. Simplified versions of the mentioned algorithms which work for normed BPA and normed BPP are given too. As a simple consequence we obtain the decidability of bisimilarity in the union of normed BPA and normed BPP processes. Received: 3 June 1997     

Partially-commutative context-free processes: Expressibility and tractability

Bisimulation equivalence is decidable in polynomial time for both sequential and commutative normed context-free processes, known as BPA and BPP, respectively. Despite apparent similarity between the two classes, different algorithmic techniques were used in each case. We provide one polynomial-time algorithm that works in a superclass of both normed BPA and BPP. It is derived in the setting of partially-commutative context-free processes, a new process class introduced in the paper. It subsumes both BPA and BPP and seems to be of independent interest. Expressibility issue of the new class, in comparison with the normed PA class, is also tackled in the paper.     

Weak bisimilarity and regularity of context-free processes is EXPTIME-hard

We show that checking weak bisimulation equivalence of two context-free processes (also called BPA-processes) is EXPTIME-hard, even under the condition that the processes are normed. Furthermore, checking weak regularity (finiteness up to weak bisimilarity) for context-free processes is EXPTIME-hard as well. Adding a finite control of the minimal non-trivial size of 2 to the BPA process already makes weak bisimilarity undecidable.     

Decidability of Branching Bisimulation on Normed Commutative Context-Free Processes

We investigate normed commutative context-free processes (Basic Parallel Processes). We show that branching bisimilarity admits the bounded response property: in the Bisimulation Game, Duplicator always has a response leading to a process of size linearly bounded with respect to the Spoiler’s process. The linear bound is effective, which leads to decidability of branching bisimilarity. For weak bisimilarity, we are able merely to show existence of some linear bound, which is not sufficient for decidability. We conjecture however that the same effective bound holds for weak bisimilarity as well. We suppose that further elaboration of novel techniques developed in this paper may be sufficient to demonstrate decidability.     

A relationship between difference hierarchies and relativized polynomial hierarchies

Chang and Kadin have shown that if the difference hierarchy over NP collapses to levelk, then the polynomial hierarchy (PH) is equal to thekth level of the difference hierarchy over ₂ ^p . We simplify their poof and obtain a slightly stronger conclusion: if the difference hierarchy over NP collapses to levelk, then PH collapses to (P _(k–1) ^NP )^NP, the class of sets recognized in polynomial time withk – 1 nonadaptive queries to a set in NP^NP and an unlimited number of queries to a set in NP. We also extend the result to classes other than NP: For any classC that has _m ^p -complete sets and is closed under _conj ^p -and _m ^NP -reductions (alternatively, closed under _disj ^p -and _m ^co-NP -reductions), if the difference hierarchy overC collapses to levelk, then PH ^C = (P _(k–1)–tt ^NP ) ^C . Then we show that the exact counting class C_P is closed under _disj ^p - and _m ^co-NP -reductions. Consequently, if the difference hierarchy over C_P collapses to levelk, then PH^PP(= PH^C_P) is equal to (P _(k–1)–tt ^NP )^PP. In contrast, the difference hierarchy over the closely related class PP is known to collapse.Finally we consider two ways of relativizing the bounded query class P _k–tt ^NP : the restricted relativization P _k–tt ^{NP C} and the full relativization (P _k–tt ^NP ) ^C . IfC is NP-hard, then we show that the two relativizations are different unless PH ^C collapses.Richard Beigel was supported in part by NSF Grants CCR-8808949 and CCR-8958528. Richard Chang was supported in part by NSF Research Grant CCR 88-23053. This work was done while Mitsunori Ogiwara was at the Department of Information Science, Tokyo Institute of Technology, Tokyo, Japan.     

The most nonelementary theory

We give a direct proof by generic reduction that testing validity of formulas in a decidable rudimentary theory Ω of finite typed sets (Henkin, Fundamenta Mathematicæ 52 (1963) 323–344) requires space and time exceeding infinitely often(1)where n denotes the length of input. This gives the highest currently known lower bound for a decidable logical theory and affirmatively settles Problem 10.13 from (Compton and Henson, Ann. Pure Applied Logic 48 (1990) 1–79):

Is there a “natural” decidable theory with a lower bound of the form exp_∞(f(n)), where f is not linearly bounded?

The highest previously known lower (and upper) bounds for “natural” decidable theories, like WS1S, S2S, are of the form exp_∞(dn), with just linearly growing stacks of twos.Originally, the lower bound (1) for Ω was settled in (12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), 1997, 294–305) using the powerful uniform lower bounds method due to Compton and Henson, and probably would never be discovered otherwise. Although very concise, the original proof has certain gaps, because the method was pushed out of the limits it was originally designed and intended for, and some hidden assumptions were violated. This results in slightly weaker bounds—the stack of twos in (1) grows subexponentially, but superpolynomially, namely, as for formulas with fixed quantifier prefix, or as 2^cn/log(n) for formulas with varying prefix. The independent direct proof presented in this paper closes the gaps and settles the originally claimed lower bound (1) for the minimally typed, succinct version of Ω.     

Simulation Preorder over Simple Process Algebras

We consider the problem of simulation preorder/equivalence between infinite-state processes and finite-state ones. First, we describe a general method how to utilize the decidability of bisimulation problems to solve (certain instances of) the corresponding simulation problems. For certain process classes, the method allows us to design effective reductions of simulation problems to their bisimulation counterparts and some new decidability results for simulation have already been obtained in this way. Then we establish the decidability border for the problem of simulation preorder/equivalence between infinite-state processes and finite-state ones w.r.t. the hierarchy of process rewrite systems. In particular, we show that simulation preorder (in both directions) and simulation equivalence are decidable in EXPTIME between pushdown processes and finite-state ones. On the other hand, simulation preorder is undecidable between PA and finite-state processes in both directions. These results also hold for those PA and finite-state processes which are deterministic and normed, and thus immediately extend to trace preorder. Regularity (finiteness) w.r.t. simulation and trace equivalence is also shown to be undecidable for PA. Finally, we prove that simulation preorder (in both directions) and simulation equivalence are intractable between all classes of infinite-state systems (in the hierarchy of process rewrite systems) and finite-state ones. This result is obtained by showing that the problem whether a BPA (or BPP) process simulates a finite-state one is PSPACE-hard and the other direction is co -hard; consequently, simulation equivalence between BPA (or BPP) and finite-state processes is also co -hard.     

Deciding Branching Bisimilarity of Normed Context-Free Processes Is in Σ2

We show that the problem of deciding branching bisimulation equivalence for normed context-free processes is in Σ^p₂, the second level of the polynomial-time hierarchy, and hence in PSPACE. We also show that minimization of normed context-free process graphs is in PSPACE.     

Optimal Algorithms for the Coverability, the Subword, the Containment, and the Equivalence Problems for Commutative Semigroups

In this paper, we present decision procedures for the coverability, the subword, the containment, and the equivalence problems for commutative semigroups. These procedures require at most space 2^c·n, where n is the size of the problem instance, and c is some problem independent constant. Furthermore, we show that the exponential space hardness of the above problems follows from the work of Mayr and Meyer. Thus, the presented algorithms are space optimal. Our results close the gap between the 2^{c′·n·log n} space upper bound, shown by Rackoff for the coverability problem and shown by Huynh for the containment and the equivalence problems, and the exponential space lower bound resulting from the corresponding bound for the uniform word problem established by Mayr and Meyer.     

The Difference between Polynomial-Time Many-One and Truth-Table Reducibilities on Distributional Problems

In this paper we separate many-one reducibility from truth-table reducibility for distributional problems in DistNP under the hypothesis that P ≠ NP . As a first example we consider the 3-Satisfiability problem (3SAT) with two different distributions on 3CNF formulas. We show that 3SAT with a version of the standard distribution is truth-table reducible but not many-one reducible to 3SAT with a less redundant distribution unless P = NP . We extend this separation result and define a distributional complexity class C with the following properties: (1) C is a subclass of DistNP, this relation is proper unless P = NP. (2) C contains DistP, but it is not contained in AveP unless DistNP \subseteq AveZPP. (3) C has a ≤ ^p _m -complete set. (4) C has a ≤ ^p _tt -complete set that is not ≤ ^p _m -complete unless P = NP. This shows that under the assumption that P ≠ NP, the two completeness notions differ on some nontrivial subclass of DistNP.     

On the Power of DNA-Computing

Adleman used biological manipulations with DNA strings to solve some instances of the Directed Hamiltonian Path Problem. Lipton showed how to extend this idea to solve any NP problem. We prove that exactly the problems in P^NP=Δ^p₂can be solved in polynomial time using Lipton's model. Various modifications of Lipton's model, based on other DNA manipulations, are investigated systematically, and it is proved that their computational power in polynomial time can be characterized by one of the complexity classes P,Δ^p₂, orΔ^p₃.     

Isomorphic Implication

We study the isomorphic implication problem for Boolean constraints. We show that this is a natural analog of the subgraph isomorphism problem. We prove that, depending on the set of constraints, this problem is in P, or is NP-complete, or is NP-hard, coNP-hard, and in P_‖^NP. We show how to extend the NP-hardness and coNP-hardness to P_‖^NP-hardness for some cases, and conjecture that this can be done in all cases. Supported in part by grants NSF-CCR-0311021 and DFG VO 630/5-1 and VO 630/5-2. An extended abstract of this paper appears in Proceedings of the 30th International Symposium on Mathematical Foundations of Computer Science (MFCS 2005), pp. 119–130, Springer-Verlag Lecture Notes in Computer Science #3618, August 2005. Work of M. Bauland done in part while visiting CASCI’s Laboratory for Complexity at Rochester Institute of Technology. Work of E. Hemaspaandra done in part while on sabbatical at the University of Rochester.     

Bounds on element order in rings Zm with divisors of zero

If p is a prime, integer ring Z_p has exactly ((p)) generating elements ω, each of which has maximal index I_p(ω) = (p) = p − 1. But, if m = Π^R_{J = 1} p^αJ_J is composite, it is possible that Z_m does not possess a generating element, and the maximal index of an element is not easily discernible. Here, it is determined when, in the absence of a generating element, one can still with confidence place bounds on the maximal index. Such a bound is usually less than (m), and in some cases the bound is shown to be strict. Moreover, general information about existence or nonexistence of a generating element often can be predicted from the bound.     

Linearity and bisimulation

Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not affect well-typed observers. This gives a congruence far larger than the standard bisimilarity while retaining semantic soundness. The framework is smoothly extendible to other settings involving nondeterminism and state. As an application we develop a behavioural theory of secrecy in the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach, while still offering compositional verification techniques.     

Toward a theory of Pollard's rho method

Pollard's “rho” method for integer factorization iterates a simple polynomial map and produces a nontrivial divisor of n when two such iterates agree modulo this divisor. Experience and heuristic arguments suggest that a prime divisor p should be detected in steps, but this has never been proved. Indeed, nothing seems to be have been rigorously proved about the probability of success that would improve the obvious lower bound of 1/p. This paper shows that for fixed k, this probability is at least (₂^k)/p + O(p^−3/2) as p → ∞. This leads to an Ω(log²p)/p estimate of the success probability.     

On Deciding Readiness and Failure Equivalences for Processes

In this paper, we study the complexity of deciding readiness and failure equivalences for finite state processes and recursively defined processes specified by normed context-free grammars (CFGs) in Greibach normal form (GNF). The results are as follows: (1) Readiness and failure equivalences for processes specified by normed GNF CFGs are both undecidable. For this class of processes, the regularity problem with respect to failure or readiness equivalence is also undecidable. Moreover, all these undecidability results hold even for locally unary processes. In the unary case, these problems become decidable. In fact, they are Π^p₂-complete, We also show that with respect to bisimulation equivalence, the regularity for processes specified by normed GNF CFGs is NL-complete. (2) Readiness and failure equivalences for finite state processes are PSPACE-complete. This holds even for locally unary finite state processes. These two equivalences are co-NP-complete for unary finite state processes. Further, for acyclic finite state processes, readiness and failure equivalences are co-NP-complete and they are NL-complete in the unary case. (3) For finite tree processes, we show that finite trace, readiness, and failure equivalences are all L-complete. Further, the results remain true for the unary case. Our results provide a complete characterization of the computational complexity of deciding readiness and failure equivalences for several important classes of processes.