agenticraft_foundation.verification.probabilistic

Probabilistic verification for Discrete-Time Markov Chains (DTMC).

Provides DTMC representation, reachability probability computation, steady-state distribution, and expected steps analysis. Based on Hansson & Jonsson (1994) and Baier & Katoen Ch. 10.

Probabilistic verification for Discrete-Time Markov Chains (DTMC).

This module provides: - DTMC representation with labeled states and probabilistic transitions - Reachability probability computation (linear system solving) - Steady-state distribution (power iteration) - Expected steps to reach target states - DTMC validation (probability sum = 1.0 per state)

Theory: Hansson & Jonsson (1994), PCTL model checking. Algorithms from Baier & Katoen, "Principles of Model Checking", Chapter 10.

Key insight for LLM agents: agents are inherently stochastic. The LTS/CSP framework handles non-determinism (what CAN happen), but DTMC handles probability (how LIKELY things are). This module bridges the gap.

Implementation: - numpy for linear system solving (Gaussian elimination / LU decomposition) - Value iteration fallback for larger systems

ProbabilisticTransition dataclass

A probabilistic transition: source ─p→ target.

ATTRIBUTE	DESCRIPTION
source	Source state ID. TYPE: int
target	Target state ID. TYPE: int
probability	Transition probability (0 < p <= 1). TYPE: float

DTMCState dataclass

A state in a DTMC.

ATTRIBUTE	DESCRIPTION
id	State identifier. TYPE: int
labels	Set of atomic propositions holding in this state. TYPE: set[str]

DTMC dataclass

Discrete-Time Markov Chain.

A DTMC is a tuple (S, P, ι, AP, L) where: - S: finite set of states - P: S × S → [0,1] transition probability matrix - ι: initial distribution (here: single initial state) - AP: set of atomic propositions - L: S → 2^AP labeling function

ATTRIBUTE	DESCRIPTION
states	Mapping from state IDs to DTMCState objects. TYPE: dict[int, DTMCState]
transitions	List of probabilistic transitions. TYPE: list[ProbabilisticTransition]
initial_state	ID of the initial state. TYPE: int

num_states property

Number of states.

num_transitions property

Number of transitions.

add_state(state_id, labels=None)

Add a state to the DTMC.

PARAMETER	DESCRIPTION
state_id	Unique state identifier. TYPE: int
labels	Set of atomic propositions for this state. TYPE: set[str] | None DEFAULT: None

RETURNS	DESCRIPTION
DTMCState	The created DTMCState.

add_transition(source, target, probability)

Add a probabilistic transition.

PARAMETER	DESCRIPTION
source	Source state ID. TYPE: int
target	Target state ID. TYPE: int
probability	Transition probability (must be in (0, 1]). TYPE: float

RETURNS	DESCRIPTION
ProbabilisticTransition	The created ProbabilisticTransition.

RAISES	DESCRIPTION
ValueError	If probability is not in (0, 1] or states don't exist.

get_transitions_from(state_id)

Get all transitions from a state.

PARAMETER	DESCRIPTION
state_id	The source state. TYPE: int

RETURNS	DESCRIPTION
list[ProbabilisticTransition]	List of transitions from the state.

get_transition_probability(source, target)

Get the probability of transitioning from source to target.

PARAMETER	DESCRIPTION
source	Source state ID. TYPE: int
target	Target state ID. TYPE: int

RETURNS	DESCRIPTION
float	Transition probability, or 0.0 if no transition exists.

successors(state_id)

Get successor states with their probabilities.

PARAMETER	DESCRIPTION
state_id	The source state. TYPE: int

RETURNS	DESCRIPTION
list[tuple[int, float]]	List of (target_state, probability) tuples.

states_with_label(label)

Get all states with a given label.

PARAMETER	DESCRIPTION
label	The atomic proposition to search for. TYPE: str

RETURNS	DESCRIPTION
set[int]	Set of state IDs with the given label.

states_with_labels(labels)

Get all states with any of the given labels.

PARAMETER	DESCRIPTION
labels	Set of atomic propositions. TYPE: set[str]

RETURNS	DESCRIPTION
set[int]	Set of state IDs with at least one of the given labels.

is_absorbing(state_id)

Check if a state is absorbing (self-loop with probability 1).

PARAMETER	DESCRIPTION
state_id	The state to check. TYPE: int

RETURNS	DESCRIPTION
bool	True if the state is absorbing.

validate()

Validate the DTMC.

Checks that: 1. All states have outgoing transitions 2. Outgoing probabilities sum to 1.0 for each state 3. All transition targets exist

RAISES	DESCRIPTION
ValueError	If the DTMC is malformed.

ProbabilisticResult dataclass

Result of a probabilistic verification query.

ATTRIBUTE	DESCRIPTION
probability	The probability for the initial state. TYPE: float
per_state	Probability for each state. TYPE: dict[int, float]
is_certain	True if probability is 1.0. TYPE: bool
is_impossible	True if probability is 0.0. TYPE: bool

is_certain property

True if probability is 1.0 (within tolerance).

is_impossible property

True if probability is 0.0 (within tolerance).

SteadyStateResult dataclass

Result of steady-state distribution computation.

ATTRIBUTE	DESCRIPTION
distribution	Mapping from state ID to steady-state probability. TYPE: dict[int, float]
converged	Whether the computation converged. TYPE: bool
iterations	Number of iterations used. TYPE: int

ExpectedStepsResult dataclass

Result of expected steps computation.

ATTRIBUTE	DESCRIPTION
expected	Expected number of steps from the initial state. TYPE: float
per_state	Expected steps from each state. TYPE: dict[int, float]
is_infinite	True if target is unreachable (infinite expected steps). TYPE: bool

is_infinite property

True if expected steps is infinite.

check_reachability(dtmc, target_labels=None, target_states=None)

Compute reachability probabilities for target states.

Computes Pr(◇ target) — the probability of eventually reaching a state with the given labels, from each state.

The algorithm: 1. Partition states into: - target states: prob = 1.0 - states that can't reach target: prob = 0.0 - remaining: solve linear system p(s) = Σ P(s,s') × p(s') 2. Solve via Gaussian elimination (small) or value iteration (large).

PARAMETER	DESCRIPTION
dtmc	The DTMC to analyze. TYPE: DTMC
target_labels	Labels identifying target states (at least one must match). TYPE: set[str] | None DEFAULT: None
target_states	Explicit set of target state IDs. If both are given, the union is used. TYPE: set[int] | None DEFAULT: None

RETURNS	DESCRIPTION
ProbabilisticResult	ProbabilisticResult with probabilities per state.

RAISES	DESCRIPTION
ValueError	If neither target_labels nor target_states is provided.

steady_state(dtmc, max_iterations=_MAX_ITERATIONS)

Compute the steady-state (stationary) distribution.

For ergodic chains, computes π such that π = πP. For absorbing chains, computes the absorption probabilities.

Uses power iteration: π_{k+1} = π_k × P.

PARAMETER	DESCRIPTION
dtmc	The DTMC. TYPE: DTMC
max_iterations	Maximum iterations for convergence. TYPE: int DEFAULT: _MAX_ITERATIONS

RETURNS	DESCRIPTION
SteadyStateResult	SteadyStateResult with distribution and convergence info.

expected_steps(dtmc, target_labels=None, target_states=None)

Compute expected number of steps to reach target states.

Solves: e(s) = 1 + Σ P(s,s') × e(s') for non-target states. Target states: e(s) = 0. States that can't reach target: e(s) = ∞.

PARAMETER	DESCRIPTION
dtmc	The DTMC. TYPE: DTMC
target_labels	Labels identifying target states. TYPE: set[str] | None DEFAULT: None
target_states	Explicit set of target state IDs. TYPE: set[int] | None DEFAULT: None

RETURNS	DESCRIPTION
ExpectedStepsResult	ExpectedStepsResult with expected steps per state.

RAISES	DESCRIPTION
ValueError	If neither target_labels nor target_states is provided.

build_dtmc_from_lts(lts_states, lts_transitions, initial_state=0)

Build a DTMC from explicit state/transition descriptions.

Convenience function for creating DTMCs from dictionaries.

PARAMETER	DESCRIPTION
lts_states	Mapping from state ID to label sets. TYPE: dict[int, set[str]]
lts_transitions	Mapping from state ID to list of (target, probability) tuples. TYPE: dict[int, list[tuple[int, float]]]
initial_state	The initial state ID. TYPE: int DEFAULT: 0

RETURNS	DESCRIPTION
DTMC	A validated DTMC.