Abstract
This work has been motivated by the study of the S/R models which allow to represent systems as a set of communicating state machines cooperating through a shared memory.
We show that S/R models can be expressed in terms of a process algebra called Boolean SCCS which is a special case of Milner's SCCS, in the sense that the actions are elements of some boolean algebra. We define for Boolean SCCS an operational and a symbolic semantics modulo strong bisimulation equivalence. A complete axiomatisation of bisimulation and simulation equivalences on this algebra is proposed.
Furthermore, we propose a very general renaming operator, and show by means of examples that it allows the definition of abstractions.
This work has been partially supported by ESPRIT Basic Research Action ‘Spec’
Chapter PDF
References
S. Aggarwal, D. Barbara, K. Z. Meth. “SPANNER-A Tool for the Specification, Analysis, and Evaluation of Protocols,” IEEE Trans. on Software Engineering (to appear).
S. Aggarwal, C. Courcoubetis. “Distributed Implementation of a Model of Communication and Computation,” Proceedings of the Int. Conf. on System Sciences, January, 1985.
S. Aggarwal, R. P. Kurshan, K. K. Sabnani. “A Calculus for Protocol Specification and Validation,” in Protocol Specification, Testing and Verification III, North-Holland, 1983.
R. Kurshan, “Analysis of Discrete Event Coordination”. LNCS 430 (1990).
S. Aggarwal, C. Courcoubetis, P. Wolper. “Adding Liveness Properties to Coupled Finite-State Machines”, ACM TOPLAS, Vol. 12, No 2, April 1990.
B. Gopinath, B. Kurshan. “The Selection/Resolution Model for Coordinating Concurrent Processes”, AT&T Bell Laboratories Technical Report.
J. Katzenelson, B. Kurshan, “S/R: A Language for Specifying Protocols and other Coordinating Processes”, Proc. 5th Ann. Int'l Phoenix Conf. Comput. Commun., IEEE, 1986.
A. Bouajjani, J.-C. Fernandez, S. Graf, C. Rodriguez, J. Sifakis. Safety for Branching Semantics, ICALP 91, Madrid, LNCS Vol. 510, 1991.
F. Maraninchi. Argos: a graphical synchronous language for the description of reactive systems, Report Spectre C-29, Grenoble, March 91, submitted to SCP
R. Milner. A Calculus for Communicating Systems, LNCS 92, 1980
R. Milner. Calculi for Synchrony and Asynchrony, Theoret. Comp. Sci. 25, 1983.
R. Milner. A Complete Inference System for a Class of Regular Behaviours, Journal of Comp. and Syst. Sci. Vol. 28, 1984
R. Milner. Communication and Concurrency, Prentice Hall, 1989
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Courcoubetis, C., Graf, S., Sifakis, J. (1992). An algebra of Boolean processes. In: Larsen, K.G., Skou, A. (eds) Computer Aided Verification. CAV 1991. Lecture Notes in Computer Science, vol 575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55179-4_42
Download citation
DOI: https://doi.org/10.1007/3-540-55179-4_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55179-9
Online ISBN: 978-3-540-46763-2
eBook Packages: Springer Book Archive