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

Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions, Morphisms and Minimisation of Weighted Automata, PROBABILISTIC ROLE MODELS AND THE GUARDED FRAGMENT, On Applicative Similarity, Sequentiality, and Full Abstraction, Statistical Model Checking for Networks of Priced Timed Automata, Model Checking Probabilistic Systems, Applicative Bisimulation and Quantum λ-Calculi, Bisimulation as a logical relation, Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence, Deriving Syntax and Axioms for Quantitative Regular Behaviours, Weighted Bisimulation in Linear Algebraic Form, A Demonic Approach to Information in Probabilistic Systems, Structural Operational Semantics for Weighted Transition Systems, Unnamed Item, Unnamed Item, Generic Infinite Traces and Path-Based Coalgebraic Temporal Logics, Converging from branching to linear metrics on Markov chains, Model Checking Linear-Time Properties of Probabilistic Systems, An algebra-based method to associate rewards with EMPA terms, Symbolic model checking for probabilistic processes, A Tutorial on Interactive Markov Chains, A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems, Formalizing Probabilistic Noninterference, A Formalized Hierarchy of Probabilistic System Types, When Are Prime Formulae Characteristic?, Differential Bisimulation for a Markovian Process Algebra, Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions, Reasoning with Global Assumptions in Arithmetic Modal Logics, Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement, Quantitative analysis of interval Markov chains, Probabilistic concurrent constraint programming, Bisimulations for non-deterministic labelled Markov processes, Bisimulations of Probabilistic Boolean Networks, Deciding Simulations on Probabilistic Automata, Unnamed Item, Unnamed Item, Unnamed Item, A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories, Unnamed Item, Compositional bisimulation metric reasoning with Probabilistic Process Calculi, EQUIVALENCE OF LABELED MARKOV CHAINS, On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context, Unnamed Item, Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains, From Gene Regulation to Stochastic Fusion, Logical relations for monadic types, On deciding some equivalences for concurrent processes, Asymmetric Distances for Approximate Differential Privacy, Coalgebraic logic over general measurable spaces – a survey, Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra, WEIGHTED AUTOMATA AS COALGEBRAS IN CATEGORIES OF MATRICES, Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation, Modular Markovian Logic, VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC, A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols, Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations, Bisimulation on Markov Processes over Arbitrary Measurable Spaces, The Complexity of Computing a Bisimilarity Pseudometric on Probabilistic Automata, Free Energy of Petri Nets, Bisimulation for Markov Decision Processes through Families of Functional Expressions, Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice, Linear Structures for Concurrency in Probabilistic Programming Languages, Equivalence relations for modular performance evaluation in dtsPBC, Quantales, finite observations and strong bisimulation, Bisimilarity is not Borel, Corrigendum to ``A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time, Global Caching for Coalgebraic Description Logics, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Process algebra for performance evaluation, Model checking for a class of weighted automata, Testing preorders for probabilistic processes, Coalgebraic Hybrid Logic, Concurrency, σ-Algebras, and Probabilistic Fairness, A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems, Unnamed Item, Unnamed Item, Unnamed Item, Approximating Markov Processes by Averaging, Symbolic computation of differential equivalences, Timed Automata Can Always Be Made Implementable, Bisimulations Meet PCTL Equivalences for Probabilistic Automata, A Spectrum of Behavioral Relations over LTSs on Probability Distributions, OBLIGATION BLACKWELL GAMES AND P-AUTOMATA, A Formal Framework for User Centric Control of Probabilistic Multi-agent Cyber-Physical Systems, CoLoSS: The Coalgebraic Logic Satisfiability Solver, Non-termination and secure information flow, Axiomatizing Weak Ready Simulation Semantics over BCCSP, Efficient Coalgebraic Partition Refinement, Non Expansive ε-Bisimulations, Bisimulation for probabilistic transition systems: A coalgebraic approach, Unnamed Item, Bisimulation and Simulation Relations for Markov Chains, Markovian Testing and Trace Equivalences Exactly Lump More Than Markovian Bisimilarity, Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey, General patterns of interaction in stochastic fusion, Belief and truth in hypothesised behaviours, A metrized duality theorem for Markov processes, Identifying all preorders on the subdistribution monad, A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces, Timed process calculi with deterministic or stochastic delays: commuting between durational and durationless actions, A logic for reasoning about time and reliability, Processes with probabilities, priority and time, Ready to preorder: an algebraic and general proof, Switched PIOA: parallel composition via distributed scheduling, Preferential choice and coordination conditions, A pseudometric in supervisory control of probabilistic discrete event systems, Two-thirds simulation indexes and modal logic characterization, Metrics for labelled Markov processes, Quantitative analysis of software approximate correctness, Behavioural equivalences of a probabilistic pi-calculus, A game-based abstraction-refinement framework for Markov decision processes, Conjunction on processes: Full abstraction via ready-tree semantics, SOS formats and meta-theory: 20 years after, Parametric probabilistic transition systems for system design and analysis, Weak bisimulation for probabilistic timed automata, Testing probabilistic equivalence through reinforcement learning, Structural operational semantics for stochastic and weighted transition systems, A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time, SOS specifications for uniformly continuous operators, A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences, Probabilistic bisimilarity as testing equivalence, \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics, Composition and behaviors of probabilistic I/O automata, Axiomatizing Lüttgen \& Vogler's ready simulation for finite processes in \(\mathrm{CLL}_{R}\), Approximating labelled Markov processes, The power of reachability testing for timed automata, Algebraic theory of probabilistic and nondeterministic processes., On the use of MTBDDs for performability analysis and verification of stochastic systems., Algebraic theory of probabilistic processes., A coalgebraic perspective on linear weighted automata, Measurable stochastics for Brane calculus, Lumpability abstractions of rule-based systems, Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems, Integrating stochastic reasoning into Event-B development, Value-passing CCS with noisy channels, Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation, On behavioural pseudometrics and closure ordinals, The infinite evolution mechanism of \(\epsilon\)-bisimilarity, Equivalences for a biological process algebra, Lattice-valued simulations for quantitative transition systems, Constructive logical characterizations of bisimilarity for reactive probabilistic systems, Verification and control for probabilistic hybrid automata with finite bisimulations, Probabilistic communicating processes, Stochastic coalgebraic logic: bisimilarity and behavioral equivalence, Approximate relational Hoare logic for continuous random samplings, Structural operational semantics for non-deterministic processes with quantitative aspects, Logical characterizations of simulation and bisimulation for fuzzy transition systems, Model-based testing of probabilistic systems, Comparing disjunctive modal transition systems with an one-selecting variant, Transition system specifications with negative premises, Structured operational semantics and bisimulation as a congruence, Lumping-based equivalences in Markovian automata: algorithms and applications to product-form analyses, Algorithms for task allocation in ants. (A study of temporal polyethism: Theory), Automatic verification of distributed systems: the process algebra approach., CSP is a retract of CCS, Differential privacy in probabilistic systems, Quantitative Kleene coalgebras, A logical duality for underspecified probabilistic systems, On metrics for probabilistic systems: definitions and algorithms, A hierarchy of probabilistic system types, A compositional approach to defining logics for coalgebras, Unprovability of the logical characterization of bisimulation, Non-expansive \(\varepsilon\)-bisimulations for probabilistic processes, Domain theory, testing and simulation for labelled Markov processes, A behavioural pseudometric for probabilistic transition systems, A translation of \(\text{TPAL}_{p}\) into a class of timed-probabilistic Petri nets, Measuring the confinement of probabilistic systems, Weakening the perfect encryption assumption in Dolev-Yao adversaries, On the metric-based approximate minimization of Markov chains, Kleisli morphisms and randomized congruences for the Giry monad, Tempus fugit: How to plug it, Probabilistic mobile ambients, (Bi)simulations up-to characterise process semantics, LOTOS extended with probabilistic behaviours, Optimal state-space lumping in Markov chains, Coalgebraic logic for stochastic right coalgebras, Priority as extremal probability, A formal approach to the integration of performance aspects in the modeling and analysis of concurrent systems, A linear process-algebraic format with data for probabilistic automata, Branching bisimulation congruence for probabilistic systems, Domain semantics of possibility computations, Coalgebraic logic, Universal coalgebra: A theory of systems, Measure and probability for concurrency theorists, Performance measure sensitive congruences for Markovian process algebras, Discrete time generative-reactive probabilistic processes with different advancing speeds, Testing preorders for probabilistic processes., The theory of interactive generalized semi-Markov processes, Testing preorders for probabilistic processes can be characterized by simulations, Automatic verification of real-time systems with discrete probability distributions., A process algebra for probabilistic and nondeterministic processes, Additive models of probabilistic processes, Equivalence notions and model minimization in Markov decision processes, Kantorovich functors and characteristic logics for behavioural distances, Reverse bisimilarity vs. forward bisimilarity, Explainability of probabilistic bisimilarity distances for labelled Markov chains, Weighted and branching bisimilarities from generalized open maps, Extended Markovian Process Algebra, Guaranteed Error Bounds on Approximate Model Abstractions Through Reachability Analysis, Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach, Convex lattice equation systems, Sound approximate and asymptotic probabilistic bisimulations for PCTL, Bridging Causal Reversibility and Time Reversibility: A Stochastic Process Algebraic Approach, Back to the format: a survey on SOS for probabilistic processes, Probabilistic weak bisimulation and axiomatization for probabilistic models, Equivalence checking 40 years after: a review of bisimulation tools, Approximate constrained lumping of polynomial differential equations, 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