.. _ltl: 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. 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 :math:`X`. :math:`X` can be one of the following: - :math:`G(p,t)` (globally): checks that a predicate :math:`p` is true for all future timesteps after :math:`t` - :math:`F(p,t)` (finally): checks that a predicate :math:`p` is true at least once after timestep :math:`t` - :math:`X(p,t)` (next): checks that if a predicate :math:`p` is true for timestep :math:`t`, then it is true for timestep :math:`t+1` - :math:`U(p1,p2)` (until): checks that :math:`p1` is true for at least one timestep, and that during all timesteps beforehand, :math:`p2` is true Implementing LTL in CAISAR -------------------------- Representing time with a Matrix ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We represent a set of sampled values as a matrix :math:`M \in \mathbb{R}^t\times\mathbb{R}^d` where :math:`t` is the number of discret samples and :math:`d` the feature space. .. literalinclude:: ../../stdlib/caisar/types.mlw :language: whyml :start-at: theory Matrix :end-at: end We can then implement LTL operators using WhyML likeso: Globally ~~~~~~~~ .. literalinclude:: ../../examples/ltl/ltl-small.why :language: whyml :start-after: @BEGIN INCLUDE GLOBALLY_DEFINITION@ :end-before: @END INCLUDE GLOBALLY_DEFINITION@ Finally ~~~~~~~ .. literalinclude:: ../../examples/ltl/ltl-small.why :language: whyml :start-after: @BEGIN INCLUDE FINALLY_DEFINITION@ :end-before: @END INCLUDE FINALLY_DEFINITION@ Next ~~~~ .. literalinclude:: ../../examples/ltl/ltl-small.why :language: whyml :start-after: @BEGIN INCLUDE NEXT_DEFINITION@ :end-before: @END INCLUDE NEXT_DEFINITION@ Until ~~~~~ .. literalinclude:: ../../examples/ltl/ltl-small.why :language: whyml :start-after: @BEGIN INCLUDE UNTIL_DEFINITION@ :end-before: @END INCLUDE UNTIL_DEFINITION@ Those theories can be placed inside of the ``stdlib`` folder; CAISAR will then be able to use them in future specification. 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. 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 :math:`\neg G \Psi \implies f(x) = 1` :math:`\equiv F (\neg \Psi) \implies f (x) = 1`, where :math:`\Psi` represents a formula describing a chemical or physical law and :math:`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 :math:`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. 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 :math:`y_1` being larger than :math:`y_0` . Formally, this can be expressed as :math:`\phi_1 \equiv F (x_{temperature} \leq 0) \implies y_0 \leq y_1` where :math:`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. .. literalinclude:: ../../examples/ltl/ltl-small.why :language: whyml :start-after: @BEGIN INCLUDE COLBOUND@ :end-before: @END INCLUDE COLBOUND@ We can then write our property using this function: .. literalinclude:: ../../examples/ltl/ltl-small.why :language: whyml :start-after: @BEGIN INCLUDE GOAL_LTL@ :end-before: @END INCLUDE GOAL_LTL@ .. code-block:: console $ 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. More complex properties ~~~~~~~~~~~~~~~~~~~~~~~ A complete theory of matrices and LTL properties used in [Lutz2027]_ are available under the `caisar repository examples `_. .. [Biere2003] 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 .. [Lutz2027] Lutz, S., Girard-Satabin, J., Neider, D., (2027), *Verification of LTL properties on Neural Networks for Chemical Process Monitoring*, AI Verification, doi: 10.1007/978-3-032-32357-6_15