{"id":25628,"date":"2021-08-04T10:53:28","date_gmt":"2021-08-04T08:53:28","guid":{"rendered":"https:\/\/cesam.community\/?p=25628"},"modified":"2022-11-15T11:23:57","modified_gmt":"2022-11-15T10:23:57","slug":"appendix-a-system-temporal-logic","status":"publish","type":"post","link":"https:\/\/cesam.community\/fr\/2021\/08\/04\/appendix-a-system-temporal-logic\/","title":{"rendered":"Appendix A \u2013 System Temporal Logic"},"content":{"rendered":"

Formal requirements are expressed in system temporal logic<\/em>1<\/a><\/sup>The 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. <\/span>, 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:<\/p>\n

O = (O(t)) for all t \u2208 T, where we set O(t) = (x(t), y(t), q(t))2<\/a><\/sup>Using here the formalism of Definition 0.1.<\/span>.<\/p>\n

It is based on atomic formulae that may be either \u201cTRUE\u201d or equal to O(x, y, q)3<\/a><\/sup>As 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.<\/span> 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 \u00d8 (that models an arbitrary value), excepted that x, y and q cannot be all equal to \u00d8.<\/p>\n

TRUE, O(x, y, q) for all x \u2208 X \u222a {\u00d8}, y \u2208 Y \u222a {\u00d8} and q \u2208 Q \u222a {\u00d8} with (x, y, z) \u2260 (\u00d8, \u00d8, \u00d8 ).<\/p>\n<\/div>

Equation 2 \u2013 Atomic formulae within system temporal logic\u00a0<\/span><\/strong><\/p>\n<\/div>

System temporal logic will then manipulate logical formulae \u2013 i.e. well-formed predicates \u2013 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):<\/p>\n