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     

Helping by unambiguous computation and probabilistic computation

Schöning [S] introduced a notion of helping and suggested the study of the class P_help(C) of languages that can be helped by oracles in a given classC. He showed that P_help(BPP) is included in ZPP. Later, Ko [K] introduced a weaker notion of helping, called one-sided helping, and proved that P_1-help(BPP) is included in R and that UP is included in P_1-help(UP). The three inverse inclusions are open problems (see [Hem]). Caiet al. [CHV] constructed a relativized world in which the third open inclusion fails. We show relativized worlds in which all three open inclusions fail in a strong way. In particular, we strengthen the result of Caiet al., showing that P_help(UP) is not included in Few. This is obtained as a corollary of a general result that gives sufficient conditions, on a relativizable complexity classC, to ensure the relativized separation of P_help(UP) fromC. Further separations are also derived. The other two open inclusions are showed to fail strongly by the relativized separation of ZPP from P_1-help(AM ∩ co-AM).     

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.     

Accepting splicing systems with permitting and forbidding words

In this paper we propose a generalization of the accepting splicing systems introduced in Mitrana et al. (Theor Comput Sci 411:2414–2422, 2010). More precisely, the input word is accepted as soon as a permitting word is obtained provided that no forbidding word has been obtained so far, otherwise it is rejected. Note that in the new variant of accepting splicing system the input word is rejected if either no permitting word is ever generated (like in Mitrana et al. in Theor Comput Sci 411:2414–2422, 2010) or a forbidding word has been generated and no permitting word had been generated before. We investigate the computational power of the new variants of accepting splicing systems and the interrelationships among them. We show that the new condition strictly increases the computational power of accepting splicing systems. Although there are regular languages that cannot be accepted by any of the splicing systems considered here, the new variants can accept non-regular and even non-context-free languages, a situation that is not very common in the case of (extended) finite splicing systems without additional restrictions. We also show that the smallest class of languages out of the four classes defined by accepting splicing systems is strictly included in the class of context-free languages. Solutions to a few decidability problems are immediately derived from the proof of this result.     

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.     

A Decidability Result for the Model Checking of Infinite-State Systems

We present a decidability result for the model checking of a certain class of properties that can be conveniently expressed as ground formulae of a first-order temporal fragment. The decidability result is obtained by importing into the context of model-checking problems some techniques developed for the combination of decision procedures for the satisfiability of constraints. The general decidability result is then specialized for checking properties of particular interest, such as liveness and safety, and, for the latter case, a more optimized algorithm has been proposed.     

Bisimulation equivalence of a BPP and a finite-state system can be decided in polynomial time

In this paper we consider the problem of deciding bisimulation equivalence of a BPP and a finite-state system. We show that the problem can be solved in polynomial time and we present an algorithm deciding the problem in time O(n⁴). The algorithm also constructs for each state of the finite-state system a ‘symbolic’ semilinear representation of the set of all states of the BPP system which are bisimilar with this state.     

Regular set of representatives for time-constrained MSC graphs

Systems involving both time and concurrency are notoriously difficult to analyze. Existing decidability results apply when clocks on different processes cannot be compared or when the set of timed executions is regular. We prove new decidability results for timed concurrent systems, requiring neither restriction. We consider the formalism of time-constrained MSC graphs (TC-MSC graphs for short) introduced in Akshay et al. (2007) [1], and study if the set of timed executions generated by a TC-MSC graph is empty. This emptiness problem is known to be undecidable in general (Gastin et al., 2009) [11]. Our approach consists of finding a regular set R of representative timed executions, i.e., such that every timed execution of the system has an equivalent, up to commutation, timed execution in R. This allows us to solve the emptiness problem under the assumption that the TC-MSC graph is prohibited from (1) forcing any basic scenario to take an arbitrarily long time to complete and (2) enforcing unboundedly many events to occur within one unit of time.     

Deletion along trajectories

We describe a new way to model deletion operations on formal languages, called deletion along trajectories. We examine its closure properties, which differ from those of shuffle on trajectories, previously introduced by Mateescu et al. In particular, we define classes of non-regular sets of trajectories such that the associated deletion operation preserves regularity. Our results give uniform proofs of closure properties of the regular languages for several deletion operations.

We also show that deletion along trajectories serves as an inverse to shuffle on trajectories. This leads to results on the decidability of certain language equations, including those of the form LTX=R, where L,R are regular languages and X is unknown.     

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

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

Distributed synthesis for well-connected architectures

We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly well-connected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.     

A new sure-success generalization of Grover iteration and its application to weight decision problem of Boolean functions

In two recent papers, a sure-success version of the Grover iteration has been applied to solve the weight decision problem of a Boolean function and it is shown that it is quadratically faster than any classical algorithm (Braunstein et al. in J Phys A Math Theor 40:8441, 2007; Choi and Braunstein in Quantum Inf Process 10:177, 2011). In this paper, a new approach is proposed to generalize the Grover’s iteration so that it becomes exact and its application to the same problem is studied. The regime where a small number of iterations is applied is the main focus of this work. This task is accomplished by presenting the conditions on the decidability of the weights where the decidability problem is reduced to a system of algebraic equations of a single variable. Thus, it becomes easier to decide on distinguishability by solving these equations analytically and, if not possible, numerically. In addition, it is observed that the number of iterations scale as the square root of the iteration number of the corresponding classical probabilistic algorithms.     

Derivation languages of grammar forms†

The family of derivation languages or Szilard languages associated with a grammar form is studied. It is shown that Szilard equivalence, regular completeness and regular sufficiency are decidable properties. Although the decidability of left Szilard equivalence remains open, we reduce this problem to the equivalence problem for a special class of s-grammar forms     

Tree automata with one memory set constraints and cryptographic protocols

We introduce a class of tree automata that perform tests on a memory that is updated using function symbol application and projection. The language emptiness problem for this class of tree automata is shown to be in DEXPTIME.We also introduce a class of set constraints with equality tests and prove its decidability by completion techniques and a reduction to tree automata with one memory.Finally, we show how to apply these results to cryptographic protocols. We introduce a class of cryptographic protocols and show the decidability of secrecy for an arbitrary number of agents and an arbitrary number of (concurrent or successive) sessions, provided that only a bounded number of new data is generated. The hypothesis on the protocol (a restricted copying ability) is shown to be necessary: without this hypothesis, we prove that secrecy is undecidable, even for protocols without nonces.     

Risk Assessment for One-Counter Threads

Threads as contained in a thread algebra are used for the modeling of sequential program behavior. A thread that may use a counter to control its execution is called a ‘one-counter thread’. In this paper the decidability of risk assessment (a certain form of action forecasting) for one-counter threads is proved. This relates to Cohen’s impossibility result on virus detection (Comput. Secur. 6(1), 22–35, 1984). Our decidability result follows from a general property of the traces of one-counter threads: if a state is reachable from some initial state, then it is also reachable along a path in which all counter values stay below a fixed bound that depends only on the initial and final counter value. A further consequence is that the reachability of a state is decidable. These properties are based on a result for ω-one counter machines by Rosier and Yen (SIAM J. Comput. 16(5), 779–807, 1987).     

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.     

Some decidability problems of sentential formst †

Various decidability problems of SF-languages, i.e. sets of sentential forms, of Chomsky grammars are studied. Among the problems are the equivalence, ambiguity, equality to a regular set, and regularity of SF-languages, and the SF-ness of regular languages. All of these problems are undecidable for type 0 grammars, and many of them are decidable for minimal linear grammars. Strongest possible undecidability and decidability results are looked for.     

I-Fuzzy equivalence relations and I-fuzzy partitions

A T-fuzzy equivalence relation is a fuzzy binary relation on a set X which is reflexive, symmetric and T-transitive for a t-norm T. Recently, Mesiar et al. [R. Mesiar, B. Reusch, H. Thiele, Fuzzy equivalence relations and fuzzy partitions, J. Multi-Valued Logic Soft Comput. 12 (2006) 167-181] have generalised the t-norm T to any general conjunctor C and investigated the minimal assumptions required on such operations, called duality fitting conjunctors, such that the fuzzification of the equivalence relation admits any value from the unit interval and also the one-one correspondence between the fuzzy equivalence relations and fuzzy partitions is preserved. In this work, we conduct a similar study by employing a related form of C-transitivity, viz., I-transitivity, where I is an implicator. We show that although every I-fuzzy equivalence relation can be shown to be a C-fuzzy equivalence relation, there exist C-fuzzy equivalence relations that are not I-fuzzy equivalence relations and hence these concepts are not equivalent. Most importantly, we show that the class of duality fitting implicators I is much richer than the residuals of the duality fitting conjunctors in the study of Mesiar et al. We also show that the I-fuzzy partitions have a “constant-wise” structure.