Add Support for Interval Signal Temporal Logic (I-STL) and PAC-Bounded Signal Temporal Logic (pacSTL)

[petdalh]

As a part of my Master's thesis I have been using the PAC-Bounded Signal Temporal Logic (pacSTL) framework (see reference list) to monitor motion planning RL training in a simulated marine traffic environment. For this I have extended RTAMT with interval arithmetic and characteristic time-point tracking. So I figured it would be worth proposing it as an extension to the library. This issue proposes extending RTAMT with Interval Signal Temporal Logic (I-STL) and pacSTL, enabling monitoring under uncertainty by using reachable sets. The extension operate at the semantics layer only, no grammar changes are needed.

Motivation

In practice, signals are uncertain, predicates may have uncertain parameters. I-STL and pacSTL address this by propagating interval-valued uncertainty through the STL semantics. See for more details:

• I-STL (Baird et al., IEEE CSL 2023): replaces scalar robustness with interval robustness using minimal inclusion functions for min and max, yielding three-valued semantics (TRUE / FALSE / UNDEF).

• pacSTL (Dietrich, Krasowski et al., 2025): extends I-STL with characteristic time-point tracking, enabling PAC probabilistic guarantees on robustness intervals when combined with external reachable set predictions.

Proposed Design Decisions

• Subclass existing visitors: Using the offline and discrete instance as an example: IStlDiscreteTimeOfflineAstVisitor extends StlDiscreteTimeOfflineAstVisitor, overriding methods to operate on intervals. Same pattern for other visitors.

• No syntax changes: STL grammar is reused as-is.

• Optimization lives outside RTAMT: For pacSTL, RTAMT handles interval propagation and time-point tracking. The user is responsible for computing interval signals from reachable sets (via whatever optimization engine suits their problem). This keeps RTAMT focused on temporal logic monitoring.

• Interval Arithmetic: We use a modified npinterval custom numpy dtype, which overwrites most standard arithmetic operators (+, -, *, /, comparisons) for interval types. However, min/max and abs follow a different syntax in npinterval, so the visitor methods explicitly call the interval-specific .minimum(), .maximum(), and interval abs operations rather than relying on operator overloading. This means that most of the implementation would entail overwriting operations in the AstVisitor class.

• pacSTL: Extend I-STL with characteristic time-point tracking. Every method returns (robustness, t_lows, t_highs) where t_lows[i] and t_highs[i] record which time steps determined the lower and upper bounds. This would only be done on a trace, which means that we only would need to implement pacSTL for an offline use-case. This could be passed as an option on initialization and would have to be handled in the StlDiscreteTimeSpecification function.