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 traces and deadlock behaviour (i.e. is finer than completed trace equivalence)

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

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