Skip to content

stl

Signal Temporal Logic (STL) operations for trajectory optimization.

This module provides symbolic expression nodes for Signal Temporal Logic (STL) operations, enabling the specification of complex temporal and logical constraints in optimization problems. STL is particularly useful for robotics and autonomous systems where tasks involve temporal reasoning.

STL operators accept Constraint objects (predicates) and extract robustness expressions which are lowered to STLJax during compilation.

Or

Bases: STLExpr

Logical OR operation for STL predicates.

Combines constraint predicates with disjunction. The Or is satisfied if at least one of its operands is satisfied.

During lowering, this is handled by STLJax which computes the smooth maximum (LogSumExp) of the robustness values automatically.

The Or operation allows expressing constraints like: - "Reach either goal A OR goal B" - "Avoid obstacle 1 OR obstacle 2" (at least one must be satisfied) - "Use path 1 OR path 2 OR path 3"

Attributes:

Name Type Description
predicates

List of predicates (Constraint or STLExpr objects)
Example

Visit either waypoint 1 OR waypoint 2:

import openscvx as ox
position = ox.State("pos", shape=(2,))
goal_a = ox.Parameter("goal_a", shape=(2,), value=[1.0, 1.0])
goal_b = ox.Parameter("goal_b", shape=(2,), value=[-1.0, -1.0])

# Define predicates as constraints
reach_a = ox.Norm(position - goal_a) <= 0.5
reach_b = ox.Norm(position - goal_b) <= 0.5

# Combine with OR operator
reach_either = ox.stl.Or(reach_a, reach_b)

# Enforce continuously over time interval
constraints = [reach_either.over((3, 5))]

Nested STL operators are also supported:

# Or of And expressions
expr = ox.stl.Or(
    ox.stl.And(c1, c2),
    ox.stl.And(c3, c4),
)
Note

Or evaluates to a scalar robustness value (positive when satisfied). Use .over() or .at() to convert to a constraint, or manually create a constraint with: -Or(...) <= 0

See Also

stljax.formula.Or: Underlying STLJax implementation used during lowering

Source code in openscvx/symbolic/expr/stl.py 
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
class Or(STLExpr):
    """Logical OR operation for STL predicates.

    Combines constraint predicates with disjunction. The Or is satisfied if
    at least one of its operands is satisfied.

    During lowering, this is handled by STLJax which computes the smooth maximum
    (LogSumExp) of the robustness values automatically.

    The Or operation allows expressing constraints like:
    - "Reach either goal A OR goal B"
    - "Avoid obstacle 1 OR obstacle 2" (at least one must be satisfied)
    - "Use path 1 OR path 2 OR path 3"

    Attributes:
        predicates: List of predicates (Constraint or STLExpr objects)

    Example:
        Visit either waypoint 1 OR waypoint 2:

            import openscvx as ox
            position = ox.State("pos", shape=(2,))
            goal_a = ox.Parameter("goal_a", shape=(2,), value=[1.0, 1.0])
            goal_b = ox.Parameter("goal_b", shape=(2,), value=[-1.0, -1.0])

            # Define predicates as constraints
            reach_a = ox.Norm(position - goal_a) <= 0.5
            reach_b = ox.Norm(position - goal_b) <= 0.5

            # Combine with OR operator
            reach_either = ox.stl.Or(reach_a, reach_b)

            # Enforce continuously over time interval
            constraints = [reach_either.over((3, 5))]

        Nested STL operators are also supported:

            # Or of And expressions
            expr = ox.stl.Or(
                ox.stl.And(c1, c2),
                ox.stl.And(c3, c4),
            )

    Note:
        Or evaluates to a scalar robustness value (positive when satisfied).
        Use `.over()` or `.at()` to convert to a constraint, or manually create
        a constraint with: `-Or(...) <= 0`

    See Also:
        stljax.formula.Or: Underlying STLJax implementation used during lowering
    """

    def __init__(self, *predicates: Union[Constraint, "STLExpr"]):
        """Initialize a logical OR operation.

        Args:
            *predicates: Two or more Constraint or STLExpr objects to combine
                        with logical OR. Each represents a predicate to be satisfied.

        Raises:
            ValueError: If fewer than two predicates are provided
            TypeError: If predicates are not Constraint or STLExpr instances
        """
        if len(predicates) < 2:
            raise ValueError("Or requires at least two predicates")

        # Validate that all predicates are constraints or STL expressions
        for pred in predicates:
            if not isinstance(pred, (Constraint, STLExpr)):
                raise TypeError(
                    f"Or requires Constraint or STLExpr predicates, got "
                    f"{type(pred).__name__}. "
                    f"Did you mean to write a constraint like 'expr <= value'?"
                )

        # Store predicates directly - robustness extraction happens during lowering
        self.predicates = list(predicates)

    def children(self):
        """Return predicates as children."""
        return self.predicates

    def canonicalize(self) -> "Expr":
        """Canonicalize by flattening nested Or and canonicalizing predicates.

        Flattens nested Or operations into a single flat Or with all predicates
        at the same level. For example: Or(a, Or(b, c)) → Or(a, b, c).

        Returns:
            Expr: Canonical form. If only one predicate remains, returns it directly.
        """
        predicates = []

        for pred in self.predicates:
            canonicalized = pred.canonicalize()
            if isinstance(canonicalized, Or):
                # Flatten nested Or: Or(a, Or(b, c)) -> Or(a, b, c)
                predicates.extend(canonicalized.predicates)
            else:
                predicates.append(canonicalized)

        if len(predicates) == 1:
            return predicates[0]

        # Reconstruct Or with canonicalized predicates
        result = Or.__new__(Or)
        result.predicates = predicates
        return result

    def check_shape(self) -> Tuple[int, ...]:
        """Validate predicate shapes and return scalar shape.

        Returns:
            tuple: Empty tuple () indicating a scalar result (STL robustness)

        Raises:
            ValueError: If fewer than two predicates exist
        """
        if len(self.predicates) < 2:
            raise ValueError("Or requires at least two predicates")

        # Validate all predicates
        for pred in self.predicates:
            pred.check_shape()

        # Or produces a scalar (STL robustness value)
        return ()

    def __repr__(self) -> str:
        predicates_repr = " | ".join(repr(p) for p in self.predicates)
        return f"Or({predicates_repr})"
__init__(*predicates: Union[Constraint, STLExpr])

Initialize a logical OR operation.

Parameters:

Name Type Description Default
*predicates Union[Constraint, STLExpr]

Two or more Constraint or STLExpr objects to combine with logical OR. Each represents a predicate to be satisfied.

 ()

Raises:

Type Description
ValueError

If fewer than two predicates are provided
TypeError

If predicates are not Constraint or STLExpr instances
Source code in openscvx/symbolic/expr/stl.py 
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
def __init__(self, *predicates: Union[Constraint, "STLExpr"]):
    """Initialize a logical OR operation.

    Args:
        *predicates: Two or more Constraint or STLExpr objects to combine
                    with logical OR. Each represents a predicate to be satisfied.

    Raises:
        ValueError: If fewer than two predicates are provided
        TypeError: If predicates are not Constraint or STLExpr instances
    """
    if len(predicates) < 2:
        raise ValueError("Or requires at least two predicates")

    # Validate that all predicates are constraints or STL expressions
    for pred in predicates:
        if not isinstance(pred, (Constraint, STLExpr)):
            raise TypeError(
                f"Or requires Constraint or STLExpr predicates, got "
                f"{type(pred).__name__}. "
                f"Did you mean to write a constraint like 'expr <= value'?"
            )

    # Store predicates directly - robustness extraction happens during lowering
    self.predicates = list(predicates)
canonicalize() -> Expr

Canonicalize by flattening nested Or and canonicalizing predicates.

Flattens nested Or operations into a single flat Or with all predicates at the same level. For example: Or(a, Or(b, c)) → Or(a, b, c).

Returns:

Name Type Description
Expr Expr

Canonical form. If only one predicate remains, returns it directly.
Source code in openscvx/symbolic/expr/stl.py 
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
def canonicalize(self) -> "Expr":
    """Canonicalize by flattening nested Or and canonicalizing predicates.

    Flattens nested Or operations into a single flat Or with all predicates
    at the same level. For example: Or(a, Or(b, c)) → Or(a, b, c).

    Returns:
        Expr: Canonical form. If only one predicate remains, returns it directly.
    """
    predicates = []

    for pred in self.predicates:
        canonicalized = pred.canonicalize()
        if isinstance(canonicalized, Or):
            # Flatten nested Or: Or(a, Or(b, c)) -> Or(a, b, c)
            predicates.extend(canonicalized.predicates)
        else:
            predicates.append(canonicalized)

    if len(predicates) == 1:
        return predicates[0]

    # Reconstruct Or with canonicalized predicates
    result = Or.__new__(Or)
    result.predicates = predicates
    return result
check_shape() -> Tuple[int, ...]

Validate predicate shapes and return scalar shape.

Returns:

Name Type Description
tuple Tuple[int, ...]

Empty tuple () indicating a scalar result (STL robustness)

Raises:

Type Description
ValueError

If fewer than two predicates exist
Source code in openscvx/symbolic/expr/stl.py 
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
def check_shape(self) -> Tuple[int, ...]:
    """Validate predicate shapes and return scalar shape.

    Returns:
        tuple: Empty tuple () indicating a scalar result (STL robustness)

    Raises:
        ValueError: If fewer than two predicates exist
    """
    if len(self.predicates) < 2:
        raise ValueError("Or requires at least two predicates")

    # Validate all predicates
    for pred in self.predicates:
        pred.check_shape()

    # Or produces a scalar (STL robustness value)
    return ()
children()

Return predicates as children.

Source code in openscvx/symbolic/expr/stl.py 
201
202
203
def children(self):
    """Return predicates as children."""
    return self.predicates

STLExpr

Bases: Expr

Base class for Signal Temporal Logic operators.

STL operators combine predicates (constraints) using temporal and logical operations. This base class provides: - Common functionality for all STL operators - Helper methods like .over() and .at() to convert STL expressions to constraints - Future: utility methods for STL formula manipulation, pretty-printing, etc.

STL operators are Expr nodes that store robustness expressions. During lowering, they are handled by STLJax which computes the appropriate smooth approximations.

STL Robustness Convention

STL uses "robustness" values that are positive when constraints are satisfied. For an Inequality constraint lhs <= rhs: - Constraint residual: lhs - rhs (should be <= 0 when satisfied) - STL robustness: rhs - lhs (should be >= 0 when satisfied)

Example

STL operators can be converted to constraints using helper methods:

wp1 = Norm(pos - c_1) <= r_1
wp2 = Norm(pos - c_2) <= r_2
visit_either = ox.stl.Or(wp1, wp2)  # STL operator

# Convert to constraint with .over()
constraints = [visit_either.over((3, 5))]
Note

This is a base class. Use concrete subclasses like Or, And, Eventually, Always, or Until for actual STL specifications.

Source code in openscvx/symbolic/expr/stl.py 
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
class STLExpr(Expr):
    """Base class for Signal Temporal Logic operators.

    STL operators combine predicates (constraints) using temporal and logical
    operations. This base class provides:
    - Common functionality for all STL operators
    - Helper methods like `.over()` and `.at()` to convert STL expressions to constraints
    - Future: utility methods for STL formula manipulation, pretty-printing, etc.

    STL operators are Expr nodes that store robustness expressions. During lowering,
    they are handled by STLJax which computes the appropriate smooth approximations.

    STL Robustness Convention:
        STL uses "robustness" values that are positive when constraints are satisfied.
        For an Inequality constraint `lhs <= rhs`:
        - Constraint residual: `lhs - rhs` (should be <= 0 when satisfied)
        - STL robustness: `rhs - lhs` (should be >= 0 when satisfied)

    Example:
        STL operators can be converted to constraints using helper methods:

            wp1 = Norm(pos - c_1) <= r_1
            wp2 = Norm(pos - c_2) <= r_2
            visit_either = ox.stl.Or(wp1, wp2)  # STL operator

            # Convert to constraint with .over()
            constraints = [visit_either.over((3, 5))]

    Note:
        This is a base class. Use concrete subclasses like Or, And,
        Eventually, Always, or Until for actual STL specifications.
    """

    def over(
        self,
        interval: tuple[int, int],
        penalty: str = "squared_relu",
        idx: Optional[int] = None,
        check_nodally: bool = False,
    ) -> "CTCS":
        """Apply this STL expression over a continuous interval using CTCS.

        Converts the STL expression to a constraint and wraps it in CTCS
        for continuous-time enforcement.

        Args:
            interval: Tuple of (start, end) node indices for enforcement interval
            penalty: Penalty function type for CTCS
            idx: Optional grouping index for multiple augmented states
            check_nodally: Whether to also enforce at discrete nodes

        Returns:
            Continuous-time constraint satisfaction wrapper

        Example:
            Enforce STL expression over an interval:

                visit_either = ox.stl.Or(wp1, wp2)
                constraint = visit_either.over((3, 5))
        """
        from .arithmetic import Neg
        from .constraint import CTCS, Inequality

        # Create constraint: -STL_expr(...) <= 0
        # STL expressions evaluate to robustness (positive when satisfied)
        # We negate to get constraint residual (negative when satisfied)
        constraint = Inequality(Neg(self), Constant(np.array(0.0)))

        return CTCS(
            constraint, penalty=penalty, nodes=interval, idx=idx, check_nodally=check_nodally
        )

    def at(self, nodes: Union[list, tuple]) -> "NodalConstraint":
        """Apply this STL expression only at specific nodes.

        Converts the STL expression to a constraint and wraps it in NodalConstraint.

        Args:
            nodes: List of node indices where the constraint should be enforced

        Returns:
            Nodal constraint wrapper

        Example:
            Enforce STL expression at specific nodes:

                visit_either = ox.stl.Or(wp1, wp2)
                constraint = visit_either.at([0, 5, 10])
        """
        from .arithmetic import Neg
        from .constraint import Inequality, NodalConstraint

        # Create constraint: -STL_expr(...) <= 0
        constraint = Inequality(Neg(self), Constant(np.array(0.0)))

        if isinstance(nodes, int):
            nodes = [nodes]
        return NodalConstraint(constraint, list(nodes))
at(nodes: Union[list, tuple]) -> NodalConstraint

Apply this STL expression only at specific nodes.

Converts the STL expression to a constraint and wraps it in NodalConstraint.

Parameters:

Name Type Description Default
nodes Union[list, tuple]

List of node indices where the constraint should be enforced

 required

Returns:

Type Description
NodalConstraint

Nodal constraint wrapper
Example

Enforce STL expression at specific nodes:

visit_either = ox.stl.Or(wp1, wp2)
constraint = visit_either.at([0, 5, 10])
Source code in openscvx/symbolic/expr/stl.py 
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
def at(self, nodes: Union[list, tuple]) -> "NodalConstraint":
    """Apply this STL expression only at specific nodes.

    Converts the STL expression to a constraint and wraps it in NodalConstraint.

    Args:
        nodes: List of node indices where the constraint should be enforced

    Returns:
        Nodal constraint wrapper

    Example:
        Enforce STL expression at specific nodes:

            visit_either = ox.stl.Or(wp1, wp2)
            constraint = visit_either.at([0, 5, 10])
    """
    from .arithmetic import Neg
    from .constraint import Inequality, NodalConstraint

    # Create constraint: -STL_expr(...) <= 0
    constraint = Inequality(Neg(self), Constant(np.array(0.0)))

    if isinstance(nodes, int):
        nodes = [nodes]
    return NodalConstraint(constraint, list(nodes))
over(interval: tuple[int, int], penalty: str = 'squared_relu', idx: Optional[int] = None, check_nodally: bool = False) -> CTCS

Apply this STL expression over a continuous interval using CTCS.

Converts the STL expression to a constraint and wraps it in CTCS for continuous-time enforcement.

Parameters:

Name Type Description Default
interval tuple[int, int]

Tuple of (start, end) node indices for enforcement interval

 required
penalty str

Penalty function type for CTCS

 'squared_relu'
idx Optional[int]

Optional grouping index for multiple augmented states

 None
check_nodally bool

Whether to also enforce at discrete nodes

 False

Returns:

Type Description
CTCS

Continuous-time constraint satisfaction wrapper
Example

Enforce STL expression over an interval:

visit_either = ox.stl.Or(wp1, wp2)
constraint = visit_either.over((3, 5))
Source code in openscvx/symbolic/expr/stl.py 
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
def over(
    self,
    interval: tuple[int, int],
    penalty: str = "squared_relu",
    idx: Optional[int] = None,
    check_nodally: bool = False,
) -> "CTCS":
    """Apply this STL expression over a continuous interval using CTCS.

    Converts the STL expression to a constraint and wraps it in CTCS
    for continuous-time enforcement.

    Args:
        interval: Tuple of (start, end) node indices for enforcement interval
        penalty: Penalty function type for CTCS
        idx: Optional grouping index for multiple augmented states
        check_nodally: Whether to also enforce at discrete nodes

    Returns:
        Continuous-time constraint satisfaction wrapper

    Example:
        Enforce STL expression over an interval:

            visit_either = ox.stl.Or(wp1, wp2)
            constraint = visit_either.over((3, 5))
    """
    from .arithmetic import Neg
    from .constraint import CTCS, Inequality

    # Create constraint: -STL_expr(...) <= 0
    # STL expressions evaluate to robustness (positive when satisfied)
    # We negate to get constraint residual (negative when satisfied)
    constraint = Inequality(Neg(self), Constant(np.array(0.0)))

    return CTCS(
        constraint, penalty=penalty, nodes=interval, idx=idx, check_nodally=check_nodally
    )