Probabilistic Computation Tree Logic (PCTL) Constraint

Overview

Probabilistic CTL (PCTL) style constraint monitor (simplified).

The current implementation mirrors the safety-style structure used elsewhere: it accumulates unsafe occurrences based on a per-step cost function applied to labels. While named “PCTL”, this monitor presently behaves like a boolean “safety so far” tracker under the local convention cost >= 0.5.

Conceptually, a PCTL-style safety constraint might aim to bound the probability of reaching unsafe states, e.g.:

\[\Pr(\Diamond\,\mathsf{unsafe}) \le \alpha,\]

but note that this file’s current implementation does not compute an explicit probability estimate; it tracks whether any unsafe event occurred.

API Reference

class masa.common.constraints.pctl.PCTL(cost_fn: Callable[[Iterable[str]], float], alpha: float)

Bases: Constraint

Simplified PCTL-named monitor tracking whether any unsafe step occurred.

Parameters:

• cost_fn – Mapping from label sets to scalar cost.

• alpha – Threshold parameter stored for downstream use (not currently used in the logic in this file).

Variables:

• cost_fn – Cost function labels -> float.

• alpha – User-specified parameter (reserved for probabilistic variants).

• safe – True until an unsafe cost is observed.

• step_cost – Most recent cost value.

• total_unsafe – Count of unsafe steps (as floats).

reset()

Reset episode counters.

update(labels: Iterable[str])

Update safety flags from the current label set.

Parameters:

labels – Iterable of atomic propositions.

satisfied() → bool

Whether the episode remains safe so far.

episode_metric() → Dict[str, float]

End-of-episode metrics.

Returns:

• "cum_unsafe": count of unsafe steps,

• "satisfied": 1.0 if safe else 0.0.

Return type:

Dict containing

step_metric() → Dict[str, float]

Per-step metrics.

Returns:

• "cost": current step cost,

• "violation": 1.0 if cost >= 0.5 else 0.0.

Return type:

Dict containing

property constraint_type: str

"pctl".

Type:

Stable identifier string

class masa.common.constraints.pctl.PCTLEnv(env: gym.Env, cost_fn: CostFn = dummy_cost_fn, alpha: float = 0.01, **kw)

Bases: BaseConstraintEnv

Gymnasium wrapper for the PCTL monitor.

Parameters:

• env – Base environment (must be a LabelledEnv).

• cost_fn – Cost function mapping labels to a scalar.

• alpha – Threshold parameter stored on the monitor (see PCTL).

• **kw – Extra keyword arguments forwarded to BaseConstraintEnv.

Initialize the wrapper.

Parameters:

• env – Base environment. Must already be wrapped as a LabelledEnv so that step/reset provide label sets in info["labels"].

• constraint – A constraint monitor implementing Constraint.

• **kw – Unused extra keyword arguments (kept for wrapper compatibility).

Raises:

TypeError – If env is not a LabelledEnv.