agenticraft_foundation.verification.temporal

CTL (Computation Tree Logic) temporal model checking over LTS.

Provides a formula AST (Atomic, Not, And, Or, EX, EF, EG, EU, AX, AF, AG, AU) and bottom-up model checking via backward fixpoint computation. Based on Clarke & Emerson (1981) and Baier & Katoen Ch. 4 & 6.

CTL (Computation Tree Logic) temporal model checking.

This module provides: - CTL formula AST (Atomic, Not, And, Or, EX, EF, EG, EU, AX, AF, AG, AU) - Bottom-up model checking via backward fixpoint computation - Counterexample trace generation for failing properties

Theory: Clarke & Emerson (1981), Turing Award 2007. Algorithms from Baier & Katoen, "Principles of Model Checking", Chapters 4 (CTL) and 6 (fixpoint characterization).

CTL Semantics (over Kripke structures / LTS): - EX φ: there Exists a neXt state satisfying φ - AX φ: All neXt states satisfy φ - EF φ: there Exists a path where φ holds in some Future state - AF φ: on All paths, φ holds in some Future state - EG φ: there Exists a path where φ holds Globally - AG φ: on All paths, φ holds Globally - E[φ U ψ]: there Exists a path where φ holds Until ψ - A[φ U ψ]: on All paths, φ holds Until ψ

The model checking algorithm evaluates formulas bottom-up: - Base case: Atomic propositions evaluated via labeling function - Boolean: set operations (complement, intersection, union) - EX: backward one-step (predecessors) - EF: least fixpoint via BFS backward from sat(φ) - EG: greatest fixpoint via iterative removal - EU: least fixpoint combining sat(ψ) and EX - Universal quantifiers (AX, AF, AG, AU): defined as duals of existential

Labeling = dict[int, set[str]] module-attribute

Mapping from state IDs to sets of atomic proposition names.

CTLFormula

Bases: ABC

Abstract base class for CTL formulas.

Atomic dataclass

Bases: CTLFormula

Atomic proposition: holds in states labeled with the given proposition.

ATTRIBUTE	DESCRIPTION
prop	The name of the atomic proposition. TYPE: str

Not dataclass

Bases: CTLFormula

Negation: ¬φ.

ATTRIBUTE	DESCRIPTION
formula	The formula to negate. TYPE: CTLFormula

And dataclass

Bases: CTLFormula

Conjunction: φ ∧ ψ.

ATTRIBUTE	DESCRIPTION
left	Left conjunct. TYPE: CTLFormula
right	Right conjunct. TYPE: CTLFormula

Or dataclass

Bases: CTLFormula

Disjunction: φ ∨ ψ.

ATTRIBUTE	DESCRIPTION
left	Left disjunct. TYPE: CTLFormula
right	Right disjunct. TYPE: CTLFormula

Implies dataclass

Bases: CTLFormula

Implication: φ → ψ (syntactic sugar for ¬φ ∨ ψ).

ATTRIBUTE	DESCRIPTION
left	Antecedent. TYPE: CTLFormula
right	Consequent. TYPE: CTLFormula

EX dataclass

Bases: CTLFormula

EX φ: there exists a next state satisfying φ.

ATTRIBUTE	DESCRIPTION
formula	The formula that must hold in some successor. TYPE: CTLFormula

EF dataclass

Bases: CTLFormula

EF φ: there exists a path where φ eventually holds.

Equivalent to E[True U φ].

ATTRIBUTE	DESCRIPTION
formula	The formula that must eventually hold. TYPE: CTLFormula

EG dataclass

Bases: CTLFormula

EG φ: there exists a path where φ holds globally.

ATTRIBUTE	DESCRIPTION
formula	The formula that must hold on all states of some path. TYPE: CTLFormula

EU dataclass

Bases: CTLFormula

E[φ U ψ]: there exists a path where φ holds until ψ holds.

ATTRIBUTE	DESCRIPTION
left	The formula that must hold until right holds. TYPE: CTLFormula
right	The formula that must eventually hold. TYPE: CTLFormula

AX dataclass

Bases: CTLFormula

AX φ: all next states satisfy φ.

Equivalent to ¬EX(¬φ).

ATTRIBUTE	DESCRIPTION
formula	The formula that must hold in all successors. TYPE: CTLFormula

AF dataclass

Bases: CTLFormula

AF φ: on all paths, φ eventually holds.

Equivalent to ¬EG(¬φ) by path-quantifier duality: AF φ holds iff there is no path on which ¬φ holds globally. Reference: Baier & Katoen (2008), Theorem 6.23.

ATTRIBUTE	DESCRIPTION
formula	The formula that must eventually hold on all paths. TYPE: CTLFormula

AG dataclass

Bases: CTLFormula

AG φ: on all paths, φ holds globally.

Equivalent to ¬EF(¬φ).

ATTRIBUTE	DESCRIPTION
formula	The formula that must hold on all paths globally. TYPE: CTLFormula

AU dataclass

Bases: CTLFormula

A[φ U ψ]: on all paths, φ holds until ψ holds.

ATTRIBUTE	DESCRIPTION
left	The formula that must hold until right holds. TYPE: CTLFormula
right	The formula that must eventually hold. TYPE: CTLFormula

ModelCheckResult dataclass

Result of CTL model checking.

ATTRIBUTE	DESCRIPTION
satisfied	Whether the formula holds in the initial state. TYPE: bool
satisfying_states	Set of states where the formula holds. TYPE: set[int]
counterexample	A trace to a violating state (if not satisfied), found via BFS from the initial state. TYPE: Trace | None
formula	The formula that was checked. TYPE: CTLFormula | None

model_check(system, formula, labeling, max_counterexample_length=100)

Check whether a CTL formula holds in the initial state of a system.

Performs bottom-up evaluation of the formula over the LTS state space.

PARAMETER	DESCRIPTION
system	The system to check (CSP process or LTS). TYPE: Process | LTS
formula	The CTL formula to verify. TYPE: CTLFormula
labeling	Mapping from state IDs to sets of atomic propositions. TYPE: Labeling
max_counterexample_length	Maximum length for counterexample traces. TYPE: int DEFAULT: 100

RETURNS	DESCRIPTION
ModelCheckResult	ModelCheckResult with satisfaction status, satisfying states,
ModelCheckResult	and counterexample trace if the property fails.

Example

labeling = {0: {"init"}, 1: {"processing"}, 2: {"done"}} result = model_check(lts, AG(Not(Atomic("error"))), labeling) result.satisfied True

check_safety(system, bad_prop, labeling)

Check a safety property: AG(¬bad_prop).

Convenience function for the common pattern of verifying that a "bad" state is never reached.

PARAMETER	DESCRIPTION
system	The system to check. TYPE: Process | LTS
bad_prop	Atomic proposition labeling "bad" states. TYPE: str
labeling	State labeling function. TYPE: Labeling

RETURNS	DESCRIPTION
ModelCheckResult	ModelCheckResult — satisfied means the bad state is unreachable.

check_liveness(system, good_prop, labeling)

Check a liveness property: AF(good_prop).

Convenience function for verifying that a "good" state is eventually reached on all paths.

PARAMETER	DESCRIPTION
system	The system to check. TYPE: Process | LTS
good_prop	Atomic proposition labeling "good" states. TYPE: str
labeling	State labeling function. TYPE: Labeling

RETURNS	DESCRIPTION
ModelCheckResult	ModelCheckResult — satisfied means the good state is always eventually reached.

check_invariant(system, invariant_prop, labeling)

Check an invariant property: AG(invariant_prop).

Convenience function for verifying that a property holds in all reachable states.

PARAMETER	DESCRIPTION
system	The system to check. TYPE: Process | LTS
invariant_prop	Atomic proposition that should hold everywhere. TYPE: str
labeling	State labeling function. TYPE: Labeling

RETURNS	DESCRIPTION
ModelCheckResult	ModelCheckResult — satisfied means the invariant holds globally.