Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Completeness Theorem for Probabilistic Regular Expressions

Wojciech Różowski, Alexandra Silva

TL;DR

This work introduces Probabilistic Regular Expressions (PRE) as a probabilistic analogue of Kleene regular expressions and develops a Salomaa-style axiomatisation for probabilistic language equivalence. It provides a small-step operational semantics via Antimirov derivatives that yield Generative Probabilistic Transition Systems (GPTS), and proves soundness and completeness of the axiomatisation using a coalgebraic framework and the rational fixpoint. The authors establish a Kleene-like theorem for PREs by connecting finite-state GPTS with PRE expressions through a generalized determinisation construction and a Brzozowski-style equation-solving method. The resulting theory gives a principled, abstract foundation for reasoning about probabilistic languages and lays groundwork for verification techniques for probabilistic programs and systems.

Abstract

We introduce Probabilistic Regular Expressions (PRE), a probabilistic analogue of regular expressions denoting probabilistic languages in which every word is assigned a probability of being generated. We present and prove the completeness of an inference system for reasoning about probabilistic language equivalence of PRE based on Salomaa's axiomatisation of Kleene Algebra.

A Completeness Theorem for Probabilistic Regular Expressions

TL;DR

This work introduces Probabilistic Regular Expressions (PRE) as a probabilistic analogue of Kleene regular expressions and develops a Salomaa-style axiomatisation for probabilistic language equivalence. It provides a small-step operational semantics via Antimirov derivatives that yield Generative Probabilistic Transition Systems (GPTS), and proves soundness and completeness of the axiomatisation using a coalgebraic framework and the rational fixpoint. The authors establish a Kleene-like theorem for PREs by connecting finite-state GPTS with PRE expressions through a generalized determinisation construction and a Brzozowski-style equation-solving method. The resulting theory gives a principled, abstract foundation for reasoning about probabilistic languages and lays groundwork for verification techniques for probabilistic programs and systems.

Abstract

We introduce Probabilistic Regular Expressions (PRE), a probabilistic analogue of regular expressions denoting probabilistic languages in which every word is assigned a probability of being generated. We present and prove the completeness of an inference system for reasoning about probabilistic language equivalence of PRE based on Salomaa's axiomatisation of Kleene Algebra.
Paper Structure (17 sections, 63 theorems, 58 equations, 1 figure)

This paper contains 17 sections, 63 theorems, 58 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Probabilistic Regular Expressions
  3. Operational Semantics of $\mathsf{PRE}$
  4. Roadmap to (Sound+Complete)ness
  5. (Co)algebras and Determinisations
  6. Soundness
  7. Completeness
  8. Discussion
  9. Antimirov derivatives are finite
  10. Positive convex algebras
  11. Syntax and axioms
  12. Soundness wrt bisimilarity
  13. Fundamental theorem
  14. Algebra structure
  15. Soundness of axioms for probabilistic language equivalence
  16. ...and 2 more sections

Key Result

lemma 1

For all $e \in \mathsf{Exp}$ it holds that $E(e)=\partial(e)(\checkmark)$.

Figures (1)

  • Figure 1: For $p \in [0,1]$, we write $\overline{p}=1-p$. The rules involving the division of probabilities are defined only when the denominator is non-zero. The function $E(-)$ provides a termination side condition to the Unique fixpoint axiom.

Theorems & Definitions (66)

  • lemma 1
  • lemma 2
  • theorem 1
  • lemma 3
  • lemma 4
  • lemma 5
  • theorem 2: Soundness
  • lemma 6
  • lemma 7
  • theorem 3: Milius:2018:Proper
  • ...and 56 more