4.5. Specifying temporal properties¶
This chapter was written based on a work from Simon Lutz [Lutz2027].
Being able to express specifications on time allow to model a wide range of phenomena, such as degradation over time or conservation of quantities. This can be applied for predictive maintenance or checking that some property stays true during multiple observations.
Given a finite number of time steps, we can draw from the theory of Bounded Linear Temporal Logic (or Bounded Model-Checking) [Biere2003] to write a specification for such systems with the CAISAR language. This tutorial will show how to express the Bounded LTL theory and verify a property on an industrial use-case.
4.5.1. Linear Temporal Logic (LTL)¶
LTL is a particular kind of logic derived from predicate logic with additional operators (this is also called a modal logic). We denote those modal operators \(X\). \(X\) can be one of the following:
\(G(p,t)\) (globally): checks that a predicate \(p\) is true for all future timesteps after \(t\)
\(F(p,t)\) (finally): checks that a predicate \(p\) is true at least once after timestep \(t\)
\(X(p,t)\) (next): checks that if a predicate \(p\) is true for timestep \(t\), then it is true for timestep \(t+1\)
\(U(p1,p2)\) (until): checks that \(p1\) is true for at least one timestep, and that during all timesteps beforehand, \(p2\) is true
4.5.2. Implementing LTL in CAISAR¶
4.5.2.1. Representing time with a Matrix¶
We represent a set of sampled values as a matrix \(M \in \mathbb{R}^t\times\mathbb{R}^d\) where \(t\) is the number of discret samples and \(d\) the feature space.
theory Matrix
use Vector
use int.Int
(* Flat representation. [r] is the number of rows, [c] the number of columns *)
type t 'a = {d: vector 'a; r: int; c: int}
(* True if the matrix has [r] rows and [c] columns *)
predicate has_shape (m: t 'a) (r: int) (c: int) =
m.r = r /\ m.c = c
(* True if the provided index [i] is between 0 and the number of rows *)
predicate valid_row (m: t 'a) (i: int) =
0 <= i /\ i < m.r
(* True if the provided index [j] is between 0 and the number of columns *)
predicate valid_column (m: t 'a) (j: int) =
0 <= j /\ j < m.c
predicate valid_coordinate (m: t 'a) (i: int) (j: int) =
valid_row m i /\ valid_column m j
(* [get m i j] returns the value located at row [i] and column [j] in matrix [m] *)
function get (m: t 'a) (i: int) (j: int) : 'a =
let coord = (i * m.c) + j in m.d[coord]
end
We can then implement LTL operators using WhyML likeso:
4.5.2.2. Globally¶
(* The "Globally" (G) operator in LTL. Given a predicate [p] on a matrix [m],
a timestep [i],
G checks that [p] is valid for all future timesteps after [i].
*)
function global_m
(p: Matrix.t 'a-> int -> bool)
(m: Matrix.t 'a)
(i: int)
: bool =
valid_row m i /\ forall j: index. i <= j < m.r -> p m j
4.5.2.3. Finally¶
(* The "Finally" (F) operator in LTL. Given a predicate [p] on a matrix [m],
a timestep [i],
F checks that [p] is valid for at least one timestep after [i].
*)
function final_m (p: Matrix.t 'a -> int -> bool) (m: Matrix.t 'a) (i: int): bool =
valid_row m i /\ (exists j: index. i <= j < m.r /\ p m j)
4.5.2.4. Next¶
(* The "Next" (X) operator in LTL. Given a predicate [p] on a matrix [m],
timestep [i],
X checks that [p] is valid for the next timestep after [i].
*)
function next_m (p: Matrix.t 'a -> int -> bool) (m: Matrix.t 'a) (i: int): bool =
valid_row m i /\ valid_row m (i + 1) /\ p m (i + 1)
4.5.2.5. Until¶
(* Given two predicates [p] and [q] on a matrix [m],
a timestep [i], [until_m] checks that [F q m i] holds and that until then,
[G p m k] holds, for k >= i *)
function until_m
(p: Matrix.t 'a -> int -> bool)
(q: Matrix.t 'a -> int -> bool)
(m: Matrix.t 'a) (i: int)
: bool =
valid_row m i /\ (
exists j: index. i <= j < m.r /\ q m j /\
forall k: index. (i <= k < j) -> p m k
)
Those theories can be placed inside of the stdlib folder; CAISAR will then
be able to use them in future specification.
4.5.3. Application: verifying a neural network for chemical process monitoring¶
We check properties on a neural network used for batch distillation monitoring. Batch distillation processes often run only for a certain time frame in a lab-scale distillation plant and are in general used for small-scale production units with high product-quality requirements. Detecting anomalies in chemical processes is a crucial task to ensure the safety of chemical plants and their operators. When an anomaly is missed, this can cause severe environmental damage or endanger human lives as unexpected behavior can lead to fatal incidents such as the ex- plosion of a plant. When developing machine learning solutions to assist human operators by automatically detecting anomalies in a process, it needs to be ensured that these neural anomaly detectors are safe and reliable.
4.5.3.1. Formalization¶
The properties we aim to verify are inspired by chemical laws that need to stay true whenever the plant operates in a normal condition. Whenever such a law is violated, an anomaly must be detected. Formally, these correctness properties are given by formulas \(\neg G \Psi \implies f(x) = 1\) \(\equiv F (\neg \Psi) \implies f (x) = 1\), where \(\Psi\) represents a formula describing a chemical or physical law and \(f (x) = 1\) indicates that the neural network f predicts an anomaly.
All properties assume time series containing the sensor readings of 4 features for 5 time-steps as input and a neural network \(f : \mathbb{R}^{20} \mapsto \mathbb{R}^2\) described as above. Note that in the implementation of the properties within CAISAR the thresholds below are normalized following the same normalization process used during the training of the network.
4.5.3.2. Temperature constant¶
The first property describes the physical law that the temperature in the plant can never be zero or below. Therefore, whenever the input to the neural network contains a value below or equal to zero, an anomaly should be predicted, as indicated by the output \(y_1\) being larger than \(y_0\) . Formally, this can be expressed as \(\phi_1 \equiv F (x_{temperature} \leq 0) \implies y_0 \leq y_1\) where \(x_{temperature}\) refers to the sensor readings of the temperature sensor.
First, we write a small helper function to help us bound a particular column of the matrix with a given value. In our setting, it is equivalent to bound a certain feature vector for all timesteps.
(* Function parametrized by a matrix [m]. Ensures has all values of column
[j] are bounded by constant [c] for all timesteps. *)
function matrix_column_bound
(j: index)
(c: Float64.t)
: (Matrix.t Float64.t -> int -> bool) =
(*_k unused, here to accomodate the Global predicate *)
fun m _k ->
forall i: index. valid_row m i -> c .<= get m i j
We can then write our property using this function:
(* G_1: checks that when the temperature is above a certain threshold for at
least one timestep, then the first output is below the second output*)
goal G_1:
let rows = 5 in
let columns = 4 in
let lb = (-1.0:Float64.t) in
let ub = (1.0:Float64.t) in
let temperature_index = 0 in
let temperature = (0.75:Float64.t) in
forall v: vector Float64.t. has_length v (rows * columns) ->
let m = {d = v; r = rows; c = columns} in
matrix_valid_input_same_bounds m lb ub ->
let temperature_bounded = matrix_column_bound temperature_index temperature
in
let out = (nn @@ m.d) in
final_m (temperature_bounded) m 0 -> out[0] .<= out[1]
$ caisar verify examples/ltl/ltl-small.why --prover Marabou -m 8GB
Verifying with CAISAR returns an Invalid, meaning that the temperature never
goes below the defined threshold.
4.5.3.3. More complex properties¶
A complete theory of matrices and LTL properties used in [Lutz2027] are available under the caisar repository examples.
Biere A.; Heljanko K.; Junttila T; Latvala T.; Schuppan V. (2003). Linear Encodings of Bounded LTL Model Checking, Logical Methods in Computer Science, doi: 10.2168/LMCS-2(5:5)2006