Sound approximate and asymptotic probabilistic bisimulations for PCTL

DOI10.46298/LMCS-19(1:22)2023arXiv2111.03117MaRDI QIDQ6135748FDOQ6135748

Authors: Massimo Bartoletti, Maurizio Murgia 

Publication date: 26 August 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: We tackle the problem of establishing the soundness of approximate bisimilarity with respect to PCTL and its relaxed semantics. To this purpose, we consider a notion of bisimilarity inspired by the one introduced by Desharnais, Laviolette, and Tracol, and parametric with respect to an approximation error $delta$, and to the depth $n$ of the observation along traces. Essentially, our soundness theorem establishes that, when a state $q$ satisfies a given formula up-to error $delta$ and steps $n$, and $q$ is bisimilar to $q^{\prime }$ up-to error $delt{a}^{\prime }$ and enough steps, we prove that $q^{\prime }$ also satisfies the formula up-to a suitable error $$ and steps $n$. The new error $$ is computed from $delta$, $delt{a}^{\prime }$ and the formula, and only depends linearly on $n$. We provide a detailed overview of our soundness proof. We extend our bisimilarity notion to families of states, thus obtaining an asymptotic equivalence on such families. We then consider an asymptotic satisfaction relation for PCTL formulae, and prove that asymptotically equivalent families of states asymptotically satisfy the same formulae.

Full work available at URL: https://arxiv.org/abs/2111.03117

Recommendations

• Bisimulations meet PCTL equivalences for probabilistic automata
• Bisimulations meet PCTL equivalences for probabilistic automata
• Compositionality of approximate bisimulation for probabilistic systems
• Probabilistic bisimulations for PCTL model checking of interval MDPs
• Bisimulation and cocongruence for probabilistic systems
• scientific article; zbMATH DE number 1754605
• Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation
• Probabilistic bisimulation and simulation algorithms by abstract interpretation
• scientific article; zbMATH DE number 1759621
• On the relationship between bisimulation and trace equivalence in an approximate probabilistic context

zbMATH Keywords

probabilistic processesapproximate bisimulationPCTL

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Bisimulation for labelled Markov processes
• Title not available (Why is that?)
• Bisimulation through probabilistic testing
• Bounded linear logic: A modular approach to polynomial-time computability
• A logic for reasoning about time and reliability
• Metrics for labelled Markov processes
• Title not available (Why is that?)
• A behavioural pseudometric for probabilistic transition systems
• Automata, Languages and Programming
• Weak bisimulation is sound and complete for pCTL\(^*\)
• Game Refinement Relations and Metrics
• Title not available (Why is that?)
• Probabilistic logical characterization
• On the complexity of computing probabilistic bisimilarity
• Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems
• Weakening the perfect encryption assumption in Dolev-Yao adversaries
• Bisimulations meet PCTL equivalences for probabilistic automata
• Title not available (Why is that?)
• Łukasiewicz μ-calculus
• On the verification of qualitative properties of probabilistic processes under fairness constraints.
• Robust PCTL model checking
• The Complexity of Computing a Bisimilarity Pseudometric on Probabilistic Automata
• On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context
• Upper-Expectation Bisimilarity and Łukasiewicz μ-Calculus
• Computing Game Metrics on Markov Decision Processes
• Title not available (Why is that?)
• Title not available (Why is that?)
• On session types and polynomial time
• Computing Probabilistic Bisimilarity Distances via Policy Iteration
• Title not available (Why is that?)
• Deciding probabilistic bisimilarity distance one for labelled Markov chains
• Riesz Modal Logic with Threshold Operators
• Title not available (Why is that?)

This page was built for publication: Sound approximate and asymptotic probabilistic bisimulations for PCTL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135748)