Propositional Operators¶

API Reference¶

class masa.common.pctl.BoundedPCTLFormula[source]¶

Bases: object

Base class for bounded PCTL-style formulas.

MASA represents bounded PCTL formulas as a tree of BoundedPCTLFormula objects. A formula is evaluated on a Markov chain transition kernel (dense or compact) and a vectorized labeling matrix.

The formula API centers around two related operations:

sat(): evaluate the formula at its final time bound and return a per-state satisfaction indicator (a float array in {0.0, 1.0}).
_prob_seq(): compute a time-indexed sequence \(P_0(s), \dots, P_K(s)\) up to a specified horizon.

For propositional (state) formulas, the default _prob_seq() repeats the time-0 satisfaction vector across all time steps.

Vectorized labels

A LabelFn maps each state to a set of atomic predicates (strings). The model checker precomputes:

\[\mathrm{vec\_label\_fn} \in \{0,1\}^{|AP| \times |S|},\]

where vec_label_fn[i, s] = 1 iff atomic predicate AP[i] holds in state s.

Variables:: bound – Total time bound of the formula (including any nested subformula contributions).

Notes

Implementations of temporal operators typically use JAX (e.g. jit, vmap, lax.scan) to accelerate probability-sequence computation.

property _bound: int¶

Internal bound implementation.

Subclasses must implement this property.

Returns:: The non-negative time bound.
Raises:: NotImplementedError – If a subclass does not implement this property.

property bound: int¶: Total time bound of this formula (read-only).

_prob_seq(kernel: ndarray | Tuple[ndarray, ndarray], vec_label_fn: ndarray, atom_dict: Dict[str, int], max_k: int | None = None) → ndarray[source]¶

Compute a satisfaction/probability sequence up to horizon max_k.

The returned sequence has shape (max_k + 1, n_states) where row k corresponds to the value at time k.

For state formulas, the default implementation repeats sat() across time, i.e. \(P_k(s) = P_0(s)\).

Parameters:

kernel – Markov-chain kernel (dense (S,S) or compact (succ,p)).
vec_label_fn – Vectorized labeling matrix of shape (n_atoms, n_states).
atom_dict – Mapping from atomic predicate string to row index in vec_label_fn.
max_k – Sequence horizon (inclusive). If None, defaults to bound.

Returns:

A float64 array of shape (max_k + 1, n_states).

Notes

Temporal/probabilistic operators override this method.

sat(kernel: ndarray | Tuple[ndarray, ndarray], vec_label_fn: ndarray, atom_dict: Dict[str, int]) → ndarray[source]¶

Evaluate the formula at its bound for all states.

Parameters:

kernel – Markov-chain kernel (dense or compact).
vec_label_fn – Vectorized labeling matrix (n_atoms, n_states).
atom_dict – Mapping from atomic predicate string to row index.

Returns:

Float64 array of shape (n_states,) with values in {0.0, 1.0}.

class masa.common.pctl.Truth[source]¶

Bases: BoundedPCTLFormula

Boolean constant \(\top\) (true).

property _bound¶: Truth has zero temporal bound.

sat(kernel: ndarray | Tuple[ndarray, ndarray], vec_label_fn: ndarray, atom_dict: Dict[str, int]) → ndarray[source]¶

Return 1.0 for all states.

Parameters:

kernel – Transition kernel (used only to infer n_states).
vec_label_fn – Unused.
atom_dict – Unused.

Returns:

Float64 array of ones with shape (n_states,).

class masa.common.pctl.Atom(atom: str)[source]¶

Bases: BoundedPCTLFormula

Atomic proposition.

The atom name is resolved via atom_dict and selects the corresponding row in vec_label_fn.

Parameters:: atom – Name of the atomic predicate.
Variables:: atom – Atomic predicate name.

property _bound¶: Atoms have zero temporal bound.

sat(kernel: ndarray | Tuple[ndarray, ndarray], vec_label_fn: ndarray, atom_dict: Dict[str, int]) → ndarray[source]¶

Return the per-state truth values of this atomic predicate.

Parameters:

kernel – Unused (present for signature consistency).
vec_label_fn – Vectorized labeling matrix (n_atoms, n_states).
atom_dict – Mapping from atom string to row index.

Returns:

Float64 array of shape (n_states,) in {0.0, 1.0}.

class masa.common.pctl.Neg(subformula: BoundedPCTLFormula)[source]¶

Bases: BoundedPCTLFormula

Logical negation \(\neg \Phi\).

Parameters:: subformula – Subformula \(\Phi\).
Variables:: subformula – Nested formula \(\Phi\).

property _bound¶: Negation does not add temporal bound.

_prob_seq(kernel, vec_label_fn, atom_dict, max_k=None)[source]¶

Compute 1 - the subformula probability sequence.

Parameters:

kernel – Markov-chain kernel.
vec_label_fn – Vectorized labeling matrix.
atom_dict – Atom-to-row mapping.
max_k – Sequence horizon.

Returns:

Float64 array 1.0 - sub_seq with shape (max_k + 1, n_states).

sat(kernel: ndarray | Tuple[ndarray, ndarray], vec_label_fn: ndarray, atom_dict: Dict[str, int]) → ndarray[source]¶

Compute 1 - the subformula satisfaction indicator.

Parameters:

kernel – Markov-chain kernel.
vec_label_fn – Vectorized labeling matrix.
atom_dict – Atom-to-row mapping.

Returns:

Float64 array of shape (n_states,) in {0.0, 1.0}.

class masa.common.pctl.And(subformula_1: BoundedPCTLFormula, subformula_2: BoundedPCTLFormula)[source]¶

Bases: BoundedPCTLFormula

Logical conjunction \(\Phi_1 \land \Phi_2\).

MASA uses multiplication as conjunction for {0,1}-valued satisfaction arrays.

Parameters:

subformula_1 – Left operand \(\Phi_1\).
subformula_2 – Right operand \(\Phi_2\).

Variables:

subformula_1 – Left operand.
subformula_2 – Right operand.

property _bound¶: Bound is max(bound(subformula_1), bound(subformula_2)).

_prob_seq(kernel, vec_label_fn, atom_dict, max_k=None)[source]¶

Compute the elementwise product of operand sequences.

Parameters:

kernel – Markov-chain kernel.
vec_label_fn – Vectorized labeling matrix.
atom_dict – Atom-to-row mapping.
max_k – Sequence horizon.

Returns:

Float64 array of shape (max_k + 1, n_states).

sat(kernel: ndarray | Tuple[ndarray, ndarray], vec_label_fn: ndarray, atom_dict: Dict[str, int]) → ndarray[source]¶

Compute the conjunction per state.

Returns:: Float64 array of shape (n_states,) in {0.0, 1.0}.

class masa.common.pctl.Or(subformula_1: BoundedPCTLFormula, subformula_2: BoundedPCTLFormula)[source]¶

Bases: BoundedPCTLFormula

Logical disjunction \(\Phi_1 \lor \Phi_2\).

For {0,1} satisfaction arrays, MASA uses:

\[a \lor b \equiv 1 - (1-a)(1-b).\]

Parameters:

subformula_1 – Left operand \(\Phi_1\).
subformula_2 – Right operand \(\Phi_2\).

Variables:

subformula_1 – Left operand.
subformula_2 – Right operand.

property _bound¶: Bound is max(bound(subformula_1), bound(subformula_2)).

sat(kernel: ndarray | Tuple[ndarray, ndarray], vec_label_fn: ndarray, atom_dict: Dict[str, int]) → ndarray[source]¶

Compute the disjunction per state.

Returns:: Float64 array of shape (n_states,) in {0.0, 1.0}.

_prob_seq(kernel, vec_label_fn, atom_dict, max_k=None)[source]¶

Compute the disjunction sequence using 1 - (1-a)*(1-b).

Returns:: Float64 array of shape (max_k + 1, n_states).