Documentation/trace/rv/linear_temporal_logic.rst

Source file repositories/reference/linux-study-clean/Documentation/trace/rv/linear_temporal_logic.rst

File Facts

System
Linux kernel
Corpus path
Documentation/trace/rv/linear_temporal_logic.rst
Extension
.rst
Size
4345 bytes
Lines
135
Domain
Support Tooling And Documentation
Bucket
Documentation
Inferred role
Support Tooling And Documentation: documentation
Status
atlas-only

Why This File Exists

Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.

Dependency Surface

Detected Declarations

Annotated Snippet

Linear temporal logic
=====================

Introduction
------------

Runtime verification monitor is a verification technique which checks that the
kernel follows a specification. It does so by using tracepoints to monitor the
kernel's execution trace, and verifying that the execution trace sastifies the
specification.

Initially, the specification can only be written in the form of deterministic
automaton (DA).  However, while attempting to implement DA monitors for some
complex specifications, deterministic automaton is found to be inappropriate as
the specification language. The automaton is complicated, hard to understand,
and error-prone.

Thus, RV monitors based on linear temporal logic (LTL) are introduced. This type
of monitor uses LTL as specification instead of DA. For some cases, writing the
specification as LTL is more concise and intuitive.

Many materials explain LTL in details. One book is::

  Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
  Press, 2008.

Grammar
-------

Unlike some existing syntax, kernel's implementation of LTL is more verbose.
This is motivated by considering that the people who read the LTL specifications
may not be well-versed in LTL.

Grammar:
    ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl

Operands (opd):
    true, false, user-defined names consisting of upper-case characters, digits,
    and underscore.

Unary Operators (unop):
    always
    eventually
    next
    not

Binary Operators (binop):
    until
    and
    or
    imply
    equivalent

This grammar is ambiguous: operator precedence is not defined. Parentheses must
be used.

Example linear temporal logic
-----------------------------
.. code-block::

   RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA)

means: if it is raining, going outside means having an umbrella.

.. code-block::

   RAIN imply (WET until not RAIN)

means: if it is raining, it is going to be wet until the rain stops.

Annotation

Implementation Notes