Abstract
An alternative semantic model is that provided by automata, and here we explore how refinement is defined in that setting, introducing the idea of forward and backward simulations. This causes us to consider the role of infinite behaviour in more depth. We discuss completeness results, that is whether the use of simulations is sufficient to verify a refinement. Finally, we introduce the important concept of bisimulation.
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
References
de Roever W-P, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. CUP
Lynch N, Vaandrager FW (1995) Forward and backward simulations I: untimed systems. Inf Comput 121(2):214–233
Lynch N, Vaandrager FW (1996) Forward and backward simulations part II: timing-based systems. Inf Comput 128:1–25
Park D (1981) Concurrency and automata on infinite sequences. In: Deussen P (ed) Theoretical computer science. Lecture notes in computer science, vol 104. Springer, Heidelberg, pp 167–183
Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J. ACM 32(1):137–161
Milner R (1989) Communication and concurrency. Prentice-Hall
Bowman H, Gomez R (2005) Concurrency theory: calculi an automata for modelling untimed and timed concurrent systems. Springer, USA
Klarlund N, Schneider FB (1989) Verifying safety properties using non-deterministic infinite-state automata. Technical report, Cornell University, USA
Klarlund N, Schneider FB (1993) Proving nondeterministically specified safety properties using progress measures. Inf Comput 107(1):151–170
Jonsson B (1991) Simulations between specifications of distributed systems. In: Baeten JCM, Groote JF (eds) CONCUR ’91: 2nd international conference on concurrency theory. Lecture notes in computer science, vol 527. Springer, Heidelberg, pp 346–360
Derrick J, Boiten EA (2014) Refinement in Z and Object-Z, 2nd edn. Springer, Berlin
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Derrick, J., Boiten, E. (2018). Automata - Introducing Simulations. In: Refinement. Springer, Cham. https://doi.org/10.1007/978-3-319-92711-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-92711-4_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-92709-1
Online ISBN: 978-3-319-92711-4
eBook Packages: Computer ScienceComputer Science (R0)