Propositional Formula

Overview

Lightweight propositional (LTL-style) formula objects and a deterministic finite automaton (DFA) whose transitions are guarded by those formulae.

Core ideas:

• A label is an iterable of atomic proposition names (strings).

• A Formula implements a satisfaction predicate Formula.sat().

• A DFA transition from \(q\) to \(q'\) is enabled when the edge guard formula is satisfied by the current label set.

• DFACostFn wraps a DFA as a MASA CostFn where the cost is 1.0 upon reaching accepting states (after stepping) and 0.0 otherwise.

This module is intentionally minimal: it does not implement full LTL temporal operators (X, U, F, G). Instead, it provides propositional guards for DFA edges, which is sufficient for DFA-based monitoring and safety cost construction.

API Reference

class masa.common.ltl.Formula

Bases: object

Base class for propositional formulae over atomic proposition labels.

A formula is evaluated against a label set (an iterable of strings), and returns whether the formula is satisfied.

Subclasses must implement sat(), which defines the satisfaction relation between the formula and a set of labels.

Notes

The operators provided here are propositional (Boolean) connectives only. Temporal structure is represented externally via a DFA that consumes a trace of label sets.

sat(labels: Iterable[str]) → bool

Checks whether the formula is satisfied by the given labels.

Parameters:

labels – Iterable of atomic proposition names that hold at the current step.

Returns:

True if the formula is satisfied under the given labels.

Raises:

NotImplementedError – If the subclass does not implement the satisfaction relation.

class masa.common.ltl.Atom(atom: str)

Bases: Formula

Atomic proposition.

An Atom is satisfied iff the stored atomic proposition name appears in the given label set.

Variables:

atom – The atomic proposition name.

sat(labels: Iterable[str]) → bool

Evaluates whether the atom is present in labels.

Parameters:

labels – Iterable of atomic proposition names.

Returns:

True iff atom is in labels.

class masa.common.ltl.Truth

Bases: Formula

Constant truth.

Always satisfied, regardless of the labels.

sat(labels: Iterable[str]) → bool

Evaluates the truth constant.

Parameters:

labels – Unused. Included for API consistency.

Returns:

True.

class masa.common.ltl.And(subformula_1: Formula, subformula_2: Formula)

Bases: Formula

Conjunction of two subformulae.

Satisfied iff both subformulae are satisfied.

Variables:

• subformula_1 – Left operand.

• subformula_2 – Right operand.

sat(labels: Iterable[str]) → bool

Evaluates conjunction satisfaction.

Parameters:

labels – Iterable of atomic proposition names.

Returns:

True iff both subformula_1 and subformula_2 are satisfied by labels.

class masa.common.ltl.Or(subformula_1: Formula, subformula_2: Formula)

Bases: Formula

Disjunction of two subformulae.

Satisfied iff at least one subformula is satisfied.

Variables:

• subformula_1 – Left operand.

• subformula_2 – Right operand.

sat(labels: Iterable[str]) → bool

Evaluates disjunction satisfaction.

Parameters:

labels – Iterable of atomic proposition names.

Returns:

True iff either subformula_1 or subformula_2 is satisfied by labels.

class masa.common.ltl.Neg(subformula: Formula)

Bases: Formula

Negation of a subformula.

Satisfied iff the subformula is not satisfied.

Variables:

subformula – The formula being negated.

sat(labels: Iterable[str]) → bool

Evaluates negation satisfaction.

Parameters:

labels – Iterable of atomic proposition names.

Returns:

True iff subformula is not satisfied by labels.

class masa.common.ltl.Implies(subformula_1: Formula, subformula_2: Formula)

Bases: Formula

Implication between two subformulae.

Implies(a, b) is satisfied iff either a is false or b is true under the given labels, i.e. it is equivalent to:

\[\neg a \lor b\]

Variables:

• subformula_1 – Antecedent (premise).

• subformula_2 – Consequent (conclusion).

sat(labels: Iterable[str]) → bool

Evaluates implication satisfaction.

Parameters:

labels – Iterable of atomic proposition names.

Returns:

True iff the implication holds under labels.