Abstract
A symbolic semantics for Full LOTOS in terms of symbolic transition systems is defined, following the approach taken for message passing CCS in [HL95a], altered to take account of the particular features of LOTOS (multi-way synchronisation, value negotiation, selection predicates). Symbolic bisimulation over symbolic transition systems is defined, and symbolic bisimulation on ground behaviour expressions is shown to preserve the usual concrete (strong) bisimulation on the standard semantics. Finally, a modal logic based on symbolic transition systems is defined. All are illustrated with reference to examples.
This author was partially supported by a grant from the British Council enabling travel from Scotland to the Netherlands.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. In P.H.J. van Eijk, C.A. Vissers, and M. Diaz, editors, The Formal Description Technique LOTOS, pages 23–76. Elsevier Science Publishers B.V. (North-Holland), 1989.
T. Bolognesi, editor. Catalogue of LOTOS Correctness Preserving Transformations. Technical Report Lo/WPl/Tl.2/N0045, The LOTOSPHERE Esprit Project, 1992. Task 1.2 deliverable. LOTOSPHERE information disseminated by J. Lagemaat, email lagemaat@cs.utwente.nl.
E. Brinksma. From Data Structure to Process Structure. In K.G. Larsen and A. Skou, editors, Proceedings of CAV 91, LNCS 575, pages 244–254, 1992.
H. Eertink. Simulation Techniques for the Validation of LOTOS Specifications. PhD thesis, University of Twente, 1994.
R. Gotzhein. Specifying Abstract Data Types with LOTOS. In B. Sarikaya and G.V. Bochmann, editors, Protocol Specification, Testing, and Verification, VI, pages 15–26. Elsevier Science Publishers B.V. (North-Holland), 1987.
M. Hennessy and H. Lin. Symbolic Bisimulations. Theoretical Computer Science, 138:353–389, 1995.
M. Hennessy and X. Liu. A Modal Logic for Message Passing Processes. Acta Informatica, 32:375–393, 1995.
M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery, 32(1):137–161, 1985.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
International Organisation for Standardisation. Information Processing Systems — Open Systems Interconnection — LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, 1988.
C. Kirkwood and M. Thomas. Experiences with LOTOS Verification: A Report on Two Case Studies. In Workshop on Industrial-Strength Formal Specification Techniques, pages 159–171. IEEE Computer Society Press, 1995.
R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.
M. Thomas and T. Ormsby. On the Design of Side-Stick Controllers in Fly-by-Wire Aircraft. In Applied Computing Review, Special Issue: Safety-Critical Software, pages 15–20. ACM Press, Volume 2, Number 1 Spring 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shankland, C., Thomas, M. (1997). Symbolic bisimulation for Full LOTOS. In: Johnson, M. (eds) Algebraic Methodology and Software Technology. AMAST 1997. Lecture Notes in Computer Science, vol 1349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000491
Download citation
DOI: https://doi.org/10.1007/BFb0000491
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63888-9
Online ISBN: 978-3-540-69661-2
eBook Packages: Springer Book Archive