Temporal Logic Operators¶

class jlnn.reasoning.temporal.AlwaysNode(*args: Any, **kwargs: Any)[source]¶

Bases: Node

Implementation of the ‘Always’ (Globally) temporal operator, denoted as $mathcal{G}$.

In Linear Temporal Logic (LTL), the formula $mathcal{G}phi$ is true if the sub-formula $phi$ holds at every time step within a given sequence. Within the JLNN framework, this is realized as a generalized conjunction (AND) over the temporal axis.

It utilizes the Gödel t-norm (minimum) to aggregate truth intervals, ensuring that the resulting lower bound represents the “least true” moment in the time series.

child¶

The logical subtree or formula to be evaluated over time.

Type:: Node

window_size¶

The specific temporal look-ahead window. If None, the operator applies to the entire input sequence.

Type:: Optional[int]

forward(values: Dict[str, Array]) → Array[source]¶

Calculates the minimum truth interval across the temporal dimension.

Computes the intersection of truth values over time, effectively finding the invariant truth level of the sequence.

Parameters:: values – A dictionary of input tensors where the temporal dimension is expected at axis 1.
Returns:: A JAX array of truth intervals $[L, U]$ with the temporal dimension collapsed via the min operation.

class jlnn.reasoning.temporal.EventuallyNode(*args: Any, **kwargs: Any)[source]¶

Bases: Node

Implementation of the ‘Eventually’ (Finally) temporal operator, denoted as $mathcal{F}$.

In LTL, the formula $mathcal{F}phi$ is true if the sub-formula $phi$ holds at least once at some point in the future or present. In JLNN, this is implemented as a generalized disjunction (OR) over the temporal axis.

It utilizes a t-conorm (maximum) to aggregate truth intervals, meaning the overall truth is determined by the “most true” moment in the sequence.

child¶

The logical subtree to be evaluated.

Type:: Node

window_size¶

The specific temporal look-ahead window.

Type:: Optional[int]

forward(values: Dict[str, Array]) → Array[source]¶

Calculates the maximum truth interval across the temporal dimension.

Determines the peak truth value within the sequence, identifying if the condition is met at any point.

Parameters:: values – A dictionary of input tensors.
Returns:: A JAX array of truth intervals $[L, U]$ with the temporal dimension collapsed via the max operation.

This module implements operators inspired by Linear Temporal Logic (LTL), optimized for processing time series in JAX.

Implemented Operators:¶

AlwaysNode (Globally): Implemented as a generalized conjunction (AND) over the time axis. Requires the formula to hold at all steps in the window.
EventuallyNode (Finally): Implemented as a generalized disjunction (OR). It suffices for the formula to hold at least once in a moment.

Use:¶

Ideal for analyzing sensor data, where we seek persistent states (Always) or event detection (Eventually) in a sliding window.