Appendix A – System Temporal Logic

Formal requirements are expressed in system temporal logic1The system temporal logic that we present here is a system-adaptation of the simplest temporal logic used in theoretical computer science, which is called LTL (Linear Temporal Logic; see [8], [11], [45], [54], [64] or [69]). However there exists plenty of other more expressive temporal logics (see [11] or [54]) that can also be adapted to a systems engineering context if necessary, depending of the level of expressivity that may be requested. , a mathematical formalism that we did not present below and that we will discuss in full details in this appendix. System temporal logic is a formal logic that extends the same classical notion for computer programs (see for instance [8], [11], [45], [54], [58], [69] or [64]). Such a logic intends to specify the sequences of input/output and internal observations that can be made on a formal system whose input, output and internal states sets X, Y, Q and timescale T are fixed. In other terms, system temporal logic specifies the sequences O of inputs, outputs and internal states values that can be observed among all moments of time t within the timescale T, as stated below:

O = (O(t)) for all t ∈ T, where we set O(t) = (x(t), y(t), q(t))2Using here the formalism of Definition 0.1..

It is based on atomic formulae that may be either “TRUE” or equal to O(x, y, q)3As we will see below, O(x, y, z) stands for a predicate that will fix the initial value x(t0), y(t0) and q(t0) of the input, output and internal states variables to x, y and q at the initial moment t0 of the considered timescale. where x (resp. y or q) is either an element of the input set X (resp. output set Y or internal states set Q) or equal to some special symbol Ø (that models an arbitrary value), excepted that x, y and q cannot be all equal to Ø.

TRUE, O(x, y, q) for all x ∈ X ∪ {Ø}, y ∈ Y ∪ {Ø} and q ∈ Q ∪ {Ø} with (x, y, z) ≠ (Ø, Ø, Ø ).

Equation 2 – Atomic formulae within system temporal logic 

System temporal logic will then manipulate logical formulae – i.e. well-formed predicates – that are expressing the expected properties of the sequences of inputs, outputs and state variables of a formal system among all moments of time t within a considered timescale. Such a logic involves the two following kinds of logical operators (see [3] and [4] for more details):

  • Two classical truth-functional operators: AND and NOT,
  • Two specific temporal operators X (neXt) and U (Until) whose syntax is provided below:
    o   X f, meaning that formula f is fulfilled at next state,
    o   f U g, meaning that formula f is fulfilled until g becomes fulfilled.

We will provide soon the system semantics of all these different operators. However we now are in position to syntactically define a temporal formula as any well-formed logical formula that may be obtained by applying recursively these different logical operators, starting with an atomic formula. For the sake of simplicity, one may also introduce, on one hand, two other truth-functional operators, OR and → (implies), and on the other hand, two other temporal operators, ◊ (eventually) and □ (always), which can be expressed using the previous operators (hence they do not extend the power of expressivity of the underlying logic), since they allow to state more easily temporal properties:

  • Additional truth-functional logical operators:
    o   f OR g = NOT ( NOT f AND NOT g),
    o   f → g = NOT f OR g (f implies g),
  • Additional temporal operators:
    o     f = TRUE U f (f will be eventually true at some moment of time in the future),
    o  □ f = NOT (NOT f) (f is true at any moment of time).

To end our presentation of system temporal logic, we must of course define the semantics of the different previous logical operators. In other terms, we need to explain when a formal system S whose input, output and internal states sets are X, Y and Q and whose timescale is T, will satisfy to a temporal formula constructed with these operators, which is expressed by writing S ⊨ f, which reads that the system S satisfies to the formula f or equivalently that f is satisfied by S. This satisfaction relationship ⊨ , which provides the semantics of all system temporal formulae, can then be defined inductively according to the following properties (where we systematically set below S[t] for the system that has the same behavior than S, but whose initial moment is t instead of t0):

  • S ⊨ TRUE for any system S,
  • S ⊨ O(x,y,q) if and only if x(t0) = x, y(t0) = y and q(t0) = q (when x, y, q ≠ Ø)4Where t0 stands for the initial moment of the considered timescale T,
  • S ⊨ f AND g if and only S ⊨ f and S ⊨ g,
  • S ⊨ NOT f if and only if one does not have S ⊨ f,
  • S ⊨ X f if and only if S[t0+] ⊨ f,
  • S ⊨ f U g if and only if ∃ t ∈ T such that S[t] ⊨ g and S[u] ⊨ f for all u ∈ T with u < t.

It is also interesting to provide explicitly the semantics of the two additional temporal operators that we introduced above, as it can be deduced from the previous definitions:

  • S ⊨ □ f if and only if for all t ∈ T, one has S[t] ⊨ f,
  • S ⊨ f if and only if there exists t ∈ T such that S[t] ⊨ f.

Our formalism allows to express all usual temporal properties of systems. To be more specific, let us now see how to express a system performance property in this system temporal logic framework. To this purpose, we need first to introduce the two following logical predicates that are here modeling intervals, respectively of input and output values:

X(x0,x1) = AND O(x, Ø, Ø) for all x ∈ [x0,x1] ,
Y(y0,y1) = AND O(x, Ø, Ø) for all y ∈ [y0,y1] .

A typical performance property stating for instance that a system must always have its inputs lying between two values, a and b, and its outputs lying between two other values, c and d, as soon as it enters into the internal state q, will then be expressed as follows:

Performance = □ ( O(Ø, Ø, q) → X(a,b) AND Y(c,d) ).

We can also provide the example of a maintainability property that is generically stated as follows, expressing simply here that a system that satisfy such a property must always go back to a “normal” state when it enters in a non-“normal” state at a certain moment of time:

Maintainability = □ ( NOT O(Ø, Ø, “normal“) → O(Ø, Ø, “normal“) ) .

In the same way, a safety property would finally be generically defined by expressing that a system shall never be in a non-safe state, which can be stated as a system temporal logic invariant:

Safety = □ ( NOT O(Ø, Ø, “non-safe“) ) .

Table des matières

REFERENCES

[3] Aiguier M., Golden B., Krob D., Modeling of Complex Systems II : A minimalist and unified semantics for heterogeneous integrated systems, Applied Mathematics and Computation, 218, (16), 8039-8055, doi : 10.1016/j.amc.2012.01.048, 2012

[4] Aiguier M., Golden B., Krob D., An adequate logic for heterogeneous systems, [dans Proceedings of the 18th International Conference on Engineering of Complex Computer Systems (ICECCS’ 2013), Y. Liu, A. Martin, Eds.], IEEE, 2013 

[8] Artale A., Formal Methods – Lecture III: Linear Temporal Logic, Free University of Bolzano

[11] Baier C., Katoen J.P., Principles of Model Checking, MIT Press, 2008

[45] Katoen J.P., LTL Model Checking, University of Twente, 2009 

[54] Kröger F., Merz S., Temporal Logic and State Systems, Springer, 2008

[58] Manna Z., Pnueli A., The Temporal Logic of Reactive and Concurrent Systems, Springer, 1992

[64] Murray R.M., Linear Temporal Logic, California Institute of Technology, 2012 

[69] Pnueli A., The temporal logics of programs, IEEE 54th Annual Symposium on Foundations of Computer Science (FOCS), 46-57, IEEE, 1977

Nos réseaux