Temporal Operators

API Reference

class masa.common.pctl.Next(prob: float, subformula: BoundedPCTLFormula)[source]

Bases: BoundedPCTLFormula

Bounded PCTL next operator \(X\) with probability threshold.

This represents:

\[\mathbb{P}_{\ge p}[X\,\Phi].\]

Informally, the formula holds at state \(s\) iff the probability that \(\Phi\) holds in the next state is at least \(p\).

Parameters:

  • prob – Probability threshold \(p \in [0,1]\).

  • subformula – The subformula \(\Phi\) evaluated at the next state.

Variables:

  • prob – Probability threshold \(p\).

  • subformula – Nested formula \(\Phi\).

  • bound_param – Local bound contributed by this operator (fixed to 1).

See also

_prob_seq(): Computes the shifted probability sequence for \(X\,\Phi\).

property _bound

Total bound for Next.

Returns:

1 + subformula.bound.

static _next_prob_seq_core_dense(m: Array, sub_seq: Array) → Array[source]

JAX core for Next on a dense kernel.

Parameters:

  • m – Dense Markov-chain transition matrix of shape (S, S), where column s is the distribution over next states from state s.

  • sub_seq – Subformula sequence of shape (T, S).

Returns:

Sequence of shape (T + 1, S). Row 0 is all zeros (the shifted operator is defined to have probability 0 at time 0), and rows 1..T contain one-step expectations of sub_seq.

static _next_prob_seq_core_compact(succ: Array, p: Array, sub_seq: Array, K: int) → Array[source]

JAX core for Next on a compact kernel.

Parameters:

  • succ – Successor ids of shape (K, S).

  • p – Successor probabilities of shape (K, S) aligned with succ.

  • sub_seq – Subformula sequence of shape (T, S).

  • K – Max successors per state (static argument for JIT).

Returns:

Sequence of shape (T + 1, S) with row 0 all zeros.

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

Compute the probability sequence for \(X\,\Phi\).

Parameters:

  • kernel – Markov-chain kernel (dense or compact).

  • vec_label_fn – Vectorized labeling matrix (n_atoms, S).

  • atom_dict – Mapping from atom string to row index.

  • max_k – Local horizon (inclusive). If None, defaults to 1.

Returns:

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

Notes

If max_k == 0, returns a single row of zeros.

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

Threshold the one-step probability for \(\mathbb{P}_{\ge p}[X\,\Phi]\).

Parameters:

  • kernel – Markov-chain kernel (dense or compact).

  • vec_label_fn – Vectorized labeling matrix (n_atoms, S).

  • atom_dict – Mapping from atom string to row index.

Returns:

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

class masa.common.pctl.Until(prob: float, bound, subformula_1: BoundedPCTLFormula, subformula_2: BoundedPCTLFormula)[source]

Bases: BoundedPCTLFormula

Bounded PCTL until operator \(U^{\le B}\) with probability threshold.

This represents:

\[\mathbb{P}_{\ge p}[\Phi_1\ U^{\le B}\ \Phi_2].\]

Informally, the formula holds at state \(s\) iff the probability that \(\Phi_2\) becomes true within \(B\) steps while \(\Phi_1\) holds at all preceding steps is at least \(p\).

The bounded-until recurrence computed by _prob_seq() is:

\[\begin{split}P_0 &= \mathrm{sat}_2, \\\\ P_{k+1} &= \mathrm{sat}_2 + \bigl((1-\mathrm{sat}_2)\,\mathrm{sat}_1\bigr)\, \mathbb{E}[P_k(s')].\end{split}\]
Parameters:

  • prob – Probability threshold \(p \in [0,1]\).

  • bound – Local bound \(B\).

  • subformula_1 – Continuation condition \(\Phi_1\).

  • subformula_2 – Target condition \(\Phi_2\).

Variables:

  • prob – Probability threshold.

  • bound_param – Local bound \(B\).

  • subformula_1 – Continuation formula.

  • subformula_2 – Target formula.

property _bound

Total bound for Until.

Returns:

bound_param + subformula_1.bound + subformula_2.bound.

static _until_prob_seq_core_dense(m: Array, sat1: Array, sat2: Array, max_k: int) → Array[source]

JAX core for bounded-until probabilities using a dense kernel.

Parameters:

  • m – Dense Markov-chain transition matrix of shape (S, S).

  • sat1 – Satisfaction mask for \(\Phi_1\), shape (S,) in {0,1}.

  • sat2 – Satisfaction mask for \(\Phi_2\), shape (S,) in {0,1}.

  • max_k – Local bound \(B\).

Returns:

Float64 JAX array of shape (max_k + 1, S).

static _until_prob_seq_core_compact(succ: Array, p: Array, sat1: Array, sat2: Array, max_k: int, K: int) → Array[source]

JAX core for bounded-until probabilities using a compact kernel.

Parameters:

  • succ – Successor ids (K, S).

  • p – Successor probabilities (K, S).

  • sat1 – Satisfaction mask for \(\Phi_1\), shape (S,) in {0,1}.

  • sat2 – Satisfaction mask for \(\Phi_2\), shape (S,) in {0,1}.

  • max_k – Local bound \(B\).

  • K – Max successors per state (static argument for JIT).

Returns:

Float64 JAX array of shape (max_k + 1, S).

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

Compute the bounded-until probability sequence.

Parameters:

  • kernel – Markov-chain kernel (dense or compact).

  • vec_label_fn – Vectorized labeling matrix (n_atoms, S).

  • atom_dict – Mapping from atom string to row index.

  • max_k – Local horizon (inclusive). If None, defaults to bound_param.

Returns:

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

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

Threshold \(\mathbb{P}_{\ge p}[\Phi_1\ U^{\le B}\ \Phi_2]\).

Parameters:

  • kernel – Markov-chain kernel (dense or compact).

  • vec_label_fn – Vectorized labeling matrix (n_atoms, S).

  • atom_dict – Mapping from atom string to row index.

Returns:

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

class masa.common.pctl.Always(prob: float, bound: int, subformula: BoundedPCTLFormula)[source]

Bases: BoundedPCTLFormula

Bounded PCTL always operator \(G^{\le B}\) with probability threshold.

This represents:

\[\mathbb{P}_{\ge p}[G^{\le B}\,\Phi].\]

MASA implements bounded always via duality:

\[G^{\le B}\Phi \equiv \neg(\top\ U^{\le B}\ \neg\Phi),\]

with the threshold transformation \(p \mapsto 1-p\) applied to the inner until.

Parameters:

  • prob – Probability threshold \(p \in [0,1]\).

  • bound – Local bound \(B\).

  • subformula – Subformula \(\Phi\).

Variables:

  • prob – Probability threshold.

  • bound_param – Local bound.

  • subformula – Nested formula.

  • _inner – Desugared formula (internal) built from Neg, Until, and Truth.

property _bound: int

Total bound delegated to the desugared inner formula.

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

Delegate probability-sequence computation to _inner.

sat(kernel, vec_label_fn, atom_dict)[source]

Delegate probability-sequence computation to _inner.

class masa.common.pctl.Eventually(prob: float, bound: int, subformula: BoundedPCTLFormula)[source]

Bases: BoundedPCTLFormula

Bounded PCTL eventually operator \(F^{\le B}\) with probability threshold.

This represents:

\[\mathbb{P}_{\ge p}[F^{\le B}\,\Phi].\]

MASA implements bounded eventually as a bounded until:

\[F^{\le B}\Phi \equiv \top\ U^{\le B}\ \Phi.\]
Parameters:

  • prob – Probability threshold \(p \in [0,1]\).

  • bound – Local bound \(B\).

  • subformula – Subformula \(\Phi\).

Variables:

  • prob – Probability threshold.

  • bound_param – Local bound.

  • subformula – Nested formula.

  • _inner – Desugared formula (internal) built from Until and Truth.

property _bound: int

Total bound delegated to the desugared inner formula.

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

Delegate probability-sequence computation to _inner.

sat(kernel, vec_label_fn, atom_dict)[source]

Delegate satisfaction evaluation to _inner.