Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
The logic PML is a probabilistic version of modal logic, called Hennessy-Milner logic. Its diamond operator is decorated with a probability bound, i.e., formula \(\langle a\rangle_p\phi\) is satisfied by state \(s\) if an \(a\)-labelled transition is possible from \(s\) after which a set of states satisfying \(\phi\) is reached with probability at least \(p\). From the authors' abstract: Two alternative interpretations of PML over nondeterministic and probabilistic processes are considered and two new bisimulation-based equivalences that are in full agreement with those interpretations are provided. The new equivalences include as coarsest congruences the two bisimilarities for nondeterministic and probabilistic processes proposed by Segala and Lynch. The new interpretations of PML and the corresponding new bisimilarities are the first ones to offer a uniform framework for reasoning on processes that are purely nondeterministic or reactive probabilistic (no state has two or more outgoing transitions labelled by the same action) or that mix nondeterminism and probability in an alternating/nonalternanting way.
- A hierarchy of probabilistic system types
- A logic for reasoning about time and reliability
- A spectrum of behavioral relations over LTSs on probability distributions
- A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
- Algebraic laws for nondeterminism and concurrency
- Approximating labelled Markov processes
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Bisimulation for labelled Markov processes
- Bisimulation for probabilistic transition systems: A coalgebraic approach
- Bisimulation through probabilistic testing
- Bisimulations meet PCTL equivalences for probabilistic automata
- Characterizing finite Kripke structures in propositional temporal logic
- Coalgebraic modal logic beyond sets
- Deduction systems for coalgebras over measurable spaces
- Domain equations for probabilistic processes
- Editorial. Coalgebra and logic: a brief overview
- Exploring probabilistic bisimulations. I
- Finite state Markovian decision processes
- Formal verification of parallel programs
- Foundations of Software Science and Computational Structures
- Game Refinement Relations and Metrics
- Group-by-group probabilistic bisimilarities and their logical characterizations
- scientific article; zbMATH DE number 1759621 (Why is no real title available?)
- scientific article; zbMATH DE number 794262 (Why is no real title available?)
- scientific article; zbMATH DE number 7318983 (Why is no real title available?)
- Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
- Model checking of probabilistic and nondeterministic systems
- Probabilistic automata
- Probabilistic logical characterization
- Probabilistic models for the guarded command language
- Reactive, generative, and stratified models of probabilistic processes
- Three logics for branching bisimulation
- Validation of Stochastic Systems
- Weak bisimulation is sound and complete for pCTL\(^*\)
- Bisimulations for fuzzy transition systems revisited
- \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics
- Exploring probabilistic bisimulations. I
- Towards general axiomatizations for bisimilarity and trace semantics
- Logical characterization of branching metrics for nondeterministic probabilistic transition systems
- Bisimilar and logically equivalent programs in PDL
- Group-by-group probabilistic bisimilarities and their logical characterizations
- scientific article; zbMATH DE number 5295708 (Why is no real title available?)
- A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
- Convenient category of processes and simulations I: Modulo strong bisimilarity
- A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems
- Interval probability for sessions types
- Logical characterization of bisimulation metrics
This page was built for publication: Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2257984)
