Propositional Operators¶

API Reference¶

masa.common.pctl ¶

BoundedPCTLFormula ¶

BoundedPCTLFormula()

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. $$

Attributes:

Name	Type	Description
`bound`	`int`	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.

Source code in masa/common/pctl.py

def __init__(self) -> None:
    pass

bound `property` ¶

bound: int

Total time bound of this formula (read-only).

sat ¶

sat(kernel: Kernel, vec_label_fn: ndarray, atom_dict: Dict[str, int]) -> np.ndarray

Evaluate the formula at its bound for all states.

Parameters:

Name	Type	Description	Default
`kernel`	`Kernel`	Markov-chain kernel (dense or compact).	required
`vec_label_fn`	`ndarray`	Vectorized labeling matrix `(n_atoms, n_states)`.	required
`atom_dict`	`Dict[str, int]`	Mapping from atomic predicate string to row index.	required

Returns:

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

Source code in masa/common/pctl.py

def sat(
    self,
    kernel: Kernel,
    vec_label_fn: np.ndarray,
    atom_dict: Dict[str, int],
) -> np.ndarray:
    r"""Evaluate the formula at its bound for all states.

    Args:
        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}``.
    """
    return self._prob_seq(kernel, vec_label_fn, atom_dict, max_k=self.bound)[
        self.bound
    ]

Truth ¶

Truth()

Bases: BoundedPCTLFormula

Boolean constant $\top$ (true).

Source code in masa/common/pctl.py

def __init__(self) -> None:
    pass

sat ¶

sat(kernel: Kernel, vec_label_fn: ndarray, atom_dict: Dict[str, int]) -> np.ndarray

Return 1.0 for all states.

Parameters:

Name	Type	Description	Default
`kernel`	`Kernel`	Transition kernel (used only to infer `n_states`).	required
`vec_label_fn`	`ndarray`	Unused.	required
`atom_dict`	`Dict[str, int]`	Unused.	required

Returns:

Type	Description
`ndarray`	Float64 array of ones with shape `(n_states,)`.

Source code in masa/common/pctl.py

def sat(
    self,
    kernel: Kernel,
    vec_label_fn: np.ndarray,
    atom_dict: Dict[str, int],
) -> np.ndarray:
    """Return ``1.0`` for all states.

    Args:
        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,)``.
    """
    n_states = kernel_n_states(kernel)
    return np.ones(n_states, dtype=np.float64)

Atom ¶

Atom(atom: str)

Bases: BoundedPCTLFormula

Atomic proposition.

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

Parameters:

Name	Type	Description	Default
`atom`	`str`	Name of the atomic predicate.	required

Attributes:

Name	Type	Description
`atom`		Atomic predicate name.

Source code in masa/common/pctl.py

def __init__(self, atom: str):
    super().__init__()
    self.atom = atom

sat ¶

sat(kernel: Kernel, vec_label_fn: ndarray, atom_dict: Dict[str, int]) -> np.ndarray

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

Parameters:

Name	Type	Description	Default
`kernel`	`Kernel`	Unused (present for signature consistency).	required
`vec_label_fn`	`ndarray`	Vectorized labeling matrix `(n_atoms, n_states)`.	required
`atom_dict`	`Dict[str, int]`	Mapping from atom string to row index.	required

Returns:

Type	Description
`ndarray`	Float64 array of shape `(n_states,)` in `{0.0, 1.0}`.

Source code in masa/common/pctl.py

def sat(
    self,
    kernel: Kernel,
    vec_label_fn: np.ndarray,
    atom_dict: Dict[str, int],
) -> np.ndarray:
    """Return the per-state truth values of this atomic predicate.

    Args:
        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}``.
    """
    return vec_label_fn[atom_dict[self.atom]]

Neg ¶

Neg(subformula: BoundedPCTLFormula)

Bases: BoundedPCTLFormula

Logical negation $\neg \Phi$.

Parameters:

Name	Type	Description	Default
`subformula`	`BoundedPCTLFormula`	Subformula $\Phi$.	required

Attributes:

Name	Type	Description
`subformula`		Nested formula $\Phi$.

Source code in masa/common/pctl.py

def __init__(self, subformula: BoundedPCTLFormula):
    super().__init__()
    self.subformula = subformula

sat ¶

sat(kernel: Kernel, vec_label_fn: ndarray, atom_dict: Dict[str, int]) -> np.ndarray

Compute 1 - the subformula satisfaction indicator.

Parameters:

Name	Type	Description	Default
`kernel`	`Kernel`	Markov-chain kernel.	required
`vec_label_fn`	`ndarray`	Vectorized labeling matrix.	required
`atom_dict`	`Dict[str, int]`	Atom-to-row mapping.	required

Returns:

Type	Description
`ndarray`	Float64 array of shape `(n_states,)` in `{0.0, 1.0}`.

Source code in masa/common/pctl.py

def sat(
    self,
    kernel: Kernel,
    vec_label_fn: np.ndarray,
    atom_dict: Dict[str, int],
) -> np.ndarray:
    """Compute ``1 -`` the subformula satisfaction indicator.

    Args:
        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}``.
    """
    return 1.0 - self.subformula.sat(kernel, vec_label_fn, atom_dict)

And ¶

And(subformula_1: BoundedPCTLFormula, subformula_2: BoundedPCTLFormula)

Bases: BoundedPCTLFormula

Logical conjunction $\Phi_1 \land \Phi_2$.

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

Parameters:

Name	Type	Description	Default
`subformula_1`	`BoundedPCTLFormula`	Left operand $\Phi_1$.	required
`subformula_2`	`BoundedPCTLFormula`	Right operand $\Phi_2$.	required

Attributes:

Name	Type	Description
`subformula_1`		Left operand.
`subformula_2`		Right operand.

Source code in masa/common/pctl.py

def __init__(self, subformula_1: BoundedPCTLFormula, subformula_2: BoundedPCTLFormula):
    super().__init__()
    self.subformula_1 = subformula_1
    self.subformula_2 = subformula_2

sat ¶

sat(kernel: Kernel, vec_label_fn: ndarray, atom_dict: Dict[str, int]) -> np.ndarray

Compute the conjunction per state.

Returns:

Type	Description
`ndarray`	Float64 array of shape `(n_states,)` in `{0.0, 1.0}`.

Source code in masa/common/pctl.py

def sat(
    self,
    kernel: Kernel,
    vec_label_fn: np.ndarray,
    atom_dict: Dict[str, int],
) -> np.ndarray:
    """Compute the conjunction per state.

    Returns:
        Float64 array of shape ``(n_states,)`` in ``{0.0, 1.0}``.
    """
    return (
        self.subformula_1.sat(kernel, vec_label_fn, atom_dict)
        * self.subformula_2.sat(kernel, vec_label_fn, atom_dict)
    )

Or ¶

Or(subformula_1: BoundedPCTLFormula, subformula_2: BoundedPCTLFormula)

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:

Name	Type	Description	Default
`subformula_1`	`BoundedPCTLFormula`	Left operand $\Phi_1$.	required
`subformula_2`	`BoundedPCTLFormula`	Right operand $\Phi_2$.	required

Attributes:

Name	Type	Description
`subformula_1`		Left operand.
`subformula_2`		Right operand.

Source code in masa/common/pctl.py

def __init__(self, subformula_1: BoundedPCTLFormula, subformula_2: BoundedPCTLFormula):
    super().__init__()
    self.subformula_1 = subformula_1
    self.subformula_2 = subformula_2

sat ¶

sat(kernel: Kernel, vec_label_fn: ndarray, atom_dict: Dict[str, int]) -> np.ndarray

Compute the disjunction per state.

Returns:

Type	Description
`ndarray`	Float64 array of shape `(n_states,)` in `{0.0, 1.0}`.

Source code in masa/common/pctl.py

def sat(
    self,
    kernel: Kernel,
    vec_label_fn: np.ndarray,
    atom_dict: Dict[str, int],
) -> np.ndarray:
    """Compute the disjunction per state.

    Returns:
        Float64 array of shape ``(n_states,)`` in ``{0.0, 1.0}``.
    """
    return Neg(And(Neg(self.subformula_1), Neg(self.subformula_2))).sat(
        kernel, vec_label_fn, atom_dict
    )

Name	Type	Description	Default
`subformula_1`	`BoundedPCTLFormula`	Left operand \(\Phi_1\).	required
`subformula_2`	`BoundedPCTLFormula`	Right operand \(\Phi_2\).	required

Propositional Operators¶

API Reference¶

masa.common.pctl ¶

BoundedPCTLFormula ¶

bound property ¶

sat ¶

Truth ¶

sat ¶

Atom ¶

sat ¶

Neg ¶

sat ¶

And ¶

sat ¶

Or ¶

sat ¶

bound `property` ¶