Process Algebra: Open Problems and Future Directions July 21-25, 2003 University of Bologna Residential Center Bertinoro (Forlì), Italy

Some Open Problems in Process Algebra

We intend to maintain this page as up to date as possible, in the hope that it will be a useful resource for the practising process algebraist and concurrency theorist. To this end, we invite all of the members of the process algebra community to help us by sending the maintainer of this page suggestions for new problems to be posted here, and pointers to their solutions.

Some further open problems are mentioned in the note Some of My Favourite Results in Classic Process Algebra by Luca Aceto, and on the slides of the talks delivered at the workshop.

Problems Posted by Luca Aceto

• Does bisimulation equivalence admit a finite equational axiomatization over the language obtained by adding Hennessy's auxiliary operator from [He88] to CCS?

  News posted on October 2, 2003. A negative solution to this problem has been obtained by Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir and Bas Luttik. Full details are now available from this paper.

• Are the left merge and communication merge operators necessary to obtain a finite axiomatization of bisimulation? Can one obtain a finite axiomatization by adding only one operator to the signature of CCS?

News posted on February 10, 2004. Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir and Bas Luttik have shown that Hennessy's merge suffices to give a finite axiomatization of split-2 bisimilarity (and in fact of each split-n bisimilarity and ST bisimilarity over the restriction, relabelling and recursion free fragment of CCS. Full details are now available from this paper.
Work on settling the above question for standard bisimilarity is ongoing. In that case, Hennessy's merge does not yield a finite axiomatization of bisimilarity, and we conjecture that no single binary operation does either.

• Give a model theoretic proof of Moller's theorem to the effect that bisimulation equivalence is not finitely based over CCS.
• Prove that observation congruence is also not finitely based over CCS.
• Can one come up with sufficient conditions of a reasonably general nature (be they syntactic or semantic) that ensure that bisimulation equivalence is finitely based?

See the note Some of My Favourite Results in Classic Process Algebra by Luca Aceto for further open problems.

Problems Posted by Marco Bernardo

• [Usability of Process Algebras]
  The process algebra (PA) related open problem I am interested in is that of the usability of PA in practice, i.e. the integration of PA in the system development cycle. Here is a short and incomplete list of partially addressed/open issues:
  • identification of the phases of the system development cycle in which PA can profitably be used;
  • development of an easy-to-use syntax for modeling systems in a fully fledged component-oriented way;
  • development/combination of techniques and models for inferring system properties from component properties and providing component-oriented diagnostic information in case of property violation (where properties can be related to functionality, performability, real-time constraints, and security) as well as for synthesizing correct-by-construction systems from correct components;
  • support for designing families of systems;
  • relationship/integration with notations used in practice (UML, SDL) as well as code generation.
• [An Open Question on Markovian Bisimulation]
  While Markovian bisimulation induces an exact aggregation at the Markov chain level (ordinary lumping), it is not known what happens with Markovian testing. As a consequence, if two process terms are Markovian testing equivalent, we do not know whether they possess the same performance characteristics. The questions are:
  1. Does Markovian testing induce an exact aggregation?
  2. If so, what is the relationship with ordinary lumping?

Problems Posted by Mario Bravetti

Problems Posted by Ilaria Castellani

Problems Posted by Rob van Glabbeek

• Problem 1: What is the coarsest semantic equivalence that

  (1) respects deadlock/livelock traces, as defined in Problem 4 below (hence also respects standard partial traces)

  (2) is compositional for the standard process algebra operators (CCS, CSP)

  (3) satisfies the Recursive Specification principle, saying that each system of guarded recursive equations has a unique solution.

  When requiring merely (1) and (2) the answer is fair testing equivalence as studied in [BRV95]. The impossible futures equivalence, documented in [VM01], certainly satisfies all properties, but it is not known whether is the coarsest.

  [BRV95] Ed Brinksma, Arend Rensink and Walter Vogler: Fair Testing. CONCUR 1995: 313-327.
  [VM01] Marc Voorhoeve and Sjouke Mauw: Impossible futures and determinism, Information Processing Letters 80(1): 51-58 (2001).

• Problem 2: What is the coarsest semantic equivalence that

  (1) respects lifeness, as explained in my Bertinoro talk,
  (2) does not satisfy KFAR-like fairness assumptions,
  (3) satisfies the Recursive Specification principle, saying that each system of guarded recursive equations has a unique solution.

  I'm not sure whether this problem needs a slight reformulation (such as extra requirements) upon further contemplation.

• Problem 3 (New!): Let ! be the operator with rules
  x -a-> y
  ---------------
  !x -a-> y || !x

  for a in Act. Find a congruence format for (rooted) weak or branching bisimulation that incorporates this operator applied to running processes, i.e. allowing rules of the form

  x -a-> y
  ---------------
  f(x) -a-> g(y)

  and g(x) -a-> !x.

• Problem 4 (New!): Say that the sequence of actions s is a deadlock/livelock trace of a process P if P has an execution path p whose visible content is s, and no extension of p has a visible content that extends s. Weak bisimulation equivalence is an example of a semantic equivalence that respects such traces: two weakly bisimilar processes always have the same deadlock/livelock traces. Moreover, fair testing equivalence as studied in Ed Brinksma, Arend Rensink and Walter Vogler: Fair Testing. CONCUR 1995: 313-327.>[BRV95] is the coarsest equivalence respecting deadlock/livelock traces that is a congruence for the operators of CCSP.

  Problem: Characterise the coarsest equivalence respecting deadlock/livelock traces that is a congruence for all WB cool GSOS operators. Here WB cool is a property of GSOS languages defined by Bard Bloom in TCS 146; it guarantees that weak bisimulation is a congruence.

• Problem 5 (New! Posted by Rob on the Concurrency Mailing list on Thursday, 17 Mar 2005 21:32:28 +0100 (MET)): Does there exists a finite equational axiomatisation of weak bisimulation equivalence on recursion-free CCS, allowing any number of auxiliary GSOS operators? Rob's conjecture, and one that I second is that the answer is negative.

  Body of Rob's message to the mailing list:
  Hi all, I just opened the mail, and saw that this weeks issue of TCS starts with a paper by Luca Aceta, Wan Fokkink, Anna Ingo'lfsdo'ttir and Bas Luttik showing the nonexistence of a finite equational axiomatisation of strong bisimulation equivalence on recursion-free CCS, allowing Hennessy's merge as auxiliary operator. In contrast, there exists a finite equational axiomatisation of strong bisimulation equivalence on recursion-free CCS using *two* auxiliary binary operators, namely the left merge and the communication merge of ACP. All operators of CCS and the three merges mentioned above are GSOS operators [Bloom-Istrail-Meyer, JACM 41(2)].
  As shown in Baeten&Weijland;, CCS with these two auxiliary GSOS operators also allow a finite equational axiomatisation of *branching* bisimulation equivalence on recursion-free CCS.
  So I wonder if the same can be done for weak bisimulation, allowing any number of auxiliary GSOS operators. I don't see how. Can anyone show that it is impossible?
  (Bergstra&Klop; provide a finite equational axiomatisation of weak bisimulation equivalence on recursion-free CCS using the left-merge and a communication merge, but the latter uses lookahead and therefore is not a GSOS operator.)

Problems Posted by Bas Luttik

Problems Posted by Alban Ponse

• Is there a finite equational axiomatization of orthogonal bisimilarity over BPA? (Problem raised by Luca Aceto after looking at slide number 14 of Ponse's talk (PDF).)
• Prove or disprove the conjecture on slide number 21 of his talk (PDF).