Branching bisimilarity of normed BPA processes as a rational monoid

Logical Methods in Computer Science Vol. 13(4:17)2017, pp. 1–16 www.lmcs-online.org Submitted Feb. 22, 2016 Published Nov. 28, 2017 BRANCHING BISIMILARITY OF NORMED BPA PROCESSES AS A RATIONAL MONOID PETR JANˇ CAR Technical University Ostrava (FEI Vˇ SB-TUO), Czech Rep. e-mail address: p[email protected] Abstract. The paper presents an elaborated and simplified version of the structural result for branching bisimilarity on normed BPA (Basic Process Algebra) processes that was the crux of a conference paper by Czerwi´nski and Janˇcar (arxiv 7/2014 and LiCS 2015). That paper focused on the computational complexity, and a NEXPTIME-upper bound has been derived; the authors built on the ideas by Fu (ICALP 2013), and strengthened his decidability result. Later He and Huang announced the EXPTIME-completeness of this problem (arxiv 1/2015, and LiCS 2015), giving a technical proof for the EXPTIME membership. He and Huang indirectly acknowledge the decomposition ideas by Czerwi´nski and Janˇcar on which they also built, but it is difficult to separate their starting point from their new ideas. One aim here is to present the previous decomposition result of Czerwi´nski and Janˇcar in a technically new framework, noting that branching bisimulation equivalence on normed BPA processes corresponds to a rational monoid (in the sense of [Sakarovitch, 1987]); in particular it is shown that the mentioned equivalence can be decided by normal-form computing deterministic finite transducers. Another aim is to provide a complete description, including an informal overview, that should also make clear how Fu’s ideas were used, and to give all proofs in a form that should be readable and easily verifiable. 1. Introduction Bisimulation equivalence (or bisimilarity) is a fundamental notion in theory of processes, and the respective decidability and complexity questions are a natural research topic; we can refer to [ 21 ] for an (updated) overview of the results in a specific area of process rewrite systems. One basic model of infinite-state systems is called Basic Process Algebra (BPA), which can be naturally related to context-free grammars in Greibach normal form. Here the processes are identified with finite sequences of variables (nonterminals); a process Aα can change by performing an action, denoted by Aα a −→ βα , in which case its leftmost variable A is rewritten according to a grammar rule A−→ aβ (presented rather as Aa −→ β in our context). Key words and phrases: branching bisimulation equivalence, basic process algebra. The work was supported by the Grant Agency of the Czech Rep., project GAˇ CR:15-13784S. LOGICAL METHODS l IN COMPUTER SCIENCE DOI:10.23638/LMCS-13(4:17)2017 c P. Janˇ car CC Creative Commons 2 P. JANˇ CAR A seminal paper by Baeten, Bergstra and Klop [ 1 ] showed the decidability of bisimilarity on nBPA, i.e. on the normed BPA processes, where each variable can be stepwise rewritten to the empty word; this decidability result was later extended to the whole class BPA [ 5 ]. Further exploration placed the problem on nBPA even in PTime [ 12 ] (this problem is thus PTime -complete [ 2 ]); we can refer to [ 6 ] for further references and a way towards the so far best known upper bound. The bisimilarity problem for the whole class BPA is known to be ExpTime -hard [ 17 ] and to belong to 2ExpTime (claimed in [ 3 ] and explicitly proven in [15]). When also internal (unobservable) actions of systems are taken into account, the most studied generalization of bisimilarity is weak bisimilarity [19] but the relevance of the finer equivalence called branching bisimilarity is also well argued [22]. The (un)decidability status of weak bisimilarity on BPA, as well as on nBPA, is still open, but we have the ExpTime -hardness result by Mayr [ 18 ] for weak bisimilarity on nBPA. Similarly, the decidability status of weak bisimilarity is still open in the case of (normed) Basic Parallel Processes, which is the parallel (or commutative) version of BPA. The situation seems more favourable in the case of branching bisimilarity. It was first shown decidable for the normed Basic Parallel Processes [ 7 ], and then Fu [ 9 ] showed the decidability on nBPA. A later paper [ 23 ] shows that the mentioned decidability results for branching bisimilarity cannot be essentially extended, possibly with the exception of the full classes of BPA processes and of Basic Parallel Processes for which the decidability question remains open. The case of branching bisimilarity on nBPA is the main topic of this paper. We first note that Fu’s decidability result [ 9 ] is substantially stronger than the previous results dealing with so called totally normed BPA [ 14 , 4 ] (where no variable can “disappear” by unobservable actions). In the case of totally normed BPA processes even a polynomial time algorithm is suggested in [ 10 ], building on the unique-decomposition results and techniques that were previously used in the case of (strong) bisimilarity on nBPA. A crucial novel idea in Fu’s decidability proof is a use of the notion that can be called the class-change norm (called the branching norm in [ 9 ]); while the standard norm counts all steps in rewriting a process to the empty word, the class-change norm only counts the steps that change the current equivalence-class. It is not clear how to compute this norm directly but equivalent processes α∼β must have the same class-change norm. Another useful fact shown by Fu is that the relation of αγ and βγ (either αγ ∼βγ or αγ 6∼ βγ ) is determined solely by the redundant variables w.r.t. γ , i.e. by those X for which Xγ ∼γ , independently of the string γitself. This paper is based on the research reported on in [ 8 ], performed with W. Czerwi´nski (see Author’s acknowledgements). The main new idea there was to use the decompositions of processes that are relative to a given set of (redundant) variables; the notion is also based on the (semantic) class-change norm. This structural result is here a bit reworked and presented in a technically new framework; it is shown that the quotient of branching bisimulation equivalence on nBPA is a rational monoid (in the sense of Sakarovitch [ 20 ]). In particular, for a given nBPA system G branching bisimilarity can be decided by a (canonical) normal-form computing deterministic finite-state transducer TG ; to each process α it computes the normal form TG ( α ), which is a unique process in the equivalence-class [ α ] ∼ , and we have α∼β iff TG ( α ) = TG ( β ). The size of TG can be easily bounded by an exponential function of the size of G. BRANCHING BISIMILARITY OF NORMED BPA 3 We will not show a direct construction of TG , but we will show a quickly verifiable consistency condition for any given transducer T that guarantees T ( α ) = T ( β ) ⇒α∼β ; moreover, TG will be shown to satisfy this consistency condition w.r.t. G . This immediately yields a nondeterministic exponential-time algorithm deciding branching bisimilarity on nBPA: given G , α, β , guess a transducer T of at most exponential size (in the size of G ), check that Tis consistent with G, and verify that T(α) = T(β). The problem for which Fu [ 9 ] showed the decidability (by an involved proof in a tableau framework) is thus placed in NExpTime. Regarding the question of a lower bound, Fu [9] noted that the problem is ExpTime -hard, which was later confirmed by Huang and Yin [ 13 ]. (More details about this interesting point are given in Section 3.) In Section 5 we also add some remarks on a possible construction of the canonical transducer TG in deterministic exponential time; this seems to be (at least implicitly) related to the paper by He and Huang [11] that announced ExpTime-completeness. Structure of the paper. In Section 2 we define the used notions and make some simple observations. Section 3 gives an informal overview, which is then formalized in Section 4. Section 3 also contains a remark on the lower complexity bound, and Section 5 adds some further remarks. 2. Preliminaries We put N={0,1,2, . . . }, and [i, j] = {i, i+1, . . . , j}for i, j ∈N. For a set M , by M∗ we denote the set of finite sequences of elements of M , also called words, or strings,over M ; by ε we denote the empty string. For α∈M∗ , by |α| we denote its length. Labelled transition systems. Alabelled transition system, an LTS for short, is a tuple L= (S,A,(a −→)a∈A) where S is the set of states, A is the set of actions and a −→⊆ S × S is the set of a -labelled transitions. We reserve the symbol τfor the (unique) silent action; the visible actions are the elements of Ar{τ}. We write sa −→ t rather than ( s, t ) ∈a −→ (for a∈ A ), and we define sw −→ t for w∈ A∗ inductively: sε −→ s ; if sa −→ s0 and s0u −→ t , then sau −→ t . By sw −→ t we sometimes also refer to a concrete respective path from s to t in L . (We do not exclude cycles in the paths.) Branching bisimilarity, i.e., branching bisimulation equivalence ∼. Given an LTS L = ( S,A, ( a −→ ) a∈A ), a relation B ⊆ S × S is a branching bisimulation in L if for any (s, t)∈ B the following two conditions hold: i) for any a∈ A, any move sa −→ s0can be matched from t, i.e., a) a=τand (s0, t)∈ B, or b) there is a path t = t0 τ −→ t1 τ −→ · · · τ −→ tk a −→ t0 (for some k≥ 0) such that (s0, t0)∈ B and (s, ti)∈ B for all i∈[1, k]; ii) for any a∈ A, any move ta −→ t0can be matched from s, i.e., a) a=τand (s, t0)∈ B, or 4 P. JANˇ CAR b) there is a path s = s0 τ −→ s1 τ −→ · · · τ −→ sk a −→ s0 (for some k≥ 0) such that (s0, t0)∈ B and (si, t)∈ B for all i∈[1, k]. By s∼t , to be read as “states s, t are branching bisimilar”, we denote that there is a branching bisimulation containing ( s, t ). We can easily verify the standard facts that ∼ ⊆ S × S is the union of all branching bisimulations (in L ), and thus the largest branching bisimulation in L, and that ∼is an equivalence relation. Class-changing transitions, and class-change norm hhsii. Assuming an LTS L = ( S,A, ( a −→ ) a∈A ), we now introduce a few notions and make simple observations that turn out to be very useful for our aims. We say that atransition sa −→ s0is class-changing if s6∼ s0. Hence a class-changing transition leads from one equivalence class of ∼ to a different class. We note that s∼t and sa −→ s0 entails that either a = τ and sa −→ s0 is not class-changing (in which case s0∼t ), or there is a path t = t0 τ −→ t1 τ −→ · · · τ −→ tk a −→ t0 (for some k≥ 0) where no transition in the path t0 τ −→ t1 τ −→ · · · τ −→ tk is class-changing (hence t = t0∼t1∼ · · · ∼ tk ) and s0∼t0 ; in the latter case, the transition tk a −→ t0 is class-changing iff sa −→ s0is class-changing. We introduce the class-change norm hhsii as the “class-change distance” of s to the silent states. A state s is silent if sw −→ s0 entails w∈ {τ}∗ . (Hence we can never perform a visible action when starting from a silent state.) Let Ssil be the set of silent states (in the assumed LTS L = ( S, A, ( a −→ ) a∈A )); Ssil is obviously a (maybe empty) equivalence class of ∼ (since the set {(s, t)|s, t ∈Ssil}is a branching bisimulation, and s∈Ssil,t6∈ Ssil implies s6∼ t). By hhsii we denote the class-change norm of s , the cc-norm for short, which is the least `∈N such that there is a path s = s0 a1 −→ s1 a2 −→ · · · ak −→ sk∈Ssil that has precisely ` class-changing transitions; we put hhsii = ω if Ssil is not reachable from s . Hence hhsii = 0 iff s∈Ssil . The previous discussion (of matching sa −→ s0 from t when s∼t ) easily yields the following fact: Observation 2.1. If s∼t, then hhsii =hhtii. Remark 2.2. The cc-norm was introduced by Fu in [ 9 ], who used the name “branching norm” and a slightly different form; formally his norm also counts the visible transitions no matter if they are class-changing or not but this is no crucial difference, in fact. BPA systems and processes. We view a BPA system (where BPA stands for Basic Process Algebra) as a context-free grammar in Greibach normal form, with no starting variable (nonterminal). We denote it as G= (V,A,R) where V is a finite set of variables (or nonterminals), A is a finite set of actions (or terminals), which can contain the silent action τ , and R is a finite set of rules of the form Aa −→ α where A∈ V,a∈ A,α∈ V∗. A BPA system G= (V,A,R) has the associated LTS LG= (V∗,A,(a −→)a∈A) BRANCHING BISIMILARITY OF NORMED BPA 5 where each rule Aa −→ α in R induces the transitions Aβ a −→ αβ for all β∈ V∗ . The states of LG, i.e. the strings of variables, are also called processes. Standard (syntactic) norm kαk, and normed BPA systems (nBPA). Given a BPA system G = ( V,A,R ), the norm kαk of α∈ V∗ is the length |w| of a shortest w∈ A∗ such that αw −→ ε ; we put kαk = ω when there is no such w (where ω stands for an “infinite amount”). We say that α is normed if kαk ∈ N (i.e., if αw −→ ε for some w ). The BPA system Gis normed, an nBPA system for short, if each variable A∈ V is normed. Atransition αa −→ β is norm-reducing if kαk>kβk , in which case kβk = kαk− 1, in fact. If kαk = ω , then there is no norm-reducing transition αa −→ β . The facts captured by the next proposition are standard; they also entail that we can check in polynomial time whether a BPA system is normed. Proposition 2.3. Given a BPA system G= (V,A,R), we have: (1) kεk= 0. (2) kαβk=kαk+kβk(assuming ω+z=z+ω=ωfor any z∈N∪ {ω}). (3) kAk= 1 + kαkfor a norm-reducing rule Aa −→ α, if kAk ∈ N. (4) There is a polynomial-time algorithm that computes kAkfor each A∈ V. (5) The finite values kAkare at most exponential in the size of G. We note in particular that the algorithm in the point (4) can naturally use dynamic programming: We first temporarily assume kAk = ω (the norm is infinite) for all variables; this also temporarily yields kαk = ω for all rhs (right-hand sides) of the rules Aa −→ α , except of α = ε since we put kεk = 0 definitively. Now we repeatedly look for a variable A with a temporary norm that has a rule Aa −→ α with the least definitive kαk ∈ N ; for such A we put kAk = 1 + kαk definitively (all variables in α have the definitive norms already), and we recompute the temporary norms of the right-hands sides of the rules in R accordingly. After this repeated process finishes, all temporary cases kAk=ωbecome also definitive. Branching bisimilarity problem for nBPA. The nBPA-bbis problem asks, given an nBPA system G = ( V,A,R ) and two processes α, β ∈ V∗ , if α∼β , i.e., if α and β are branching bisimilar as the states in LG. We add a remark on hhαii , which refers to the (“semantic”) cc-norm of α in LG . By Observation 2.1 we know that α∼β implies hhαii = hhβii . We have shown how to compute the (“syntactic”) norm kαk , but it is unclear how to compute hhαii . Nevertheless, since ε is a silent state in LG , we can easily observe that hhαii ≤ kαk (and hhAii is thus at most exponential by (5) in Prop. 2.3). 3. Informal overview Here we sketch some informal ideas that are elaborated in Section 4. We also use a small, but important, example; the example is inspired by a recent work of Huang and Yin [ 13 ], which is further discussed below in an additional remark on the lower complexity bound for the nBPA-bbis problem. Let us consider the following BPA system G= (V,A,R) where • V ={A, B, C, E, FB,[FB, A]}(hence |V| = 6, since [FB, A] is one symbol), • A ={τ}∪{a, b, c, e, f1 B, f2 B}, 6 P. JANˇ CAR • R ={Aa −→ ε, B b −→ ε, C c −→ ε, E e −→ ε, FB τ −→ ε, FB f1 B −→ ε, Af1 B −→ [FB, A], B f1 B −→ B, C f1 B −→ E, [FB, A]a −→ ε, [FB, A]f1 B −→ [FB, A], [FB, A]f2 B −→ ε, A f2 B −→ FB}. All variables are normed, we even have kXk= 1 for all X∈ V. In the LTS LG we have, e.g., FBAABACCAB ∼AABACCAB but FBAACABCAB 6∼ AACABCAB. More generally for any α∈ {A, B, C}∗we have FBα∼αiff α=α0Bα00 where α0∈ {A}∗. (3.1) We can view FB as a “claim” that α satisfies “first B ”, which means that α contains B as the first (i.e., leftmost) occurrence of a symbol from {B, C} . We leave the verification of (3.1) as an interesting small exercise, since it is not crucial for us. The example illustrates that a variable can be or not be “redundant” (w.r.t. ∼ ), depending on the “suffix”; formally we say that Rγ = {X∈ V | Xγ ∼γ} is the set of redundant variables w.r.t. γ . In the example, the condition characterizing the strings α∈ {A, B, C}∗ for which FBα∼α is regular, i.e. checkable by a finite automaton. It turns out to be an important fact that each nBPA system G has an associated finite automaton FG that determines the set Rγ after reading γ . Moreover, it turns out possible, and convenient, to let the automaton FG read its input γ from right to left and use the respective sets R⊆ V as its control states; the automaton starts in the initial state Rε (which might be the empty set) and after reading γ (from right to left) it enters the state Rγ . Its transitions are thus of the form RAγ A ←− Rγ , in the notation that visualizes reading from right to left. (In Section 4 we also show the soundness: Rγ = Rδ entails RAγ = RAδ .) These ideas were already developed by Fu [9] (though he did not mention the automaton explicitly). The above example can be generalized to show that the automaton FG can have exponentially many states Rγ (w.r.t. the size of the given nBPA system G ): we can add several other pairs {B0, C0} of variables, with the respective variables FB0, [ FB0, .. ] and the respective actions and rules. The issue of exponentially many sets of redundant variables is dealt with in [13] in more detail. Remark 3.1. In [ 9 ] there was also a note saying that the nBPA-bbis problem can be shown ExpTime-hard by a slight modification of Mayr’s proof for weak bisimilarity [ 18 ]. Though this note was repeated in further works, no rigorous proof was given (as pointed out in the first version of this paper [ 16 ]). The mentioned “slight modification” has turned out to be not so obvious, but the ExpTime-hardness has been recently rigorously confirmed by Huang and Yin [13]. Mayr’s ExpTime-hardness proof [ 18 ] uses a reduction from the ALBA problem (Alternating Linear Bounded Automata acceptance), a standard ExpTime -complete problem. Huang and Yin [ 13 ] decided to use the Hit-or-Run game for their reduction; this ExpTime-complete problem was used by Kiefer [ 17 ] to show the ExpTime-hardness of strong bisimilarity for (general) BPA systems. The ExpTime-hardness of the Hit-or-Run game was also established by a reduction from the ALBA problem. It is worth to note that it is also possible to modify Mayr’s reduction [ 18 ] by the new idea of [ 13 ], to yield ExpTime-hardness of the nBPA-bbis problem by a direct reduction from the ALBA problem; the above example (inspired by [ 13 ]) BRANCHING BISIMILARITY OF NORMED BPA 7 captures the essence since it shows how it is possible to “remember” an ALBA configuration by the current set of redundant variables. (If α is a sequence of ALBA configurations, then Rα determines the leftmost configuration in the sequence; we use a special pair { [ i, 0] , [ i, 1] } of variables (like {B, C} in the example), with the respective additional variables, actions and rules, to “remember” if the i-th position is 0 or 1.) Hence Fu’s remark in [ 9 ] can be viewed as correct in the end, though it has not been straightforward to come with the appropriate “slight” modification. The contribution of this paper captures the decomposition ideas from [ 8 ]. The above discussed automaton FG , satisfying Rα α ←− Rε , can be enhanced to become a finite-state transducer TG (corresponding to a given nBPA system G = ( V,A,R )) that translates its input α into a string TG ( α ), processing α from right to left; this is denoted Rα α ←− βRε where β = TG ( α ). For the uniqueness of the “canonical transducer” TG we use a linear order on V and take TG ( α ) as the lexicographically smallest string among the longest redundancy-free strings from the equivalence class [ α ] ∼ . (Here the lexicographic order of two different strings is determined by the first position from the right where the strings differ.) By the redundancy-freeness of a string β we mean that β = β0Aβ00 entails that Aβ00 6∼ β00 (i.e., A6∈ Rβ00 ). We recall that β∈ [ α ] ∼ entails hhβii = hhαii (by Observation 2.1), and we can observe that |β| ≤ hhβii when β is redundancy-free (since any path Aβ00 u −→ β00 contains at least one class-changing transition when Aβ00 6∼ β00). We will verify the soundness of the above definition of the canonical transducer TG (for any normed BPA system G). We thus get α∼β(in LG) iff TG(α) = TG(β). We also note the idempotency TG ( TG ( α )) = TG ( α ), and the fact that TG ( α ) can be naturally viewed as the normal form (or the prime decomposition) of α ; two strings α, β are equivalent (meaning branching bisimilar) iff they have the same normal forms (the same prime decompositions). We also note that generally we do not have TG ( αγ ) = TG ( α ) TG ( γ ), since the decomposition is more subtle: we have TG ( αγ ) = TG Rγ ( α ) TG Rε ( γ ), where TG R ( α ) is the translation of αwhen the transducer starts from Rinstead of the initial state Rε. We will not show a direct construction of TG , when given an nBPA system G , but we will show a quickly verifiable “consistency” condition for any given transducer T that guarantees T ( α ) = T ( β ) ⇒α∼β ; moreover, TG will be shown to satisfy this consistency condition w.r.t. G. The size of the canonical transducer TG is at most exponential in the size of G (since |T G R ( A ) |≤kAk , as we will show easily), and we thus have a conceptually simple nondeterministic exponential-time algorithm deciding the nBPA-bbis problem: Given a normed BPA system G = ( V,A,R ) and α, β ∈ V∗ , guess a transducer T of at most exponential size (w.r.t. G ), check that T is consistent with G , and verify that T(α) = T(β). In Section 5 we add further remarks on the construction of TG and on the complexity of the nBPA-bbis problem. 8 P. JANˇ CAR 4. Branching bisimilarity on nBPA via finite transducers 4.1. Normal-form-computing transducers. By a transducer we mean a tuple T = ( Q, V, ∆ , q0 ) where Q is a finite set of (control) states, V is a finite (input and output) alphabet, ∆ is a (transition and translation) function of the type Q× V −→ Q× V∗ , and q0∈Qis the initial state. We view transducers as reading (and writing) from right to left; we write q0A ←− γq instead of ∆( q, A ) = ( q0, γ ) to visualize this fact. The function ∆ is naturally extended to the type Q× V∗−→ Q× V∗ by the following inductive definition, which uses the “visual” notation: •qε ←− εq(for each q∈Q), •if q0A ←− γqand q00 α ←− βq0, then q00 αA ←− βγ q. By Tq ( α ) we denote the translation of α∈ V∗ when starting in q∈Q , i.e., the string β such that q0α ←− βq (for some q0 ); we also use the notation T ( α ) for Tq0 ( α ). For each q∈Q we define the equivalence relation ≡T qon V∗as follows: α≡T qβ⇔df Tq(α) = Tq(β); we put ≡T=≡T q0. We say that A∈ V is a q -prime if Tq ( A ) = A , hence if q0A ←− Aq for some q0 . A string α∈ V∗ is a q-normal form if α=εor α=AkAk−1· · · A1for k≥1 where qk Ak ←− Ak qk−1 Ak−1 ←− Ak−1 qk−2· · · A3 ←− A3 q2 A2 ←− A2 q1 A1 ←− A1 qfor some q1, q2, . . . , qk. By NFT q we denote the set of q -normal forms; hence ε∈NFT q , and βA ∈NFT q iff A is a q -prime and β is a q0 -normal form for q0 satisfying q0A ←− Aq . We note that α∈NFT q entails Tq(α) = α. A transducer T = ( Q, V, ∆ , q0 ) is a normal-form-computing transducer, an nfc-transducer for short, if Tq ( A ) ∈NFT q for all q∈Q , A∈ V , and the “target states” are the same for both Aand Tq(A), i.e. q0A ←− γqimplies q0γ ←− γq(where γ=Tq(A)). (4.1) For nfc-transducers we thus have Tq ( Tq ( α )) = Tq ( α ) (idempotency), which also entails that α≡T qTq(α); moreover, the condition (4.1) also entails that Tq(αβ) = Tq(αTq(β)). We note that checking if a given transducer Tis an nfc-transducer is straightforward. 4.2. Nfc-transducers consistent with a BPA system. In Section 4.3 we will define a canonical nfc-transducer TG for a normed BPA system G ; it will turn out that the branching bisimilarity ∼in LGcoincides with the equivalence ≡TG. Here we assume a fixed (general) BPA system G = ( V,A,R ) and a fixed nfc-transducer T = ( Q, V, ∆ , q0 ); we aim to find a suitable condition guaranteeing that the equivalence ≡T (on the set V∗) is a branching bisimulation in the LTS LG= (V∗,A,(a −→)a∈A). A natural idea is to require that for every action a∈ A (including the case a = τ ) the processes α and T ( α ) yield the same normal forms of the results of “long moves” BRANCHING BISIMILARITY OF NORMED BPA 9 τ −→ τ −→ · · · τ −→ a −→ where the (maybe empty) τ -prefix is bound to go inside the equivalence class [ α ] ≡T (which is the same as [ T ( α )] ≡T ), and the final a −→ -step might be missing when a = τ . We formalize this idea by Def. 4.1, after we introduce the “long moves” a q , relativized w.r.t. the states q∈Q. For our fixed Gand Twe write αa qβ, where α, β ∈ V∗,q∈Q, and a∈ A, if •either a=τand β=Tq(α), •or there are α1, α2, . . . , αk(for some k≥0) and β0such that α=α0 τ −→ α1 τ −→ · · · τ −→ αk a −→ β0in LG, Tq(α0) = Tq(α1) = · · · =Tq(αk) and Tq(β0) = β . Hence αa qβ entails that β∈NFT q ( β is a q -normal form). In particular we have ετ qε . We define the equivalences ≈qas follows: α1≈qα2⇔df ∀a∈ A :{β|α1 a qβ}={β|α2 a qβ}. Now the announced definition follows; it also uses the fact that q0A ←− εq implies q0 = q for nfc-transducers (by the condition (4.1)). Definition 4.1. An nfc-transducer T = ( Q, V, ∆ , q0 ) is consistent with a BPA system G= (V,A,R) if the following three conditions hold. (1) A≈q0εif Tq0(A) = ε(i.e., if q0 A ←− εq0); (2) A≈qTq(A) if Tq(A)6=ε(hence q0A ←− βqwhere β6=εentails A≈qβ); (3) AC ≈qCif Tq(AC) = Tq(C) = C(i.e., if q0A ←− εq0C ←− Cqfor some q0). Lemma 4.2. (1) There is a polynomial algorithm checking if a given nfc-transducer T is consistent with a given BPA system G. (2) If an nfc-transducer T is consistent with a BPA system G , then ≡T is a branching bisimulation in LG. Proof. 1. We assume an nfc-transducer T = ( Q, V, ∆ , q0 ) and a BPA system G = ( V,A,R ). For any q∈Q , we put Eq = {X∈ V | Tq ( X ) = ε} , and we define the set ¯ Eq⊆ V (of silently q-erasable variables) inductively: X∈¯ Eqif X∈ Eqand there is a rule Xτ −→ γin Rwhere γ∈(¯ Eq)∗. Using dynamic programming, the sets ¯ Eq are quickly constructible for all q∈Q . (In the first step we find X∈ Eq for which Xτ −→ ε is a rule in R ; if there are no such X , then ¯ Eq = ∅ .) It is easy to verify that the following “axioms and deduction rules” i) – v) characterize when we have αa qβ. (We omit T(α) in the notation q0α ←− T(α)qwhen unimportant.) i) ατ qTq(α) (for all α∈ V∗and q∈Q); ii) if Aa −→ δis a rule in R, then Aa qTq(δ); iii) if Aτ −→ δis a rule in R,Tq(A) = Tq(δ), and δa qβ, then Aa qβ; 16 P. JANˇ CAR [3] O. Burkart, D. Caucal, and B. Steffen. An elementary bisimulation decision procedure for arbitrary context-free processes. In Proc. MFCS’95, volume 969 of Lecture Notes in Computer Science, pages 423–433. Springer, 1995. [4] D. Caucal, D. T. Huynh, and L. Tian. Deciding branching bimiliarity of normed context-free processes is in Σp 2.Inf. Comput., 118(2):306–315, 1995. [5] S. Christensen, H. H¨uttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. Inf. Comput., 121(2):143–148, 1995. [6] W. Czerwi´nski. Partially-commutative context-free graphs. PhD thesis, University of Warsaw, 2012. Available at www.mimuw.edu.pl/˜wczerwin. [7] W. Czerwi´nski, P. Hofman, and S. Lasota. Decidability of branching bisimulation on normed commutative context-free processes. Theory Comput. Syst., 55(1):136–169, 2014. [8] W. Czerwi´nski and P. Janˇcar. Branching bisimilarity of normed BPA processes is in NEXPTIME. In Proc. LiCS’15, pages 168–179. IEEE, 2015. A preliminary version at arxiv.org/abs/1407.0645. [9] Y. Fu. Checking equality and regularity for normed BPA with silent moves. In Proc. ICALP’13, volume 7966 of Lecture Notes in Computer Science, pages 238–249. Springer, 2013. [10] C. He. A polynomial time algorithm for deciding branching bisimilarity on totally normed BPA. CoRR, abs/1411.4157, 2014. [11] C. He and M. Huang. Branching bisimilarity on normed BPA is EXPTIME-complete. In Proc. LiCS’15, pages 180–191. IEEE, 2015. A preliminary version at arxiv.org/abs/1501.04748. [12] Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theor. Comput. Sci., 158(1&2):143–159, 1996. [13] M. Huang and Q. Yin. Two lower bounds for BPA. In Proc. Concur’17, volume 85 of LIPIcs, pages 20:1–20:16. Schloss Dagstuhl–Leibniz-Zentrum f¨ur Informatik, 2017. [14] H. H¨uttel. Silence is golden: Branching bisimilarity is decidable for context-free processes. In Proc. CAV’91, volume 575 of LNCS, pages 2–12. Springer, 1992. [15] P. Janˇcar. Bisimilarity on basic process algebra is in 2-EXPTIME (an explicit proof). Logical Methods in Computer Science, 9(1:10):1–19, 2013. [16] P. Janˇcar. Branching bisimilarity of normed BPA processes as a rational monoid. CoRR, abs/1602.05151v1, 2016. [17] S. Kiefer. BPA bisimilarity is EXPTIME-hard. Inf. Process. Lett., 113(4):101–106, 2013. [18] R. Mayr. Weak bisimilarity and regularity of context-free processes is EXPTIME-hard. Theor. Comput. Sci., 330(3):553–575, 2005. [19] R. Milner. Communication and Concurrency. Prentice Hall, 1989. [20] J. Sakarovitch. Easy multiplications. I. The realm of Kleene’s theorem. Inf. Comput., 74(3):173–197, 1987. [21] J. Srba. Roadmap of infinite results. In Current Trends In Theoretical Computer Science, The Challenge of the New Century, volume 2, pages 337–350. World Scientific Publishing Co., 2004. An updated version at http://users-cs.au.dk/srba/roadmap/. [22] R. J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. J. ACM, 43(3):555–600, 1996. [23] Q. Yin, Y. Fu, C. He, M. Huang, and X. Tao. Branching bisimilarity checking for PRS. In Proc. ICALP’14, volume 8573 of Lecture Notes in Computer Science, pages 363–374. Springer, 2014. This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nd/4.0/ or send a letter to Creative Commons, PO Box 1866, Mountain View, CA 9404, USA