On the uniqueness of fixpoints modulo observation congruence

  • Ed Brinksma
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


We revisit the question of the uniqueness of solutions to fixpoint equations modulo observation congruence. In the literature various sufficient conditions are given for the uniqueness of such solutions for a given signature of process combinators, such as guardedness and sequentiality (CCS) or the absence of abstraction (ACP), concealment (CSP), or hiding (LOTOS) combinators. Our study is based on contexts, i.e. behaviour expressions with ‘holes’, whose operational semantics can be characterised by action transductions. Using these we define the context properties of opacity and abstraction-freedom, thus generalising the signature dependent conditions, which can be deduced from these properties. The condition of abstraction-freedom is further improved upon in two ways. First, by relativizing the notion of abstraction-freedom to essential guarding actions, allowing proofs of uniqueness in more cases. Second, by a new criterion based on context transductions that can be applied even more generally. We apply it to a fix-point equation based on a context where a hiding combinator removes what seem to be essential guarding actions. This implies that the condition of (relativised) abstraction-freedom is generally too strict.


Behaviour Expression Operational Semantic Unique Solvability Substitution Factor Abstraction Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BB87]
    Tommaso Bolognesi and Ed Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14:25–59, 1987.CrossRefGoogle Scholar
  2. [BK85]
    J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37(1):77–121, 1985.zbMATHMathSciNetCrossRefGoogle Scholar
  3. [BK89]
    J. A. Bergstra and J. W. Klop. Process theory based on bisimulation semantics. In J. W. de Bakker, Willem-Paul de Roever, and Grzegorz Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 50–122. Springer-Verlag, 1989.Google Scholar
  4. [Bri92]
    Ed Brinksma. On the uniqueness of fixpoints modulo observation congruence. Memoranda informatica, University of Twente, 1992. Forthcoming.Google Scholar
  5. [DNH84]
    Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  6. [GV89]
    Jan Friso Groote and Frits W. Vaandrager. Structured operational semantics and bisimulation as a congruence. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Automata, Languages and Programming, volume 372 of Lecture Notes in Computer Science, pages 423–438. Springer-Verlag, 1989.Google Scholar
  7. [Hoa85]
    C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  8. [ISO89]
    ISO. Information processing systems — open systems interconnection-LOTOS — a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807, ISO, Geneva, February 1989. 1st Edition.Google Scholar
  9. [Kra87]
    E. Kranakis. Fixed point equations with parameters in the projective model. Information and Control, 75(3), 1987.Google Scholar
  10. [Lar90]
    Kim G. Larsen. Compositional theories based on an operational semantics of contexts. In J. W. de Bakker, W. P. de Roever, and Grzegorz Rozenberg, editors, Stepwise Refinement of Distributed Systems — Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 487–518. Springer-Verlag, 1990.Google Scholar
  11. [Mil80]
    R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.Google Scholar
  12. [Mil83]
    R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.zbMATHMathSciNetCrossRefGoogle Scholar
  13. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  14. [San82]
    Michael Thomas Sanderson. Proof Techniques for CCS. PhD thesis, University of Edinburgh, November 1982.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Ed Brinksma
    • 1
  1. 1.Tele-Informatics and Open Systems GroupUniversity of TwenteAE EnschedeThe Netherlands

Personalised recommendations