Introduction to Bisimulation and Coinduction

DOI10.1017/CBO9780511777110zbMath1252.68008OpenAlexW369805404MaRDI QIDQ3118994

Davide Sangiorgi

Publication date: 7 March 2012

Full work available at URL: https://doi.org/10.1017/cbo9780511777110

zbMATH Keywords

fixed pointbisimulationcongruencelabelled transition systemsweak equivalencecoinductionprocess calculustesting scenario

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (84)

Abstraction in Fixpoint Logic ⋮ Bidirectional Runtime Enforcement of First-Order Branching-Time Properties ⋮ Precise Subtyping for Asynchronous Multiparty Sessions ⋮ Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types ⋮ Probabilistic operational semantics for the lambda calculus ⋮ Trees from Functions as Processes ⋮ Applicative Bisimulation and Quantum λ-Calculi ⋮ Unnamed Item ⋮ Structural congruence for bialgebraic semantics ⋮ BISIMULATIONS FOR KNOWING HOW LOGICS ⋮ Verification of finite-state machines: a distributed approach ⋮ Weak Bisimulation as a Congruence in MSOS ⋮ Coupled similarity: the first 32 years ⋮ Fairness and communication-based semantics for session-typed languages ⋮ Virtually timed ambients: a calculus of nested virtualization ⋮ Behavioural equivalences for coalgebras with unobservable moves ⋮ Translation of CCS into CSP, correct up to strong bisimulation ⋮ A formalisation of consistent consequence for Boolean equation systems ⋮ Productive corecursion in logic programming ⋮ Relational properties of sequential composition of coalgebras ⋮ On first-order runtime enforcement of branching-time properties ⋮ Depletable channels: dynamics, behaviour, and efficiency in network design ⋮ From infinity to choreographies. Extraction for unbounded systems ⋮ Asynchronous correspondences between hybrid trajectory semantics ⋮ Parameterizing higher-order processes on names and processes ⋮ Branching Pomsets for Choreographies ⋮ Classical (co)recursion: Mechanics ⋮ Fixpoint Theory -- Upside Down ⋮ A Spatial Logic for Simplicial Models ⋮ The different shades of infinite session types ⋮ THE ZHOU ORDINAL OF LABELLED MARKOV PROCESSES OVER SEPARABLE SPACES ⋮ Unnamed Item ⋮ Towards a process calculus for REST: current state of the art ⋮ Enhanced coalgebraic bisimulation ⋮ Unnamed Item ⋮ SOS rule formats for idempotent terms and idempotent unary operators ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Team equivalences for finite-state machines with silent moves ⋮ Unique solutions of contractions, CCS, and their HOL formalisation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Lattice-valued simulations for quantitative transition systems ⋮ Impossibility of gathering, a certification ⋮ Cathoristic Logic ⋮ A constraint-based language for multiparty interactions ⋮ Team bisimilarity, and its associated modal logic, for BPP nets ⋮ Fixpoint theory -- upside down ⋮ Distributed Modal Logic ⋮ How to Reason Coinductively Informally ⋮ Limited approximate bisimulations and the corresponding rough approximations ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ A language-independent proof system for full program equivalence ⋮ Flag-based big-step semantics ⋮ Explicit Identifiers and Contexts in Reversible Concurrent Calculus ⋮ Reversibility and Predictions ⋮ A general account of coinduction up-to ⋮ Deciding the Bisimilarity of Context-Free Session Types ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ The \(C_\pi\)-calculus: a model for confidential name passing ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A characterization of Moessner's sieve ⋮ Simulation of Action Theories and an Application to General Game-Playing Robots ⋮ On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ A logical and graphical framework for reaction systems ⋮ A monoidal view on fixpoint checks ⋮ Refinements for open automata ⋮ Unnamed Item ⋮ Synchronous gathering without multiplicity detection: a certified algorithm ⋮ Structure in machine learning ⋮ Characterizing contrasimilarity through games, modal logic, and complexity ⋮ Formal definitions and proofs for partial (co)recursive functions ⋮ Transactions and contracts based on reaction systems ⋮ Processes, systems \& tests: defining contextual equivalences ⋮ Processes against tests: on defining contextual equivalences ⋮ Consistently-detecting monitors ⋮ Models and emerging trends of concurrent constraint programming ⋮ On bidirectional runtime enforcement

This page was built for publication: Introduction to Bisimulation and Coinduction