Limit search to available items
Book Cover
E-book
Author Sangiorgi, Davide

Title Advanced Topics in Bisimulation and Coinduction
Published Cambridge : Cambridge University Press, 2011
Online access available from:
Cambridge Core    View Resource Record  

Copies

Description 1 online resource (342 pages)
Series Cambridge Tracts in Theoretical Computer Science ; v. 52
Cambridge tracts in theoretical computer science.
Contents Cover; Cambridge Tracts in Theoretical Computer Science 52; Title; Copyright; Contents; Contributors; Preface; 1 Origins of bisimulation and coinduction; 1.1 Introduction; 1.2 Bisimulation in modal logic; 1.2.1 Modal logics; 1.2.2 From homomorphism to p-morphism; 1.2.3 Johan van Benthem; 1.2.4 Discussion; 1.3 Bisimulation in computer science; 1.3.1 Algebraic theory of automata; 1.3.2 Robin Milner; 1.3.3 David Park; 1.3.4 Discussion; 1.4 Set theory; 1.4.1 Non-well-founded sets; 1.4.2 The stratified approach to set theory; 1.4.3 Non-well-founded sets and extensionality
1.4.4 Marco Forti and Furio Honsell1.4.5 Peter Aczel; 1.4.6 Jon Barwise; 1.4.7 Extensionality quotients: Roland Hinnion and others; 1.4.8 Discussion; 1.5 The introduction of fixed points in computer science; 1.6 Fixed-point theorems; Bibliography; 2 An introduction to (co)algebra and (co)induction; 2.1 Introduction; 2.2 Algebraic and coalgebraic phenomena; 2.3 Inductive and coinductive definitions; 2.4 Functoriality of products, coproducts and powersets; 2.5 Algebras and induction; 2.6 Coalgebras and coinduction; 2.7 Proofs by coinduction and bisimulation; 2.8 Processes coalgebraically
2.9 Trace semantics, coalgebraically2.10 Exercises; Bibliography; 3 The algorithmics of bisimilarity; 3.1 Introduction; 3.2 Classical algorithms for bisimilarity; 3.2.1 Preliminaries; 3.2.2 The algorithm of Kanellakis and Smolka; 3.2.3 The algorithm of Paige and Tarjan; 3.2.4 Computing bisimilarity, symbolically; 3.2.5 Checking weak equivalences; 3.3 The complexity of checking bisimilarityover finite processes; 3.3.1 Game characterisation of bisimulation-like relations; 3.3.2 Deciding bisimilarity over finite labelledtransition systems is P-complete
3.3.3 EXPTIME-completeness of equivalence checking on networks of finite processes3.4 Decidability results for bisimilarity overinfinite-state systems; 3.4.1 Process rewrite systems; 3.4.2 Deciding bisimilarity on BPP using a tableau technique; 3.4.3 Undecidability of bisimilarity on Petri nets; 3.4.4 Overview of results; 3.5 The use of bisimilarity checking in verification and tools; 3.5.1 Some uses of bisimilarity checking; 3.5.2 Concluding remarks; Bibliography; 4 Bisimulation and logic; 4.1 Introduction; 4.2 Modal logic and bisimilarity; 4.3 Bisimulation invariance; 4.4 Modal mu-calculus
4.5 Monadic second-order logic and bisimulation invarianceBibliography; 5 Howe's method for higher-order languages; 5.1 Introduction; 5.2 Call-by-value?-calculus; 5.3 Applicative (bi)similarity for call-by-value?-calculus; 5.4 Congruence; 5.5 Howe's construction; 5.6 Contextual equivalence; 5.7 The transitive closure trick; 5.8 CIU-equivalence; 5.9 Call-by-name equivalences; 5.10 Summary; 5.11 Assessment; Bibliography; 6 Enhancements of the bisimulation proof method; 6.1 The need for enhancements; 6.1.1 The bisimulation game; 6.1.2 Tracking redundancies; 6.2 Examples of enhancements
Summary Seven articles survey the state of the art. Discusses various aspects of the subject, with an emphasis on process theory
Notes 6.2.1 Diagram-based enhancements
Bibliography Includes bibliographical references and index
Notes English
Print version record
Subject Computer simulation.
Computer science -- Philosophy
Digital computer simulation.
simulation.
COMPUTERS -- Networking -- General.
Digital computer simulation
Computer science -- Philosophy
Computer simulation
Form Electronic book
Author Rutten, Jan
ISBN 9781139159340
1139159348
9781107004979
1107004977
9780511792588
0511792581
9781139161398
1139161393