Specifications

Once a model has been simulated, the output trace needs to be evaluated into a cost value, which is captured in the Specification interface. In general, a specification implementation can be any arbitrary function so long as it returns a metic value, but in the context of \(\Psi\)-TaLiRo specifications are generally evaluated in terms of system requirements expressed using an extension of Temporal Logic called Signal Temporal Logic (STL).

Introduction to STL

STL is higher-order logic that extends propositional logic (PL) with timed quantifiers, so instead of evaluating formulas for only a single instant in time we can instead evaluate a formula over multiple times. This enables us to write formulas to make assertions about some potentially time-varying properties of a system and verify that the requirement is satisfied as the system evolves at runtime.

The most basic building block of a STL formula is the predicate, which is an inequality of the form \(\textbf{a} \cdot \textbf{x} \leq b\) where the expression \(\textbf{a} \cdot \textbf{x}\) is the first-order sum of variables representing the system state, and \(b\) is a constant. The following is are some examples of predicates:

altitude >= 0.0

flow_rate - drain_rate >= 1.0

0.5 * brake + 2.0 * throttle <= 2500.0

STL formulas also include operators, which can combine or provide timed quantification of sub-formulas. The standard PL operators are supported, which are Not, And, Or, Implies, and Biconditional. The most primitive temporal operator introduced by STL is the Next operator, which asserts that for a given moment, the sub-formula holds at the following moment. STL also introduces the Until operator, which is a binary operator that requires its left sub-formula to hold until the moment before its right sub-formula holds (which is required to hold at some moment in time). From these two operators we can derive the rest of the temporal operators, which are the following:

Eventually

Unary operator that requires its sub-formula to hold at some moment in time

Always

Unary operator that requires its sub-formula to hold at all moments in time

Release

Binary operator that requires its right sub-formula to hold as long as the left sub-formula holds

The table below shows the operators and their common representations in STL formulas, as well as their -arity (how many operands they accept).

Operator name	Representation	Arity
And	and, &&, or \(\wedge\)	2
Or	or, ||, or \(\vee\)	2
Not	not or !, or \(\neg\)	1
Implication	implies, ->, or \(\rightarrow\)	2
Biconditional	<-> or \(\leftrightarrow\)	2
Next [1]	next, X, or \(\circ\)	1
Eventually [2]	eventually, F, or \(\Diamond\)	1
Always [2]	always, G, or \(\square\)	1
Until [2]	until, U, or \(\mathcal{U}\)	2
Release [2]	release, R, or \(\mathcal{R}\)	2

Notes

[1]

Only supported for discrete time specifications

[2] (1,2,3,4)

Operator optionally supports an interval written OP[t_starts, t_end] .... Without an interval, an operator applies for all time.

The following are some examples of requirements written using STL:

Requirement	STL representation
Do not come in contact with the ground	always (altitude >= 0)
Never enter the region \([10 \leq x \leq 20] \times [0 \leq y \leq 5]\)	\(G (not (x \geq 10~and~x \leq 20~and~y \leq 5~and~y \geq 0))\)
Exit the region 4 seconds after entering it	\(\square ((x\geq 10\wedge x\leq 20\wedge y\leq 5\wedge y\geq 0) \rightarrow \Diamond_{[0,4]}~\neg(x\geq 10\wedge x\leq 20\wedge y\leq 5\wedge y\geq 0))\)

Base Class

Implementing a specification can be accomplished by inheriting from the Specification class, which has one required method called evaluate() that accepts a Trace value and returns a result containing the cost value as well as any additional annotation data. The Specification[S, C, E] class is parameterized by 3 type variables: S represents the type of the system states that the specification expects, C represents the type of the cost value returned, and E represents the type of the annotation data.

from staliro import Result, Trace
from staliro.specifications import Specification

class Spec(Specification[list[float], float, None]):
    def evaluate(self, trace: Trace[list[float]]) -> Result[float, None]:
        ...

Decorator

For specifications that only depend on their inputs, you can also use the specification() decorator to create a Specification from a plain Python function.

from staliro import Result, Trace, specifications

@specifications.specification()
def spec(trace: Trace[list[float]]) -> Result[float, None]:
    ...

RTAMT

In order to evaluate a STL formula, a program called a monitor is required. One such monitor is RTAMT, developed by Dejan Nickovic and Tomoya Yamaguchi. Two specification implementations are provided using this library: Discrete and Dense. Both specifications accept the same constructor parameters, which allow users to select the type of state values expected by the optimizer. To create an instance of either class you must provide a formula written in STL and a dictionary mapping the variable names in the formula to columns in the state value, which is expected to be a list.

from staliro.models import Trace
from staliro.optimizers import rtamt

specification = rtamt.parse_dense("always (alt >= 0)", {"alt": 0})
states = {
    0.0: [2250.0],
    1.0: [2248.7],
    2.0: [2247.3],
}

specification.evaluate(Trace(states))

As an alternative method of construction, you can omit the variable-column mapping which will change the specification to expect dictionaries containing each variable in the formula.

from staliro.models import Trace
from staliro.optimizers import rtamt

specification = rtamt.parse_discrete("always (alt >= 0)")
states = {
    0.0: {"alt": 2250.0},
    1.0: {"alt": 2248.7},
    2.0: {"alt": 2247.3},
}

specification.evaluate(Trace(states))