Forward and backward simulations. I. Untimed Systems
From MaRDI portal
Publication:1899913
DOI10.1006/inco.1995.1134zbMath0834.68123OpenAlexW2328819335MaRDI QIDQ1899913
Nancy A. Lynch, Frits W. Vaandrager
Publication date: 14 November 1995
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1995.1134
Related Items
Reversibility in the higher-order \(\pi\)-calculus ⋮ Weak equivalence of higher-dimensional automata ⋮ Weak bisimulations for fuzzy automata ⋮ Verifying Visibility-Based Weak Consistency ⋮ Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory ⋮ Liveness in timed and untimed systems ⋮ Precise specification matching for adaptive reuse in embedded systems ⋮ Algebraic simulations ⋮ Theorem-proving anonymity of infinite-state systems ⋮ Focus points and convergent process operators: A proof strategy for protocol verification ⋮ Checking the Conformance of a Promela Design to its Formal Specification in Event-B ⋮ Fuzzy approximations of fuzzy relational structures ⋮ Cones and foci: A mechanical framework for protocol verification ⋮ Comparative branching-time semantics for Markov chains ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ Incompleteness of relational simulations in the blocking paradigm ⋮ A criterion for atomicity revisited ⋮ A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Characterization and computation of approximate bisimulations for fuzzy automata ⋮ On the greatest solutions to weakly linear systems of fuzzy relation inequalities and equations ⋮ A basic compositional model for spiking neural networks ⋮ On specifications and proofs of timed circuits ⋮ Faster asynchronous systems. ⋮ Temporal-logic property preservation under Z refinement ⋮ Using schedulers to test probabilistic distributed systems ⋮ Bisimulations for fuzzy automata ⋮ Nondeterministic automata: equivalence, bisimulations, and uniform relations ⋮ Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability ⋮ Hybrid I/O automata. ⋮ Starvation-free mutual exclusion with semaphores ⋮ Towards formally specifying and verifying transactional memory ⋮ Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study ⋮ Lattice-valued simulations for quantitative transition systems ⋮ Compositional Abstraction in Real-Time Model Checking ⋮ Relational Concurrent Refinement: Automata ⋮ Distributed consensus, revisited ⋮ Limited approximate bisimulations and the corresponding rough approximations ⋮ Verifying correctness of persistent concurrent data structures: a sound and complete method ⋮ Simulation Refinement for Concurrency Verification ⋮ Completeness of ASM Refinement ⋮ General Refinement, Part One: Interfaces, Determinism and Special Refinement ⋮ Büchi Automata Can Have Smaller Quotients ⋮ Reasoning with Uncertain and Inconsistent OWL Ontologies ⋮ Comparing disjunctive modal transition systems with an one-selecting variant ⋮ Universal extensions to simulate specifications ⋮ Reconciling fault-tolerant distributed algorithms and real-time computing ⋮ Computation of the greatest simulations and bisimulations between fuzzy automata ⋮ Finite and infinite implementation of transition systems ⋮ Remarks on Thatte's transformation of term rewriting systems ⋮ Simulation refinement for concurrency verification ⋮ Completeness of fair ASM refinement ⋮ Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract) ⋮ A menagerie of timed automata ⋮ Simulations in coalgebra ⋮ Turing machines, transition systems, and interaction ⋮ Probabilistic anonymity via coalgebraic simulations ⋮ Splitting forward simulations to cope with liveness ⋮ Fast asynchronous systems in dense time ⋮ ASM refinement and generalizations of forward simulation in data refinement: a comparison ⋮ Nonblocking \(k\)-compare-single-swap ⋮ Fuzzy relation equations and reduction of fuzzy automata ⋮ Branching time controllers for discrete event systems ⋮ Reduction of fuzzy automata by means of fuzzy quasi-orders ⋮ Refinement verification of the lazy caching algorithm ⋮ Quantitative simulations by matrices ⋮ Unnamed Item ⋮ Computation of the greatest right and left invariant fuzzy quasi-orders and fuzzy equivalences ⋮ Towards a real-time distributed computing model ⋮ Relational concurrent refinement. III: Traces, partial relations and automata ⋮ Unnamed Item ⋮ Trace-based derivation of a scalable lock-free stack algorithm ⋮ Liveness in timed and untimed systems ⋮ Category Theoretic Models of Data Refinement ⋮ On the refinement of liveness properties of distributed systems ⋮ Eventually-serializable data services ⋮ Unwinding Possibilistic Security Properties ⋮ Monte Carlo Methods for Process Algebra ⋮ State-level and value-level simulations in data refinement ⋮ Efficiency of asynchronous systems, read arcs, and the MUTEX-problem
