On the uniqueness of fixpoints modulo observation congruence
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.
KeywordsBehaviour Expression Operational Semantic Unique Solvability Substitution Factor Abstraction Operator
Unable to display preview. Download preview PDF.
- [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
- [Bri92]Ed Brinksma. On the uniqueness of fixpoints modulo observation congruence. Memoranda informatica, University of Twente, 1992. Forthcoming.Google Scholar
- [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
- [Hoa85]C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
- [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
- [Kra87]E. Kranakis. Fixed point equations with parameters in the projective model. Information and Control, 75(3), 1987.Google Scholar
- [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
- [Mil80]R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.Google Scholar
- [Mil89]R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
- [San82]Michael Thomas Sanderson. Proof Techniques for CCS. PhD thesis, University of Edinburgh, November 1982.Google Scholar