Skip to main content
SpringerLink
Log in

On the uniqueness of fixpoints modulo observation congruence

  • Conference paper
  • First Online:
CONCUR '92 (CONCUR 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 630))

Included in the following conference series:

  • 165 Accesses

Abstract

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.

This work has been supported in part by the CEC research programme ESPRIT (LOTOSPHERE, ref: 2303).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Tommaso Bolognesi and Ed Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14:25–59, 1987.

    Article  Google Scholar 

  2. J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37(1):77–121, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  3. 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. Ed Brinksma. On the uniqueness of fixpoints modulo observation congruence. Memoranda informatica, University of Twente, 1992. Forthcoming.

    Google Scholar 

  5. Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  6. 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. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    Google Scholar 

  8. 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. E. Kranakis. Fixed point equations with parameters in the projective model. Information and Control, 75(3), 1987.

    Google Scholar 

  10. 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. R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

    Google Scholar 

  12. R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  13. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  14. Michael Thomas Sanderson. Proof Techniques for CCS. PhD thesis, University of Edinburgh, November 1982.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Tele-Informatics and Open Systems Group, University of Twente, P.O. Box 217, 7500, AE Enschede, The Netherlands

    Ed Brinksma

Authors
  1. Ed Brinksma
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

W.R. Cleaveland

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brinksma, E. (1992). On the uniqueness of fixpoints modulo observation congruence. In: Cleaveland, W. (eds) CONCUR '92. CONCUR 1992. Lecture Notes in Computer Science, vol 630. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0084782

Download citation

  • DOI: https://doi.org/10.1007/BFb0084782

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55822-4

  • Online ISBN: 978-3-540-47293-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation