Appendix A – System Temporal Logic

Formal requirements are expressed in system temporal logic¹, 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))².

It is based on atomic formulae that may be either “TRUE” or equal to O(x, y, q)³ 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 t₀):

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 ≠ Ø)⁴,
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“) ) .

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

Appendix A – System Temporal Logic

TABLE OF CONTENTS

REFERENCES