Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Robust Probabilistic Temporal Logics

Martin Zimmermann

TL;DR

This work extends Tabuada and Neider's robust semantics to probabilistic temporal logics by introducing rPCTL and rPCTL*, which adopt a five‑valued truth framework $\mathbb{B}_4$ while preserving the original syntax and DTMC semantics. The authors show that robustness can be incorporated without increasing model‑checking complexity: rPCTL remains in $\mathsf{P}$ and rPCTL* remains in $\mathsf{PSPACE}$, with translations and automata‑based methods adapting existing PCTL/PCTL* techniques. They establish expressiveness relationships, proving that rPCTL is at least as expressive as PCTL and that rPCTL* has the same expressiveness as PCTL*, via polynomial translations. These results provide a principled, scalable way to specify and verify robust probabilistic properties, such as “99% of executions,” under environment‑assumption violations, while maintaining tractable verification. The work positions probabilistic robustness as a practical enhancement rather than a costlier computational overhead, broadening the applicability of robust specifications in probabilistic systems.

Abstract

We robustify PCTL and PCTL*, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of their model-checking problems.

Robust Probabilistic Temporal Logics

TL;DR

This work extends Tabuada and Neider's robust semantics to probabilistic temporal logics by introducing rPCTL and rPCTL*, which adopt a five‑valued truth framework while preserving the original syntax and DTMC semantics. The authors show that robustness can be incorporated without increasing model‑checking complexity: rPCTL remains in and rPCTL* remains in , with translations and automata‑based methods adapting existing PCTL/PCTL* techniques. They establish expressiveness relationships, proving that rPCTL is at least as expressive as PCTL and that rPCTL* has the same expressiveness as PCTL*, via polynomial translations. These results provide a principled, scalable way to specify and verify robust probabilistic properties, such as “99% of executions,” under environment‑assumption violations, while maintaining tractable verification. The work positions probabilistic robustness as a practical enhancement rather than a costlier computational overhead, broadening the applicability of robust specifications in probabilistic systems.

Abstract

We robustify PCTL and PCTL*, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of their model-checking problems.
Paper Structure (11 sections, 5 theorems, 7 equations, 1 figure)

This paper contains 11 sections, 5 theorems, 7 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Robust PCTL
  4. Expressiveness
  5. Model-checking
  6. Robust PCTL$^*$
  7. Expressiveness
  8. Model-checking
  9. Related Work
  10. Conclusion
  11. Acknowledgements

Key Result

Lemma 1

Let $\varphi$ be a PCTL formula without implications, and let $\mathcal{M}$ be a DTMC with initial state $s_I$. Then, $\mathcal{M},s_I \models \varphi$ iff $V_\mathcal{M}(s_I, \dot{\varphi}) = 1111$, where $\dot{\varphi}$ is the rPCTL formula obtained from $\varphi$ by dotting all temporal operators

Figures (1)

  • Figure 1: The unambiguous Büchi automata for the path properties used in the rPCTL model-checking algorithm. Transitions are labeled by sets of states that represent all states in them (recall that $S$ is the set of all states while $S'$ and $S"$ are subsets of $S$). $\overline{S'}$ denotes the complement of $S'$ w.r.t. $S$.

Theorems & Definitions (11)

  • Example 1
  • Lemma 1
  • proof
  • Corollary 1
  • Theorem 1
  • proof
  • Example 2
  • Theorem 2
  • proof
  • Theorem 3
  • ...and 1 more