Bisimulation through probabilistic testing

DOI10.1016/0890-5401(91)90030-6zbMath0756.68035OpenAlexW1976268573MaRDI QIDQ1175940

Publication date: 25 June 1992

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(91)90030-6

zbMATH Keywords

Hennessy-Milner logic concurrent process probabilistic testing

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (only showing first 100 items - show all)

Characteristic formulae for fixed-point semantics: a general framework ⋮ Approximating Labelled Markov Processes Again! ⋮ Non-strongly Stable Orders Also Define Interesting Simulation Relations ⋮ Refinement-oriented probability for CSP ⋮ Testing equivalence as a bisimulation equivalence ⋮ The Equational Theory of Weak Complete Simulation Semantics over BCCSP ⋮ A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols ⋮ Specification, testing and implementation relations for symbolic-probabilistic systems ⋮ Behavioural differential equations: a coinductive calculus of streams, automata, and power series ⋮ Bisimulation for Feller-Dynkin processes ⋮ Towards a classification of behavioural equivalences in continuous-time Markov processes ⋮ The Hennessy-Milner equivalence for continuous time stochastic logic with mu-operator ⋮ Non-bisimulation-based Markovian behavioral equivalences ⋮ Resources in process algebra ⋮ Recursively defined metric spaces without contraction ⋮ A general SOS theory for the specification of probabilistic transition systems ⋮ A space-efficient simulation algorithm on probabilistic automata ⋮ An efficient algorithm to determine probabilistic bisimulation ⋮ Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC ⋮ Trust evidence logic ⋮ A domain equation for bisimulation ⋮ Typed Linear Algebra for Weigthed (Probabilistic) Automata ⋮ Bisimulations for neural network reduction ⋮ Comparative branching-time semantics for Markov chains ⋮ A finite model construction for coalgebraic modal logic ⋮ A perspective on service orchestration ⋮ Probabilistic model checking of BPMN processes at runtime ⋮ Equivalences for fluid stochastic Petri nets ⋮ Compositional abstraction-based synthesis for networks of stochastic switched systems ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes ⋮ Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach ⋮ Determining asynchronous test equivalence for probabilistic processes ⋮ Expressiveness of probabilistic modal logics: a gradual approach ⋮ Towards a linear algebra of programming ⋮ Using schedulers to test probabilistic distributed systems ⋮ Probabilistic may/must testing: retaining probabilities by restricted schedulers ⋮ Complete and ready simulation semantics are not finitely based over BCCSP, even with a singleton alphabet ⋮ Computing branching distances with quantitative games ⋮ Discrete time stochastic and deterministic Petri box calculus dtsdPBC ⋮ Bisimulation for probabilistic transition systems: A coalgebraic approach ⋮ Linking theories in probabilistic programming ⋮ Axiomatizing weighted synchronization trees and weighted bisimilarity ⋮ Axiomatizing weak simulation semantics over BCCSP ⋮ Characteristic Formulae for Timed Automata ⋮ A quantified coalgebraic van Benthem theorem ⋮ Probabilistic bisimulations for quantum processes ⋮ The reactive simulatability (RSIM) framework for asynchronous systems ⋮ Modular construction of complete coalgebraic logics ⋮ Towards general axiomatizations for bisimilarity and trace semantics ⋮ The metric linear-time branching-time spectrum on nondeterministic probabilistic processes ⋮ Expressivity of coalgebraic modal logic: the limits and beyond ⋮ Model checking for probabilistic timed automata ⋮ Unnamed Item ⋮ Relating strong behavioral equivalences for processes with nondeterminism and probabilities ⋮ A congruence relation for sPBC ⋮ Bisimulation relations for weighted automata ⋮ Deciding probabilistic bisimilarity over infinite-state probabilistic systems ⋮ Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes ⋮ Probabilistic divide \& congruence: branching bisimilarity ⋮ Branching bisimulation for probabilistic systems: characteristics and decidability ⋮ Weak bisimulation is sound and complete for pCTL\(^*\) ⋮ A modular approach to defining and characterising notions of simulation ⋮ Bisimulation and cocongruence for probabilistic systems ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Logical characterization of branching metrics for nondeterministic probabilistic transition systems ⋮ Splitting bisimulations and retrospective conditions ⋮ Probabilistic event structures and domains ⋮ Approximating and computing behavioural distances in probabilistic transition systems ⋮ Bisimulation for labelled Markov processes ⋮ Probabilistic NetKAT ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ A linear-time-branching-time spectrum for behavioral specification theories ⋮ A probabilistic calculus of cyber-physical systems ⋮ Quantitative Abstractions for Collective Adaptive Systems ⋮ Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations ⋮ Probabilistic model of software approximate correctness ⋮ Bisimulation metrics and norms for real-weighted automata ⋮ Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations ⋮ Logical characterization of fluid equivalences ⋮ GSOS for probabilistic transition systems ⋮ Bisimulation Relations for Dynamical and Control Systems ⋮ Processes against tests: on defining contextual equivalences ⋮ Model checking for performability ⋮ Bisimulation relations for dynamical, control, and hybrid systems ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ \(\pi\)-calculus with noisy channels ⋮ A theory of stochastic systems. I: Stochastic automata ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Remarks on Testing Probabilistic Processes ⋮ Labelled Markov Processes as Generalised Stochastic Relations ⋮ Proving Approximate Implementations for Probabilistic I/O Automata ⋮ On the verification of qualitative properties of probabilistic processes under fairness constraints. ⋮ Notes on Generative Probabilistic Bisimulation ⋮ Probabilistic π-Calculus and Event Structures ⋮ Probabilistic Barbed Congruence ⋮ Simulations Up-to and Canonical Preorders ⋮ An Exercise on Transition Systems ⋮ Abstraction-based segmental simulation of chemical reaction networks ⋮ The max-plus algebra of the natural numbers has no finite equational basis

Cites Work

This page was built for publication: Bisimulation through probabilistic testing