Logical characterization of branching metrics for nondeterministic probabilistic transition systems
From MaRDI portal
Publication:2272986
DOI10.1016/j.ic.2019.06.001zbMath1430.68161OpenAlexW2949241705WikidataQ127701802 ScholiaQ127701802MaRDI QIDQ2272986
Simone Tini, Valentina Castiglioni
Publication date: 17 September 2019
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2019.06.001
metric semanticslogical characterizationnondeterministic probabilistic transition systemsbranching metrics
Logic in computer science (03B70) 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
A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces ⋮ SOS specifications for uniformly continuous operators ⋮ Explainability of probabilistic bisimilarity distances for labelled Markov chains ⋮ The metric linear-time branching-time spectrum on nondeterministic probabilistic processes ⋮ Probabilistic divide \& congruence: branching bisimilarity ⋮ Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On behavioural pseudometrics and closure ordinals
- Metrics for labelled Markov processes
- Probabilistic logical characterization
- Results on the propositional \(\mu\)-calculus
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- Non-expansive \(\varepsilon\)-bisimulations for probabilistic processes
- Bisimulation through probabilistic testing
- Chain-complete posets and directed sets with applications
- Characteristic formulae for processes with divergence
- A logic for reasoning about time and reliability
- Weak bisimulation metrics in models with nondeterminism and continuous state spaces
- SOS specifications for uniformly continuous operators
- Distribution-based bisimulation for labelled Markov processes
- A behavioural pseudometric for probabilistic transition systems
- Exploring probabilistic bisimulations. I
- Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
- Bisimulation for labelled Markov processes
- A general SOS theory for the specification of probabilistic transition systems
- A lattice-theoretical fixpoint theorem and its applications
- Converging from Branching to Linear Metrics on Markov Chains
- Characteristic formulae for fixed-point semantics: a general framework
- A General Framework for Probabilistic Characterizing Formulae
- Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics
- Taking It to the Limit: Approximate Reasoning for Markov Processes
- Probabilistic bisimulation as a congruence
- Compositional Metric Reasoning with Probabilistic Process Calculi
- Compositional bisimulation metric reasoning with Probabilistic Process Calculi
- Generalized Bisimulation Metrics
- Bisimulations for non-deterministic labelled Markov processes
- Game Refinement Relations and Metrics
- A modal characterization of observational congruence on finite terms of CCS
- Algebraic laws for nondeterminism and concurrency
- Formal verification of parallel programs
- Linear Distances between Markov Chains
- Modal Decomposition on Nondeterministic Probabilistic Processes
- Continuous Markovian Logics - Axiomatization and Quantified Metatheory
- Characterising Probabilistic Processes Logically
- Compositional weak metrics for group key update
- SOS specifications of probabilistic systems by uniformly continuous operators
- Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
- CONCUR 2003 - Concurrency Theory
- Foundations of Security Analysis and Design II
