Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Labeled Transition Systems and Their Refinement Read chapter Read first chapter

2018 | OriginalPaper | Chapter

2. Automata - Introducing Simulations

Authors : John Derrick, Eerke Boiten

Published in: Refinement

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Labeled Transition Systems and Their Refinement
next chapter Simple State-Based Refinement
Literature
1.
de Roever W-P, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. CUP
2.
3.
Lynch N, Vaandrager FW (1996) Forward and backward simulations part II: timing-based systems. Inf Comput 128:1–25CrossRef
4.
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
5.
Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J. ACM 32(1):137–161CrossRef
6.
Milner R (1989) Communication and concurrency. Prentice-Hall
7.
Bowman H, Gomez R (2005) Concurrency theory: calculi an automata for modelling untimed and timed concurrent systems. Springer, USAMATH
8.
Klarlund N, Schneider FB (1989) Verifying safety properties using non-deterministic infinite-state automata. Technical report, Cornell University, USA
9.
Klarlund N, Schneider FB (1993) Proving nondeterministically specified safety properties using progress measures. Inf Comput 107(1):151–170MathSciNetCrossRef
10.
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
11.
Derrick J, Boiten EA (2014) Refinement in Z and Object-Z, 2nd edn. Springer, BerlinCrossRef
Metadata
Title
Automata - Introducing Simulations
Authors
John Derrick
Eerke Boiten
Copyright Year
2018
Book
Refinement

Print ISBN: 978-3-319-92709-1

Electronic ISBN: 978-3-319-92711-4

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-319-92711-4_2

Premium Partner

    Image Credits