Abstract
We provide rules for calculating with invariants in process algebra with data, and illustrate these with examples. The new rules turn out to be equivalent to the well known Recursive Specification Principle which states that guarded recursive equations have at most one solution. In the setting with data this is reformulated as ‘every convergent linear process operator has at most one fixed point’ (CL-RSP). As a consequence, one can carry out verifications in well-known process algebras satisfying CL-RSP using invariants.
The authors are partly supported by the Netherlands Computer Science Research Foundation (SION) with financial support of the Netherlands Organization for Scientific Research (NWO).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.C.M. Baeten, editor. Applications of Process Algebra. Cambridge Tracts in Theoretical Computer Science 17. Cambridge University Press, 1990.
J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.
M.A. Bezem and J.F. Groote. A correctness proof of a one bit sliding window protocol in µCRL. Technical report, Logic Group Preprint Series no. 99, Utrecht University, 1993. To appear in The Computer Journal.
M.A. Bezem, J.F. Groote and J.J. van Wamel. A correctness proof of a sliding window protocol in µCRL. Technical report, Logic Group Preprint Series, Utrecht University, 1994. To appear.
K.M. Chandy and J. Misra. Parallel Program Design. A Foundation. Addison-Wesley, 1988.
L. Fredlund, J.F. Groote and H. Korver. A verification of a leader election protocol in µCRL, 1994. To appear.
R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In G.X. Ritter, editor, Information Processing 89, pages 613–618. North-Holland, 1989. Full version available as Report CS-R9120, CWI, Amsterdam, 1991.
R.A. Groenveld. Verification of a sliding window protocol by means of process algebra. Report P8701, Programming Research Group, University of Amsterdam, 1987.
J.F. Groote and A. Ponse. The syntax and semantics of µCRL. Technical Report CS-R9076, CWI, Amsterdam, December 1990.
J.F. Groote and A. Ponse. Process algebra with guards. Combining Hoare logic and process algebra (Extended abstract). In J.C.M. Baeten and J.F. Groote, editors, Proceedings CONCUR 91 Amsterdam, volume 527 of Lecture Notes in Computer Science pages 235–249. Springer-Verlag, 1991. Full version appeared as Technical Report CS-R9069, CWI, Amsterdam, 1990; and is to appear in Formal Aspects of Computing.
J.F. Groote and A. Ponse. Proof theory for µCRL. Technical Report CS-R9138, CWI, Amsterdam, August 1991.
J.F. Groote and A. Ponse. Proof theory for µCRL: a language for processes with data. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors. Proceedings of the International Workshop on Semantics of Specification Languages, pages 231250. Workshops in Computer Science, Springer Verlag, 1994.
E.C.R. Hehner. od Considered od: A contribution to the programming calculus. Acta Informatica, 11: 287–304, 1979.
A. Ponse. Process expressions and Hoare’s logic. Information and Computation, 95 (2): 192–217, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bezem, M., Groote, J.F. (1994). Invariants in Process Algebra with Data. In: Jonsson, B., Parrow, J. (eds) CONCUR ’94: Concurrency Theory. CONCUR 1994. Lecture Notes in Computer Science, vol 836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-48654-1_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-48654-1_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58329-5
Online ISBN: 978-3-540-48654-1
eBook Packages: Springer Book Archive