A model parametric real-time logic

A Model Parametric Real-Time Logic1

2

Angelo Morzenti, Dino Mandrioli, Carlo Ghezzi Politecnico di Milano, Dipartimento di Elettronica

Abstract TRIO is a formal notation for logic-based specification of real-time systems. In this paper, we briefly summarise the language and its straightforward model-theoretic semantics. Then we discuss the need for assigning a consistent meaning to TRIO specifications, with reference to a variety of underlying time structures such as infinite time structures (both dense and discrete) and finite time structures. The main motivation is the ability to validate formal specifications. We present a solution to this problem, which gives a new, model-parametric semantics to the language. We define an algorithm for constructively verifying the satisfiability of formulas in the decidable cases, and we characterize several important temporal properties of specifications. Categories and subject descriptors: D.2.1. [Requirements/Specification]: Languages, Tools; D.4.7. [Organization and Design]: Real-time and embedded systems; F.4.1. [Mathematical Logic]: Model theory. General Terms: real-time systems, formal specifications, first-order logic. Additional Key Words and Phrases: requirements validation, temporal logic, model-theoretic semantics.

1. Introduction Real-time systems are systems whose functionalities are constrained by strict response-time bounds. Very often, such systems may be viewed as embedded computer applications: a computer interacts with an external environment which evolves according to its own logic and interacts with the computer in an unpredictable way, by sending data at a speed that is not under computer control. Sample realtime systems are industrial process control applications, such as chemical and nuclear plant control systems, flight control systems, or patient monitoring systems. In all such applications, a failure of the control system to react to certain input data within some specified time bounds can cause severe damages or even fatal disasters. As [33] points out, “time” plays a fundamental role in real-time systems, in that their correctness depends on time. If certain events happen too early or too late–where “early” and “late” may be stated precisely in terms of some time scale that depends on the application–

1 This work was partially supported by CNR-Progetto Finalizzato Sistemi Informativi e Calcolo Parallelo and by

ENEL-CRA. 2 This paper appeared on ACM Transactions on Programming Languages and Systems 14, 3 July 1992.

1

the application is incorrect. This constitutes a sharp departure from sequential and concurrent systems, where time affects performance, not correctness. The goal of our research is to provide language support to the formal specification of real-time systems. Based on such language, we are designing an environment which provides tools for writing and analyzing formal specifications, and thus assess their validity before any development takes place. In particular, the environment supports the execution of formal specifications. The importance of executing formal specifications to validate requirements has been advocated, among others, by [13]. By executing formal specifications and observing the behavior of the specified system, one can check whether specifications capture the intended functional requirements or not. For example, one can check whether certain undesired sequences of events do not arise in some critical circumstances. In other terms, by executing requirements, we perform testing in the early phase of the development process. Although testing cannot prove the absence of errors, it is especially valuable as a mechanism for testing functional requirements. In a previous paper [10] we gave a first definition of TRIO, a logic language we developed for specifying real-time systems. TRIO is one of several extensions of classical temporal logic [17, 29] that introduce a quantitative view of time, so that time distances can be measured. The inadequacy of classical temporal logic to the specification of real-time systems stems from the fact that its operators provide only a qualitative view of time, thus providing a way to express properties like precedence, eventuality or invariance. It is only with the introduction of the next-time operator that temporal logic gets close to a quantitative view of time: for example, by using it one can state that a given property will hold k time units from the current time instant. The next-time operator, however, is meaningful only with reference to a discrete time domain, like that one used in [17] to model the execution of synchronous concurrent programs; it cannot deal with dense time structures which are needed to model asynchronous and non-discrete systems. Another approach is followed by the interval logic of [12, 24], which provides the ‘chop’ operator for interval concatenation and permits the immediate description of event sequences and of properties holding in distinct, adjacent intervals. Interval logic suffers, however, from the same limitations as classical temporal logic, since its features for the representation of quantitative time constraints are ultimately based on the next-time operator of linear temporal logic. The work by Bernstein and Harter [5], based on the linear time temporal logic of [29] and [28], adds a real-time constraint to the operator of temporal implication, thus imposing a maximal or minimal value to the distance in time between related events, and defines an execution model and a proof system for real-time concurrent programs where properties like bounded response time or periodic behavior, besides the usual invariance and eventuality properties, can be proved. Successive work [14, 16] extended temporal logic to support specification of real-time systems. The extension adds a numeric parameter to the classical temporal logic operators, to be interpreted as a real-time constraint. For

2

instance, in this logic, the expression A Until y implies x + 10,000 > y + 10,000

4

is true in

Z but is false in [-231..231-1]1. However, if we restrict its evaluation to values of x and

y in [-231..231-10,001] then the formula holds. Clearly, the appropriate domain of evaluation depends on the particular formula to be evaluated. In the particular case of temporal assertions, consider a sentence of the type: “The communication channel must guarantee that every time a message is forwarded through it, it is delivered within 10 msecs.” Now, imagine such a channel–or a prototype–has been built and one wants to perform experiments to test whether it satisfies the requirement. In principle, you should test the channel by supplying messages at infinitely many time points to verify that, everytime, these are delivered in time. In practice, one might feel confident that, if testing behaves correctly for any experiment lasting 10 minutes, then there are no reasons to suspect that failures could occur by doing the same experiment for several hours2. However, strictly speaking, it is clear that the above sentence–which is implicitly quantified universally with respect to time–does not hold for any finite interpretation of the time domain. For example, if the domain is the integer interval [0..10,000], in terms of microseconds, it turns out that the formula is not defined for t = 9,991 even if it holds for every t in Z. Unfortunately, the formal semantics we initially defined for TRIO [10], as for most logic languages, is such that formulas of the above type have different validity whenever we change interpretation domains. As a consequence, if we use an interpreter of TRIO to validate specifications on finite execution domains approximating infinite domains, we run into the risk of considering true formulas as false and conversely. In this paper, we face the problem of defining a formal semantics for TRIO that allows the interpretation of the same formulas in different (time) domains, in a way that guarantees consistency of the different interpretations. Assigning semantics to a formalism in the case of both finite and infinite domains or structures is often more difficult than in the infinite case only. Problems similar to those arising in the case of TRIO occur in the definition of bounded Abstract Data Types [11], and in the definition of computer implementations of arithmetics. In the latter case, as we mentioned, the model of arithmetics provided by the hardware does not coincide with the model of Peano’s arithmetics. By restricting the interpretation domains of TRIO formulas subtle semantical problems can raise, because functions that are total on the unrestricted domains become partial on the restricted domains. One possible solution consists of assigning conventional truth values to the formulas. As we will see in

1 An implementation of arithmetic could be such that every overflow results into 0, which would make the assertion

false. 2Of course, the correctness of such a feeling cannot be proved!

5

Section 3.1, however, this approach inevitably leads to counterintuitive results. In our approach we provide a semantic definition that is parametric with respect to the evaluation domains, by suitably restricting the set of values to be assigned to quantified variables, in order to uniformly and consistently assign an appropriate truth value to all formulas. For instance, if we use the class or remainders modulo k as a finite approximation of infinite arithmetics, the theorem ∀x (x + 1) > x does not hold. It still holds, however, if we restrict its evaluation to a subset of the interpretation domain that does not include k - 1. In addition, our method also states the conditions under which the truth value of a formula remains unchanged when the domains used in its evaluation are restricted. Consequently, our method provides a clear statement of the conditions under which the results of a simulation performed on a domain that is the restriction of the original domain are guaranteed to reflect the behavior of the system in the original domain. The model parametric semantics defined here for TRIO, the related properties, and the interpretation algorithms are applicable to any first-order logic when its model-theoretic semantics is adopted as a base for evaluating formulas with respect to a variety of interpretation domains. The rest of the paper is organized as follows. First, the essential features of TRIO–syntax and traditional semantics–are briefly presented. This is done in Section 2 and serves the purpose of making the paper self-contained. Then, the problems arising with using different interpretation domains are precisely stated in Section 3.1. To solve such problems, a new “model parametric” semantics is given to TRIO (Section 3.2). Restriction theorems (Section 3.3) show that the new semantics properly preserves the properties holding in the original domain, when restricted to its subsets. Section 4 gives algorithms that apply interpretation schemas based on the tableaux method to the new semantics. Section 5 extends the results of [10, 9] and shows the use of TRIO for the analysis of real-time system specifications. Technical proofs of Sections 4 and 5 are given in appendices II and III, since they are rather lengthy but straightforward extensions of proofs already given in [21]. Finally, Section 6 gives concluding remarks, including directions for further extension and an outline of a specification environment based on TRIO, which is currently being developed. A complete example showing the use of TRIO in the specification of a real-time system is given in appendix I.

2. A summary of the TRIO language TRIO is a first order logical language, augmented with temporal operators that allow the specifier to express properties whose truth value may change over time. Unlike operators of conventional temporal logic, TRIO’s temporal operators provide a metric on time, since they express precisely, and quantitatively, the distance in time between events, and the length of time intervals. The meaning of a TRIO formula is not absolute, but is given with respect to a current time instant which is left implicit in the formula, in much the same way as in temporal logic.

6

2.1 Syntax: the temporal operators The alphabet of the TRIO language includes sets of names for variables, functions, and predicates, and a fixed set of basic operator symbols. Variables are divided into time dependent (TD) variables, whose value may change with time, and time independent (TI) variables, whose value is intended to be invariant with time. Every variable name has an associated type or domain, which is just the set of values the variable may assume. Among the domains there is a distinguished one, required to be numeric in nature, which is called the Temporal Domain. Every function name has an associated arity, which is a number n ≥ 0 (when n = 0 the function is called a constant), and the indication of a type for every component of the domain and for the range. Similarly, every predicate name is associated with the number and type of its arguments. Like variables, predicates are divided into time dependent and time independent ones: time independent predicates always represent the same relation, while a time dependent predicate corresponds to a possibly distinct relation at every time instant. In principle, functions may also be divided into time independent and time dependent ones, but the introduction of this feature was avoided for reasons of simplicity and naturalness of the language. The predicates 0 → Futr (A, t))

AlwP(A) SomF (A) SomP (A)

def

def

∀t (t > 0 → Past (A, t)) ¬ AlwF (¬A) ¬ AlwP (¬A)

Sometimes (A)

def

SomP (A) ∨ A ∨ SomF (A)

Always (A)

def

AlwP (A) ∧ A ∧ AlwF (A)

Lasts (A, t)

def

∀t' (0 < t' < t → Futr (A, t'))

Lasted (A, t)

def

∀t' (0 < t' < t → Past (A, t'))

Until (A1, A2)

def

∃t (t > 0 ∧ Futr (A2, t) ∧ Lasts (A1, t) )

Since (A1, A2)

def

∃t (t > 0 ∧ Past (A2, t) ∧ Lasted (A1, t) )

NextTime (A, t)

def

Futr (A, t) ∧ Lasts (¬A, t)

LastTime (A, t)

def

Past (A, t) ∧ Lasted (¬A, t)

UpToNow (A)

def

∃δ ( δ > 0 ∧ Past (A, δ) ∧ Lasted (A, δ) )

Becomes (A)

def

A ∧ UpToNow (¬A)

=

= = def = =

=

=

=

=

=

=

=

=

=

8

The intuitive meaning of these derived temporal operators stems from that of the basic Futr and Past temporal operators, according to the kind of quantification they contain. Thus, AlwF(A) means that A will hold in all future time instants; SomF(A) means that A will hold sometimes in the future; Lasts(A, t) means that A will hold for the next t time units; Until(A1, A2) means that A2 will happen in the future and A1 will be true until then; NextTime (A, t) means that the first time in the future when A will hold is t time units apart from now. The meaning of the operators AlwP, SomP, Lasted, Since, and LastTime is exactly symmetrical to that of the corresponding operators regarding the future. Sometimes(A) means that there is a time instant–in the past, now, or in the future–where A holds. Always(A) means that A holds in every time instant of the temporal domain. UpToNow (A) means that there is a non-empty time interval ending at the present time, where A has been true. Becomes (A) means that A is true now but did not hold in the most recent time instants. Notice that for the operators expressing a duration over a time interval (for example Lasts) we gave definitions where the two extremes of the specified time interval are excluded, i.e. the interval is open. Operators including either one or both of the extremes can be easily derived from the basic ones we listed above. For notational convenience, in order to indicate inclusion or exclusion of the lower or upper bound of the interval, we append to the operator’s name two subscripts, ‘i’ or ‘e’, respectively. For example, Lastsie and Sinceei are defined as follows. Lasts ie (A, t)

def

Sinceei (A1, A2)

def

=

=

Lasts (A, t) ∧ A Since (A1, A2) ∧ A1

Similarly, the formulas Until(A1,A2) and Since(A1,A2) do not admit the possibility that their second argument takes place at the current time instant; the version of these operators that includes the present time is denoted by adding a ‘p’ superscript (for ‘present’) to the operator symbol. Untilp (A1, A2) p

Since (A1, A2)

def

= def =

Until (A1, A2) ∨ A2 Since (A1, A2) ∨ A2

The so-called weak version of the operators Until and Since, which do not require their second argument to actually take place, can be defined as: UntilW (A1, A2) SinceW (A1, A2)

def

= def =

AlwF (A1) ∨ Until (A1, A2) AlwP (A1) ∨ Since (A1, A2).

It is clear that this list of derived temporal operators includes the corresponding list of classical Temporal Logic, plus others. This suggests that the TRIO language is at least as expressive as classical Temporal Logic, of which it can be considered as an extension. In fact, TRIO provides operators to express the distance between time instants and the length of intervals. The ability of the language to

9

deal with time in a quantitative manner is necessary since we wish to use it to specify properties of real-time systems, a field where classical temporal logic fails. Appendix I contains a non-trivial example intended to show how TRIO can be used to specify both the behavior and some relevant temporal properties of a system. TRIO was also used as a specification language for embedded real-time systems [9, 21], as a high level hardware description language [7], and in the description of the control of the pondage power stations of ENEL, the Italian electric energy board [22]. 2.2 Fixed domain semantics A straightforward way of defining the semantics of the TRIO language is based on the concept of a temporal structure, from which one can derive the notions of state–an assignment of values to time dependent variables and predicates–and of evaluation function, which assigns to every TRIO formula a distinct truth value for every time instant in the temporal domain. A temporal structure is denoted as S = (D, T, G, L), where • D is a set of types, that is, of variable valuation domains: D = {D1, ... Dn}. In the following, we will use the notation D(x) to indicate the evaluation domain associated with variable x. • T is the Temporal Domain: it is supposed to be a linearly ordered abelian group, thus possessing a total addition operator ‘+’ with a neutral element ‘0’ and an ordering relation ‘≤’. The subtraction operation ‘-’ and the relational operator ‘ x implies y/x > 1” we would write if x ≠ 0 then A However, when the fact that a function is defined or not for some values depends on the particular choice of the interpretation domain, it is quite uncomfortable to modify each formula according to any specific choice of the domain. Similarly, if we wish to interpret the formula ∀x (x + 1 > x) in the subsets [0..10] and [0..100], respectively of the integers, we should change it into ∀x (if x ≤ 9 then x + 1 > x) and ∀x (if x ≤ 99 then x + 1 > x), respectively. This, however, would make the whole specification activity quite awkward. What is needed is a semantics definition that allows the user to write the specification without considering the cardinality of the temporal domain, but making implicit reference to the model that he or she considers most appropriate. The semantics should be flexible enough to adjust itself to the various possible temporal structures, and would always assign a consistent and intuitive meaning to formulas of the language. The next section contains our proposal of a model parametric semantics that satisfies all such requirements. 3.2 The model parametric semantics Our approach to model parametric semantics consists of making restrictions on the evaluability of formulas implicit in the definition of the semantics with respect to the chosen domains. For simplicity we restrict our discussion to the restriction of the temporal domain. The problems due to restrictions of the interpretation domains of variables can be dealt with similarly, and will be commented upon later. We define the notion of evaluability of a formula in a structure adequate to it. If it is not possible to evaluate the formula without any reference to time points external to the temporal domain, the formula is considered to be not evaluable in that domain. In addition, for formulas containing quantifiers, the set of values that can be assigned to the quantified variables does not necessarily coincide with its

15

type, but must be suitably restricted, in order to prevent exiting the temporal domain when evaluating the formula. Thus evaluability of a formula with respect to a structure does not depend just on the types of entities that the structure assigns to the components of the TRIO alphabet–i.e. on the adequacy of the structure–but also on their values. In order to define the notion of formula evaluability, first we define Touched (F, i, S) as the set of time points touched in the evaluation of the TRIO formula F at instant i, with reference to structure S. Definition 1. The set Touched (F, i, S) is defined inductively on the structure of formula F by the following clauses: Touched (A, i, S) = {i} if A does not contain temporal operators, Touched (¬A, i, S) = Touched (A, i, S), Touched (A ∧ B, i, S) = Touched (A, i, S) ∪ Touched (B, i, S), Touched (Futr (A, t), i, S) = if i + Si (t) ∈ T then {i} ∪ Touched (A, i + Si (t), S) else {i, i + Si (t)}, Touched (Past (A, t), i, S) = if i - Si (t) ∈ T then {i} ∪ Touched (A, i - Si (t), S) else {i, i - Si (t)}, Touched (∀xA, i, S) = Touched (A, i, S). According to the last clause, the presence of quantifications in formula F does not affect the value of Touched (F, i, S): only the ξ component of the temporal structure S affects it. Example 2. Let A and B be two atomic predicates, and let us consider the formula F = ∀x Futr (A ∧ Futr (B, x + y + m), m - 1) to be evaluated at time instant 3 of a structure S1, where T = [1..10], the set of integer values from 1 to 10, and ξ1(x) = 1, ξ1(y) = 2, η13(m) = 2, and η14(m) = 1. Then Touched (∀x Futr (A ∧ Futr (B, x + y + m), m - 1), 3, S1) = Touched (Futr (A ∧ Futr (B, x + y + m), m - 1), 3, S1) = {3} ∪ Touched (A ∧ Futr (B, x + y + m), 4, S1) = {3, 4} ∪ Touched (B, 8, S1) = {3, 4, 8}. In a different structure S 2 with the same temporal domain, but where ξ2(x) = 1, ξ2(y) = 2, η23(m) = 4, and η26(m) = 3, we have

16

Touched (∀x Futr (A ∧ Futr (B, x + y + m), m - 1), 3, S2) = Touched (Futr (A ∧ Futr (B, x + y + m), m - 1), 3, S2) = {3} ∪ Touched (A ∧ Futr (B, x + y + m), 6, S2) = {3, 6} ∪ Touched (B, 12, S2) = {3, 6, 12}. The definition of Touched allows us to characterize the structures where the evaluation of a formula is possible at a given instant. In order for the evaluation of a formula to be possible in a temporal structure, the evaluation process must not touch points outside the temporal domain, that is, the set of touched points must be a subset of the temporal domain of the structure. We thus define Evaluable (F, S, i) as the predicate that establishes whether formula F is evaluable at time instant i of the temporal domain of structure S. Evaluable (F, i, S) def = Touched (F, i, S) ⊆ T. The meaning of formulas containing temporal operators can be effectively determined, at a given time instant, only if the formula is evaluable, with respect to the structure, at that instant. When the formula is not evaluable, its truth value is conventional, and could indifferently be set to true or false. Example 3. Formula F of example 2 is evaluable in structure S 1 but not in structure S2. In order to evaluate a formula F containing quantifications of TI variables, it is necessary to determine which set of tuples of the values can be substituted for variables quantified in F, thus yielding a formula that is evaluable in S at time instant i. The set of all such values for the quantified TI variables compose what we call the evaluation domain Dom (F, i, S) for F at time instant i, with respect to structure S. If x1 .. xq are the quantified TI variables of formula F, we define ~ x 1 ... x q Dom (F, i, S) def = {(a1 ... aq) ∈ D(x1) × ... × D(xq) | Evaluable (F a 1 ... a q , i, S) } For a formula F of the type ∀xA, we define the variability domain, written as Var (x, ∀xA, i, S), as the projection of Dom (∀xA, i, S) on variable x. Formally, if x, x1, .. xq are the quantified variables in ∀xA, then ~ x x 1 ... x q Var (x, ∀xA, i, S) def = {a∈D(x) | ∃a1∈D(x1), ... ∃aq∈D(xq): Evaluable(A a a 1 ... a q , i, S)} Example 4. Consider formula F = ∀x Futr (A ∧ ∃y Futr (B, x + y + m), m - 1) and a structure S where D(x) = D(y) = [1..5], T = [1..10], η3(m) = 3, η5(m) = 1. The evaluation domain of F at time instant 3 is:

17

Dom (∀x Futr (A ∧ ∃y Futr (B, x + y + m), m - 1), 3, S) = = {(a, b) ∈ D(x) × D(y) | Evaluable (Futr (A ∧ Futr (B, a + b + m), m - 1), 3, S) } = {(a, b) ∈ [1..5]2 | {3, 5, 5+1+a+b} ⊆ [1..10]} = {(1, 1), (1, 2), (1, 3), (2, 1), (2, 2), (3, 1)} The corresponding variability domains of the quantified variables x and y are Var (x, ∀x Futr (A ∧ ∃y Futr (B, x + y + m), m - 1), 3, S) = {1, 2, 3} Var (y, ∃y Futr (B, 2 + y + m), 5, S) = {1, 2} We can now provide a formal model parametric semantics for TRIO. The evaluation function S i for terms and atomic formulas is defined as in Section 2.2. Let F be a non-atomic formula such that Evaluable (F, i, S); if F = ¬A if F = A ∧ B if F = Futr (A, t) if F = Past (A, t) if F = ∀xA

then Si (F) = true iff Si (A) = false; then Si (F) = true iff Si (A) = true and Si (B) = true; then Si (F) = true iff v = Si (t) and Si+v (A) = true; then Si (F) = true iff v = Si (t) and Si-v (A) = true; then Si (F) = true iff Si (Aax) = true for all a in the set Var (x, ∀xA, i, S).

Notice that all but the last clauses are defined as in Section 2.2. In this model parametric semantics, however, the evaluation is subject to the evaluability of the formula; in particular, since the whole formula is evaluable, the evaluation of subformula A in Futr (A, t) and Past (A, t) is always possible, because time instants i+v and i-v certainly belong to the temporal domain T. Example 5. Consider the formula presented in Example 1 F = Always ( P ↔ Futr (P, 3) ) that could not be meaningfully evaluated in a finite structure, using a semantics that assumes conventional values outside a temporal domain. The formula can be rewritten in unabbreviated normal form F = (P↔Futr (P, 3)) ∧ ∀s(s>0 → Futr (P↔Futr (P, 3), s)) ∧ ∀t (t>0 → Past (P↔Futr (P, 3), t)). Assuming that variables s and t belong to [1..10], the interpretation of the formula at time instant 4 of the temporal structure of Figure 1, yields the following evaluation domain for the quantified variables Dom (F, 4, S)

= { (s, t) ∈ [1..10]2 | {4, 7, 4+s, 4+s+3, 4-t, 4-t+3} ⊆ [0..10] } = = { (s, t) ∈ [1..10]2 | 1 ≤ s ≤ 3 ∧ 1 ≤ t ≤ 4 }.

18

Such evaluation domain is shown in Figure 2. Notice that F is satisfied in the structure, because the evaluation of subformula P ↔ Futr (P, 3) is prevented at time instants that do not belong to the interval [0..7].

t 4

1

3

1

s

Figure 2. Evaluation domain for quantified variables of formula Always ( P ↔ Futr (P, 3) ).

Remark The given definition of TRIO’s semantics is parametric with respect to the temporal domain and consistently assigns a meaning to formulas in case of finite and infinite temporal domains. Problems of the same nature arise when we consider finite interpretation domains for variables and partially defined functions. As we observed earlier, for instance, if a finite subrange is associated to integer variables and to domain and range of functions, then the arithmetic functions applied to such variables may become partial, because for some values of the operands the result of function application could be out of the specified domain. The model parametric semantics introduced in this section can deal with this problem, by slightly extending the definition of evaluability of a function. Predicate Evaluable can be redefined as follows Evaluable (F, i, S) def = Touched (F, i, S) ⊆ T ∧ Defined (F, i, S) where, informally, Defined (F, i, S) is true if and only if all functions in formula F are defined on the value of the terms to which they are applied. The definitions of evaluation domain for quantified variables, and the whole model parametric semantics, which is based on the notion of evaluability, would then remain valid as given. 3.3 Properties of the model parametric semantics Model parametric semantics ensures the usual properties of first order theories. In particular, the propositional equivalences hold, among which De Morgan’s laws ¬(A ∨ B) ≡ ¬A ∧ ¬B ¬(A ∧ B) ≡ ¬A ∨ ¬B and the cancellation of double negations 19

¬¬A ≡ A. Furthermore, the following properties hold, called temporal transparency of negation: Futr (¬A, t) ≡ ¬Futr (A, t)

and

Past (¬A, t) ≡ ¬Past (A, t)

Finally, we introduce a few properties of evaluation domains. When Dom (F, i, S) = ∅ then for no ~ x1 ... xq , i, S) holds. In other words, formula ~ q-tuple (a .. a ) Evaluable(F F is not evaluable for any 1

q

a 1 ... a q

combination of values that can be assigned to TI variables that are quantified in it. In the special case of a formula without quantifications, we state by definition

Dom

 ∅ iff ¬Evaluable (F, i, S) (F, i, S) =  {()} iff Evaluable (F, i, S)

where {()} denotes the set composed of the single 0-tuple (). As a consequence of this definition, the two statements Evaluable (F, i, S),

Dom (F, i, S) ≠ ∅

and

may be considered to be equivalent. For non atomic formulas the properties stated in the following lemmas can be easily proved. Lemma 1. Dom (A ∧ B, i, S) = Dom (A, i, S) × Dom (B, i, S) where × is the Cartesian product operator among sets of tuples 1. Notice that the above property holds because A∧B is assumed to be rectified, so that the sets of quantified variables of A and B are disjoint. Lemma 2. Dom (∀xA, i, S)

= =

∪ { a } × Dom (Aax, i, S) = a∈Var(x, ∀xA, i, S) ∪ { a } × Dom (Aax, i, S) a∈D(x)

1 If H and K are sets of h-tuples and k-tuples of values, respectively, then H × K is the set of all h+k-tuples of values,

whose first h values are in a tuple of H, and the last k values are in a tuple of K. The set {()} is the unit element for this cartesian product operation.

20

where ∪ is the set union operator among sets of tuples of values. The second equality derives from the fact that Dom (Aax, i, S) = ∅ for all a∉Var(x, ∀xA, i, S) and ∅ is the unit element for the set union operation. Concerning the cardinality of the evaluation domains (in case they are finite) the following lemma holds. Lemma 3. | Dom (A ∧ B, i, S) | = | Dom (A, i, S) | ⋅ | Dom (B, i, S) | | Dom (∀xA, i, S) |

=

and

Σ |Dom (Aax, i, S) | = Σ |Dom (Aax, i, S) | a∈Var (x, ∀xA, i, S) a∈D(x)

The first of these formulas holds also for (sub)formulas without quantified variables, since |{()}| = 1, and the second equality in the second formula derives from the fact that |∅| = 0. Model parametric semantics permits to consistently assign a meaning to a formula in any temporal structure where it is evaluable, thus supporting a view of the finite temporal domain of a temporal structure as a small window on a larger, possibly infinite description of the system evolution. Accordingly, it is immediate to introduce the notion of a restriction of a structure, which considers only a subset of the set of time points that constitutes its temporal domain. It is then useful to state the conditions under which the truth value of a formula in a given structure is preserved in all of its restrictions. ^, T ^, G ^, L ^ ) is a restriction of a TRIO temporal structure S iff T ^ ⊆ T, D ^ = D, Definition 2. ^S = (D ^ = G, and i∈T ^ implies ^η = η and Π ^ =Π. G i i i i One might conjecture that, when performing a restriction on a given temporal structure, the truth value of formulas that remain evaluable in the restricted structure remains unchanged, that is, if ^S is a restriction of S, then Evaluable (F, i, S), Evaluable (F, i, ^S), and S, i F imply ^S, i F. A simple counterexample shows that this is not the case. Consider formula F = SomF (P) to be evaluated at time instant i = 7 of the temporal domain of structures S and ^S as shown in Figures 3(a) and 3(b).

21

P

a)

b)

S

^S

0

5

0

5

10

15

10

Figure 3. Evaluation of formula SomF (P) in a structure and in its restriction.

In this case, we have S, 7 F but ^S, 7 / F. The intuitive explanation of this fact is that formula SomF (P) requires P to take place sometimes in the future. The P event takes place, in structure S, at ^ of the restricted structure ^S, where F is time instant 13, that does not belong to the temporal domain T thus not verified. Definition 3. A TRIO formula is said to contain a temporal quantification iff a TI quantified variable occurs in a term that is argument of a Futr or Past operator. The temporal quantification is said to be positive (respectively, negative) in case the variable is positively (respectively negatively) quantified1. For example, the formula Sometimes (P) contains a negative temporal quantification, whilst formula Always(P) contains a positive temporal quantification. The notion of temporal quantification can be used to express precisely the conditions under which truth values of formulas are conserved under the restriction operation on temporal structures. Such conditions are stated by the following two restriction theorems. Theorem 1 (First restriction theorem). Let F be a TRIO formula without temporal quantifications, ^S a restriction of structure S, and assume that both Evaluable (F, i, S) and Evaluable (F, i, ^S) hold. Then S, i

F

if and only if

^S, i

F.

Proof: by induction on the structure of formula F. Base step: let F be an atomic formula, F = p (t1, ... tn). From the hypothesis of evaluability of F in ^S, ^ , and since ^S is a restriction of S, we have i∈Τ and i∈T Si(tj) = ^Si(tj) ∀j∈1..n, ^ , and Π = Π ^ Πi = Π i and thus S, i

p (t1, ... tn) if and only if ^S, i

p (t1 , ... tn ).

1We remind the reader that TRIO formulas are assumed to be in unabbreviated normal form.

22

Induction step (in the sequel, the symbol ‘⇔ ’ will be used to denote logical coimplication in our proof argument, and distinguish it from the TRIO coimplication sign, ‘↔ ’). ¬A ⇔ S, i / A ⇔ (by the induction hypothesis) ^S, i / A ⇔ ^S, i

1. Let F = ¬A. S, i

2. Let F = A ∧ B. S, i A∧B ⇔ S, i and ^S, i B ⇔ ^S, i A ∧ B.

A and S, i

¬A.

B ⇔ (by the induction hypothesis) ^S, i

A

3. Let F = ∀ xA. Since F does not contain temporal quantifications, Var (x, ∀ xA, i, S) = Var (x, ∀xA, i, ^S) = D(x). Thus S, i ∀xA ⇔ S, i A xa ∀aD(x) ⇔ (by the induction hypothesis) ^S, i Ax ∀a∈D(x) ⇔ ^S, i ∀xA. a

4. Let F = Futr (A, t) (the case when F = Past (A, t) is exactly symmetrical). Since ^S is a restriction of S, ^Si (t) = Si (t) (call this quantity v). Evaluable (Futr (A, t), i, ^S) implies i+v∈T^ and Evaluable (A, i+v, ^S). S, i Futr (A, t) ⇔ S, i+v A ⇔ (by the induction hypothesis) ^S, i + v A ⇔ ^S, i Futr (A, t). QED The following lemma describes a property of quantified formulas that will be used in the proof of the next restriction theorem. Lemma 4. Any TRIO formula without negative temporal quantifications is equivalent to a formula without negative temporal quantifications that does not possess any negation sign between two nested positive temporal quantifications. Proof: from the definition of positive and negative temporal quantification, it follows that any TRIO formula contains an even number of negation signs between nested quantifications of the same type (i.e. both positive or both negative). By applying the the laws of De Morgan, cancellation of double negations, and temporal transparency of negation, the lemma can easily proved. QED Example 6. Formula ∀x(Futr (C, x) ∧ ¬(Futr (¬∀zA(z)∨B, x) ∨Past (¬∀yFutr (D, x+y), x))

)

is equivalent to formula ∀x (Futr (C, x) ∧ Futr (∀zA(z) ∧ ¬B, x) ∧ Past (∀yFutr (D, x+y), x) ) that does not have any negation between nested quantifications. Figure 4 shows the structure of the two formulas, and the transformation used to eliminate the undesired negations.

23

∀x

∀x

∧

∧

Futr (., x)

¬

Futr (., x)

C

∨

C

Futr(., x)

Past(., x)

∨

¬

¬

Futr(., x)

Past(., x) ∀y

∧

∀y

B

∧

∀z

Futr(., x+y)

A(z)

D

∀z

¬

Futr(., x+y)

A(z)

B

D

Figure 4. Transformation of a formula to eliminate negations between positive quantifications.

A further restriction theorem may be proved under the assumption that formulas without negative temporal quantifications do not possess any negation sign between nested positive temporal quantifications. Theorem 2 (second restriction theorem). Let F be a TRIO formula without negative temporal quantifications, and let ^S be a restriction of structure S, with Evaluable (F, i, S) and Evaluable (F, i, ^S); then S, i

F

implies

^S, i

F.

Proof: by induction on the structure of formula F. Base step: let F be an atomic formula, that is, F = p(t1, ... tn). ^S, i quence of the facts that S, i p(t1, ... tn) and ^S is a restriction of S.

p(t1, ... tn) is a trivial conse-

Induction step. 1. Let F = ¬A. As a consequence of Lemma 4, we can assume that A does not contain temporal quantifications. Then S, i ¬A ⇒ S, i / A ⇒ (by first restriction theorem) ^S, i / A ⇒ ^S, i ¬A. 2. Let F = A ∧ B. S, i A∧B ⇒ S, i and ^S, i B ⇒ ^S, i A ∧ B.

A and S, i

24

B ⇒ (by the induction hypothesis) ^S, i

A

3. Let F = ∀xA. S, i ∀xA ⇒ S, i Aax for all a∈Var (x, ∀xA, i, S). Since ^S is a restriction of S, Var (x, ∀xA, i, ^S) ⊆ Var (x, ∀xA, i, S), i.e., it might happen that Ax is evaluable in S but not in ^S a

at time instant i, for some a∈D(x). However, by the induction hypothesis, S, i ^S, i Aax, for all a∈Var (x, ∀xA, i, ^S). Hence ^S, i ∀xA. 4. Let F = Futr (A, t) (the case when F = Past (A, t) is exactly symmetrical). S, i i+v A, with v = Si(t) = ^Si(t) ⇒ ^S, i+v A ⇒ ^S, i Futr (A, t).

Axa implies

Futr (A, t) ⇒ S, QED

Given a temporal structure S and a TRIO formula F, the set Dom (F, i, S) depends, in general, on the interpretation assigned by S to function names, and on values assigned to time dependent and time independent variables that occur in temporal terms, that is, in terms that are argument of Futr and Past. If we consider time dependent variables occurring in all temporal terms of a formula F, it is intuitively evident that Dom (F, i, S) does not depend on the values of such variables in all instants of the temporal domain, but only at those instants that are touched in the evaluation of the formula, using, for time independent variables, all values in Dom (F, i, S). This fact can be formalized by defining the set RelTDV(F, i, S) which includes all triples (TD variable, time instant, value) corresponding to the values of the set of TD variables involved in the evaluation of formula F at time instant i of structure S. Definition 4 The evaluation kernel RelTDV (F, i, S) is inductively defined as the set of TD variables relevant to the evaluation of F at time instant i of structure S: RelTDV (A, i, S) RelTDV (¬A, i, S)

def

= =

def

∅ if A does not contain temporal operators, RelTDV (A, i, S),

RelTDV (A ∧ B, i, S)

def

RelTDV (A, i, S) ∪ RelTDV (B, i, S),

RelTDV (Futr(A, t), i, S)

def

{(y, i, ηi(y)) | y TD variable in t } ∪ RelTDV (A, i+Si(t), S),

RelTDV (Past (A, t), i, S)

def

{(y, i, ηi(y)) | y TD variable in t } ∪ RelTDV (A, i-Si(t), S)

RelTDV (∀xA, i, S)

def

∪ RelTDV (Aax , i, S) a∈Var(x, ∀xA, i, S)

=

=

=

=

The following theorem proves that Dom (F, i, S) depends on the evaluation kernel, and not on the values of other TD variables, nor on values of the same variables at different time instants. Theorem 3. Let S1 and S2 be two structures with the same components D, T, Π, and Φ; let F be a closed TRIO formula, and let i∈T. If S1 and S2 provide the same evaluation kernels for F at time instant i, i.e.: RelTDV (F, i, S1) = RelTDV (F, i, S2)

25

then the corresponding evaluation domains for F, at time instant i of structures S1 and S2 are equal, i.e.: Dom (F, i, S1) = Dom (F, i, S2). Proof: by contradiction. Under the same hypotheses, the following, equivalent proposition is proved: Dom (F, i, S1) ≠ Dom (F, i, S2)

implies

RelTDV (F, i, S1) ≠ RelTDV (F, i, S2).

Assume F has q quantified TI variables x1 .. xq. Dom (F, i, S1) ≠ Dom (F, i, S2) implies that there exists a q-tuple of values (a1...aq) that is included in one of the domains but not in the other; assume, for instance, that (a1...aq)∈Dom (F, i, S1) but (a1...aq)∉Dom (F, i, S2). This implies that ~ x1 ... xq, i, S1) ⊆ T Touched (F a 1 ... a q

~ x 1 ... xq , i, S2) ⊆ T. and Touched (F / a 1 ... a q

xq Since all quantified TI variables of F have been substituted by constants to yield ~ Fxa11 ... ... a q, this for-

mula does not contain TI variables, but only TD variables. By the definition of Touched, and by the fact that S1 and S2 have the same T and Φ components, from ~ x1 ... xq, i, S1) ≠ Touched (F ~ x 1 ... x q , i, S2) Touched (F a 1 ... a q a 1 ... a q xq it follows that there exist a subformula of ~ Fxa11 ... ... a q of the form Futr (A, t) or Past (A, t) and a time

instant ~ x1 ... xq, i, S1) ∩ Touched (F ~ x 1 ... xq , i, S2) ∩ T k ∈ Touched (F a 1 ... a q a 1 ... a q such that S1k(t) ≠ S2k(t). Since t does not contain TI variables, it must contain a TD variable–call it y– that is assigned different values by S1 and S2 at time instant k; that is, η1k(y) ≠ η2k(y) must hold. From the definition of RelTDV, it follows that (y, k, η1k(y)) ∈ RelTDV (F, i, S1), while certainly (y, k, η1k(y)) ∉ RelTDV (F, i, S2). Hence RelTDV (F, i, S1) ≠ RelTDV (F, i, S2). QED Example 7. Consider formula F = Futr (A ∧ ∀x ∃y Futr (B, x + y + m), m - 1) to be evaluated at time 3 of structure S where D(x) = D(y) = [1..5], T = [1..10], η3(m) = 3, and η5(m) = 1. Then Dom (Futr (A ∧ ∀x ∃y Futr (B, x + y + m), m - 1), 3, S) = = {(a, b) ∈ [1..5]2 | {3, 5, 5+1+a+b} ⊆ [1..10]} = {(1, 1), (1, 2), (1, 3), (2, 1), (2, 2), (3, 1)} and RelTDV (Futr (A ∧ ∀x ∃y Futr (B, x + y + m), m - 1), 3, S) = {(m, 3, 3), (m, 5, 1)}.

26

In a structure S' identical to S but with η'3(m) = 3 and η'5(m) = 2, the evaluation domain for variables is Dom (F, 3, S') = {(a, b)∈[1..5]2 | {3, 5, 5+2+a+b}⊆[1..10]} = {(1, 1), (1, 2), (2, 1)} and the evaluation kernel is different: RelTDV (Futr (A ∧ ∀x ∃y Futr (B, x + y + m), m - 1), 3, S') = {(m, 3, 3), (m, 5, 2)}.

4 Verification by model construction As explained in Section 2.1, a TRIO specification can be used to model a dynamic, real-time system because the physical and structural components of the modelled system have a logical counterpart in the constituents of the temporal structure. Physical components of the systems and immutable relations among them are represented by individual constants and time independent predicates; temporary relations and events are represented by time dependent predicates; values and measures of physical quantities that are subject to change are represented by time dependent variables. Functions can be used in the description of some predefined and fixed operations of the specified system, and time independent variables are used as placeholders to express, through the use of quantifiers, existential and universal properties of the specified system. Thus, one model of a TRIO specification intuitively corresponds to one possible evolution of the specified system, that satisfies the requirements expressed by the specification formula. In order to validate requirements expressed as TRIO specifications, one may try to prove the satisfiability of the formula by constructing a model for it. In this view, some parts of the temporal structure to be constructed are assumed to be known–namely the components D, T, Π, and Φ, which describe its static configuration. Such parts, considered as a whole, are also called the frame of the temporal structure. Given a system specification as a TRIO formula and the frame of a structure adequate to its evaluation, the construction of the remaining parts of the structure determines the dynamic evolution of the modelled system: the events that take place and the values assumed by the relevant quantities. If the interpretation domains for variables and the temporal domain T are all finite, the satisfiability of a TRIO formula is a decidable problem and effective algorithms to solve it can be defined. In the following, we present an algorithm that, under the hypothesis of finite domains, determines the satisfiability of a TRIO formula with respect to a given frame, using a constructive method. Only closed TRIO formulas will be considered, since all such formulas are intended to represent system specifications, and it is well known that in formulas expressing some kind of property all variables are quantified, although sometimes implicitly. Thus, the precise formulation of the model construction problem for TRIO is as follows: given a closed TRIO formula and the frame –i.e. parts D, T, Π, and

27

Φ, of a structure adequate to it–determine whether the formula is satisfiable, at time instant i∈T, in a structure with that frame, and construct the remaining parts of the structure (i.e. ξ, ηi, and Πi). For the sake of clarity, the algorithm is divided into two parts that are presented separately. The first part is concerned with evaluability: it determines in which structures, having the given frame, the formula is evaluable, and it computes the corresponding evaluation domains. The second part is more properly concerned with satisfiability: it determines the truth value of the TRIO formula with reference to the structures defined by the first part. In Section 5 we discuss the practical application of the algorithm for deciding satisfiability of formulas in a specification support environment for real-time applications. 4.1 Construction of the evaluability tree The first part of the algorithm determines the set of possible evaluation domains for structures having the given frame. The algorithm builds a tree, called evaluability tree; every node of the evaluability tree contains a formula tree, whose nodes (the formula nodes), contain a triple of the type (F, j, asg), where F is a closed TRIO formula, asg is a set of assigments to TI variables, of the form (x, a) or to TD variables, of the form (y, k, b), with j, k∈T, a∈D(x), and b∈D(y). During the construction of the evaluability tree, the formula nodes inside evaluability nodes, and the evaluability nodes themselves, may be marked. Tree Construction Algorithm. 1 Put a formula node with (F, i, ∅) in the root node of the evaluability tree. 2 Repeat until no operation is possible: if the formula tree of an unmarked leaf of the evaluability tree contains an unmarked leaf formula node with (F, i, asg), F being a TRIO formula of the kind 2.1 ¬A: substitute ¬A with formula A; 2.2 A∧B: create two son formula nodes, with (A, i, asg) and (B, i, asg), respectively; 2.3 ∀xA: create |D(x)| formula son nodes each one with (Aax, i, {(x, a)}∪asg); 2.4 Futr(A, t): 2.4.1 if term t contains a time dependent variable y: create |D(y)| evaluability son nodes, each one with the same formula tree, but having (Futr(A, tya ), i, {(y, i, a)}∪asg) as an additional node, son of the node containing (Futr(A, t), i, asg); 2.4.2 if term t does not contain any time dependent variable: evaluate v = S(t); 2.4.2.1 if k = i + v ∈ T create a formula son node with (A, k, asg); 2.4.2.2 if k = i + v ∉ T mark the formula node; 2.5 Past (A, t): it is the symmetrical case of Futr;

28

3. repeat until no operation is possible: if in an evaluability node 3.1

all son nodes of a formula node are marked: mark that node;

3.2

at least one son of a formula node containing a formula of the kind A∧B is marked: mark that node;

3.3

a marked formula node has unmarked son nodes: mark them;

3.4

the root node of a formula tree is marked: mark the evaluability node containing it;

4 repeat until no operation is possible: mark an evaluability node if it contains conflicting assignments to TD variables in two formula nodes (i.e. it contains both (y, i, a) and (y, i, b), with a ≠ b); 5 repeat until no operation is possible: mark an evaluability node if all its son nodes are marked. The algorithm succeeds if, at termination, the root of the evaluability tree (and thus one of its leaves) is unmarked. Example 8. Figure 5 shows a portion of the evaluability tree that is built upon execution of the algorithm on the formula examined in Example 7 F = Futr (A ∧ ∀x ∃y Futr (B, x + y + m), m - 1) with respect to time instant 3 in temporal domain T = [1..10] of a frame with D(m) = [1..4], D(x) = D(y) = [1..3]. Only the structure of the evaluability tree is shown, and its nodes are represented as circles, ignoring the formula tree included in them. Assignments to the TD variables are placed close to the nodes where they first appear. For simplicity, the assignments are written as y(i) = a instead of ηi(y) = a; for instance, Figure 5 contains m(3) = 2 rather than η3(m) = 2.

m(3)=1

m(3)=2

m(3)=3

m(3)=1 m(3)=3 m(4)=1 m(4)=3 m(3)=4 m(3)=2 m(4)=2 m(4)=4

m(5)=1 m(5)=3 m(5)=2 m(5)=4

m(3)=4

m(6)=1 m(6)=3 m(6)=2 m(6)=4

Figure 5. Evaluability tree of the formula Futr (A ∧ ∀x ∃y Futr (B, x+y+m), m-1).

The rightmost three sons of the leftmost subtree are marked because they contain conflicting assignments to TD variable m, which is assigned value 1 at time instant 3 (upon creation of the leftmost

29

subtree) and given a different value for the same time instant, since expression m - 1 of the external Futr operator has value 0 and the occurrence of m in expression x + y + m refers to the same instant 3. The rightmost son of the second subtree from the right (value 3 for variable m) and the rightmost two sons of the rightmost subtree (value 4 for variable m) are marked because the root of their formula node is also marked; in fact, for those values of variable m, the evaluation domain is empty, that is, the formula is not evaluable. For instance, if m (3) = 4 and m (6) = 3 we have Touched (Futr (A ∧ ∀x ∃y Futr (B, x + y + m), m - 1), 3, S) = {3, 6, 6+3+ξ(x)+ξ(y)}, which includes a value that does not belong to [1..10], no matter which value is assigned by the structure to x and y. Figure 6 shows the formula tree contained in a descendant of the node of the tree of figure 5 corresponding to the assignments m (3) = 3 and m (5) = 2. This determines the following evaluation domain and kernel: Dom (F, 3, S) = {(a, b)∈[1..5]2 | {3, 5, 5+2+a+b}⊆[1..10]} = {(1, 1), (1, 2), (2, 1)} RelTDV (F, 3, S) = {(m, 3, 3), (m, 5, 2)}. Such evaluation domain and kernel are equal to those calculated in Example 7, for the same formula and at the same time point, with reference to structure S '.

30

Futr (A ∧ ∀ x ∃ y Futr (B, x + y + m), m - 1) i=3 ∅ m(3) = 3 A ∧ ∀ x∃ y Futr (B, x + y + m) {(m, 3, 3)} i=5

∀ x∃ y Futr (B, x + y + m) {(m, 3, 3)} i=5

A i=5 {(m, 3, 3)} x=1 ∃ y Futr (B, 1 + y + m) {(m, 3, 3), (x, 1)} i=5 y=1

y=2

y=3

x=2

x=3

∃ y Futr (B, 2 + y + m) {(m, 3, 3), (x, 2)} i=5 y=1

y=2

y=3

∃ y Futr (B, 3 + y + m) {(m, 3, 3), (x, 3)} i=5 y=1

y=2

y=3

Futr(B,2+m) Futr(B,3+m) Futr(B,4+m) Futr(B,3+m) Futr(B,4+m) Futr(B,5+m) Futr(B,4+m) Futr(B,5+m) Futr(B,6+m) {(m,3,3), {(m,3,3), {(m,3,3), {(m,3,3), {(m,3,3), {(m,3,3), {(m,3,3), {(m,3,3), {(m,3,3), (x,1),(y,1)} (x,1),(y,2)} (x,1),(y,3)} (x,2),(y,1)} (x,2),(y,2)} (x,2),(y,3)} (x,3),(y,1)} (x,3),(y,2)} (x,3),(y,3)} i=5 i=5 i=5 i=5 i=5 i=5 i=5 i=5 i=5 m(5) = 2

m(5) = 2

Futr(B, 4) {(x, 1), (m, 3, 3), (m, 5, 2), (y, 1)} i=5

Futr(B, 5) {(x, 1), (m, 3, 3), (m, 5, 2), (y, 2)} i=5

B {(x, 1), (m, 3, 3), (m, 5, 2), (y, 1)} i=9

B {(x, 1), (m, 3, 3), (m, 5, 2), (y, 2)} i = 10

m(5) = 2

m(5) = 2

m(5) = 2

m(5) = 2

m(5) = 2

m(5) = 2

m(5) = 2

Futr(B, 6) {(x, 1), (m, 3, 3), (m, 5, 2), (y, 3)} i=5

Futr(B, 5) {(x, 2), (m, 3, 3), (m, 5, 2), (y, 1)} i=5

Futr(B, 6) {(x, 2), (m, 3, 3), (m, 5, 2), (y, 2)} i=5

Futr(B, 7) {(x, 2), (m, 3, 3), (m, 5, 2), (y, 3)} i=5

Futr(B, 6) {(x, 3), (m, 3, 3), (m, 5, 2), (y, 1)} i=5

Futr(B, 7) {(x, 3), (m, 3, 3), (m, 5, 2), (y, 2)} i=5

Futr(B, 8) {(x, 3), (m, 3, 3), (m, 5, 2), (y, 3)} i=5

B {(x, 2), (m, 3, 3), (m, 5, 2), (y, 1)} i = 10

Figure 6. Formula tree.

The tuples of Dom (F, 3, S), which describe legal assignments to variables x and y, can be immediately determined from the assignments to TI variables included in unmarked leaf nodes of the formula tree. Similarly, the evaluation kernel RelTDV(F, 3, S) is determined by the assignments to TD variables that uniquely identify the evaluability leaf. Note that the rightmost subtree is completely marked: the marking has been propagated on the whole subtree, starting from leaves containing Futr (B, 6), Futr (B, 7), and Futr (B, 8), by execution of step 3.1 of the algorithm.

31

4.2 Construction of the tableaux tree The second part of the algorithm for deciding satisfiability attempts to build a model for the formula, using the evaluation kernels and domains determined by the Tree Construction Algorithm presented in Section 4.1. It is based on a method similar to that of semantic tableaux [32]. The algorithm builds a tree, whose nodes are tableaux containing a set of elements of the form (A, j, p), where A is a subformula of F, with variables possibly substituted by their values, j∈T, and p is (a reference to) a formula node in an unmarked evaluability leaf node. Semantic Tableaux Algorithm. The following steps are repeated with reference to every unmarked leaf node of the evaluability tree. 1. Put (F, i, p) in the root node, where p points to the root node of the formula tree inside the evaluability leaf node. Also, put in the root all assignments to TD variables contained in unmarked formula nodes of the evaluability leaf node; 2. repeat until no operation is possible: if a leaf tableau contains a triple (G, i, p) with G of type 2.1. ¬¬A: create a son tableau with (A, i, p) in place of (¬¬A, i, p); 2.2. A∧B: create a son tableau with (A, i, pA) and (B, i, pB), where pA is the formula node, son of node p, that contains A, and similarly pB is the node containing B; 2.3. ¬(A∧B): create two son tableaux with (¬A, i, pA) and (¬B, i, pB), where pA and pB are defined as above; 2.4. ∀xA: create a son with as many (Aax, i, pa) as there are distinct a∈D(x) for which node p has an unmarked son pa containing Aax ; 2.5. ¬∀xA: create as many sons, each one containing (¬Aax, i, pa), as there are distinct a∈D(x) for which node p has an unmarked son pa containing Aax ; 2.6. Futr(A, t) 2.6.1 if term t contains a TD variable y: create a son with (Futr(A, tya ), i, pf), where (y, i, a) is an assignment to variable y contained in the tableau, and pf is the (only) son node of node p; 2.6.2. if term t does not contain TD variables: let v = S(t) and k = i + v, create a son node with (A, k, pf), where pf is defined as above; 2.7

similarly for ¬Futr(A, t);

2.8

symmetrically for Past;

32

3. repeat until no operation is possible: if a leaf node contains a triple (L(y), i, p) with a literal L(y) where a TD variable y occurs, then create |D(y)| son nodes, each containing (Lya, i, p) and (y, i, a), for a different a∈D(y); 4. evaluate all terms contained in literals inside leaf nodes and substitute such terms with their values, so that only ground terms remain; 5. repeat until no operation is possible: if a leaf tableau contains (y, i, a) and (y, i, b) with a ≠ b, mark it; 6. repeat until no operation is possible: mark an unmarked tableau if it contains 6.1. p(v1 ..vn), p being a time independent predicate and (v1 .. vn)∉Π(p), or ¬p(v1 .. vn) with (v 1 .. v n )∈Π(p), or 6.2. both (q(v1 .. vm), i, p') and (¬q(v1 .. vm), i, p"), with q a time dependent predicate; 7. repeat until no operation is possible: mark a tableau if all its sons are marked. The tableaux algorithm succeeds if the construction of the tableaux tree does not mark its root for at least one of the unmarked evaluability leaves taken as parameter of the construction. Example 9. Figure 7 shows the tableaux tree that is built with reference to the evaluability node containing the formula tree of Figure 6. For simplicity, we omitted the reference to the formula node that, according to the algorithm, should be included in every element of the tableaux. Thus instead of triples of type (F, i, p), Figure 7 uses pairs (F, i). Moreover, assignments to TD variables, corresponding to the evaluation kernel with respect to which the tree construction is performed, are shown in a separate table. As a side remark, this is precisely how this information would be treated in an efficient implementation of the algorithm: the evaluation kernel need not be duplicated at every expansion step of the tableaux algorithm, since it can be considered as a read-only parameter of the construction process.

33

( Futr (A ∧∀ x ∃ y Futr (B, x + y + m), m - 1), 3)

m(3)=3 m(5)=2

( A ∧ ∀ x∃ y Futr (B, x + y + m), 5)

( ∀ x ∃ y Futr (B, x + y + m), 5) (A, 5)

(¬∀ y ¬Futr (B, 1 + y + m), 5) (¬ ∀y ¬Futr (B, 2 + y + m), 5) (A, 5)

(¬¬Futr (B, 1 + 1 + m), 5) (¬ ∀y ¬Futr (B, 2 + y + m), 5) (A, 5)

(¬¬Futr (B, 1 + 2 + m), 5) (¬ ∀y ¬Futr (B, 2 + y + m), 5) (A, 5)

(¬¬Futr (B, 1 + 1 + m), 5) (¬¬Futr (B, 2 + 1 + m), 5) (A, 5)

(¬¬Futr (B, 1 + 2 + m), 5) (¬¬Futr (B, 2 + 1 + m), 5) (A, 5)

(Futr (B, 2 + m), 5) (Futr (B, 3 + m), 5) (A, 5)

(Futr (B, 3 + m), 5) (Futr (B, 3 + m), 5) (A, 5)

(B, 9) (B, 10) (A, 5)

(B, 10) (A, 5)

Figure 7. Tableaux tree.

Notice that the expansion of formula ∀x∃yFutr (B, x+y+m) produces two elements in the same tableau, since |Var (x,∀x ∃y Futr (B,x+y+m), 5, S)| = 2, and the quantification of variable x is positive; instead, two tableaux are created for the expansion of formula ∃yFutr(B, 1+y+m), because |Var (y, ∃yFutr (B, 1+y+m), 5, S)| = 2 and the quantification is negative. The following theorem states the correctness of the Semantic Tableaux Algorithm.

34

Theorem 4. Given a closed TRIO formula F and a structure S adequate to it with a frame D, T, Φ, and Π, then F is satisfiable in S at an instant i∈T if and only if the Semantic Tableaux Algorithm terminates successfully for at least one of the unmarked leaf nodes of the evaluability tree. The proof of the above theorem is postponed to Appendix II, since it is a natural extension of the proof provided in [21] for the original TRIO semantics. The tableaux algorithm provides an effective way to establish whether a TRIO specification is finitely satisfiable. Thus it can be used to provide some degree of executability to the TRIO formalism, and based on it suitable automatic tools for specification testing, system simulation, and mechanical proof of properties can be constructed. For instance, the consistency of a specification can be verified through the Semantic Tableaux Algorithm by showing that the corresponding formula is satisfiable. In addition, since a TRIO formula is valid if and only if its negation is not satisfiable, the algorithm can be used to prove that a given formula is valid. For instance, any property Π of the specified system can be proved to be a consequence of its specification Σ, by showing that the implication Σ→Π is a valid formula.

5 Temporal properties of specifications In the following some definitions and theorems regarding the characterization of temporal properties by means of TRIO formulas will be briefly presented. Similar concepts were previously introduced in [9], with reference to the TRIO semantics discussed in Section 3.1 of this paper. For this reason the results are given concisely, and the proofs are be left to the appendices. 5.1 Temporal closure and invariance A fundamental concept in first order theories is the quantification of variables, which provides a form of generalization: the properties expressed by a closed formula are intended to hold independent of the particular value associated by the interpretation to the quantified variables. The corresponding notion in the temporal framework would require a TRIO formula to be satisfied (or dissatisfied) independent of the time instant in which it is evaluated. A basic property of the TRIO language is that the current time instant–the instant where each (sub)formula is evaluated–is left implicit. For this reason, the notion of quantification over the instant of interpretation is not included directly in the language, but is introduced by the following definition of temporal closure. Definition 5. A TRIO formula is temporally closed if it satisfies one of the following conditions: i) it is an atomic formula applied to terms containing only constants and time independent variables, or ii) it has the form Sometimes (A) or Always (A), where A is any TRIO formula, or

35

iii) it derives from the propositional combination of temporally closed formulas, that is, it has the form ¬A or A∧B, A and B being temporally closed formulas. The following definition captures the concept of a formula whose truth value does not depend on the time instant in which it is evaluated. Definition 6. A TRIO formula F is temporally invariant if, in all structures S adequate to it and in all time instants such that Evaluable (F, i, S), S, i

F implies S, j

F for all j such that Evaluable (F, j, S).

The fact that the syntactic definition of temporally closed formula adequately captures the semantic notion of temporal invariance is expressed by the following theorem, whose proof is reported in Appendix III. Theorem 5. Every temporally closed TRIO formula is temporally invariant. A temporally closed formula does not necessarily have all TI variables quantified. For this reason we distinguish between the above notion of temporal closure and the property of having all TI variables quantified, called classical closure. A TRIO specification is intended to describe properties that do not refer to some absolute time instant, but are invariant with time. For similar reasons it was argued in Section 4 that a TRIO specification of a system must be a classically closed formula. Hence, we define a TRIO specification to be any closed (both classically and temporally) TRIO formula. 5.2 Histories, history completeness, and compatibility. In this section, we discuss how TRIO specifications may be formally validated by means of testing execution traces and simulating system behavior, given the initial condition(s) and external stimuli. To do so, we first show how to represent the evolution of the specified system using TRIO. Definition 7. A history (or evolution trace) is a closed TRIO formula of the kind: Sometimes (

∧i Futr (Fi, ti) ∧ ∧j Past (Pj, tj))

where all of the Fi and Pj are atomic formulas of the type • time dependent predicates p(t1, ... tn) applied to terms without variables, or • time independent predicates of the form y = t, where y is a time dependent variable, and t is a term without variables and all temporal arguments ti and tj of the Futr and Past operators can be evaluated to constants.

36

Intuitively, a history describes a sequence of events that are in a precise temporal relation with each other, but whose absolute occurrence time is not specified. This notion of independence of a sequence of events from their absolute occurrence times can be characterized in terms of the tableaux generated by the algorithms of Section 4 for constructive verification of the satisfiability of TRIO formulas. It can be easily shown that the literals for time dependent predicates and the assignments to time dependent variables included in an unmarked tableau upon successful termination of the tableaux algorithm do not completely determine a unique model for the formula, but implicitly characterize a set of models. For each model of such a set, if q is a time dependent predicate, then (v1..vn)∈Πi(q) if the triple (q(v 1 ..v n ), i, p') is included in the tableau, while (v 1 ..v n )∉ Π i (q) if the triple (¬q(v 1 ..v n ), i, p") appears in it; also, η i (y) = a if the triple (y, i, a) is present. However, for every n-tuple (v1..vn) and every instant i∈T such that neither (q(v1..vn), i, p') nor (¬q(v1..vn), i, p") have been produced, the value assigned to the tuple by the structure is immaterial to the satisfiability of the formula: both the models that include the tuple (v1..vn) in relation Πi(q) (the relation associated by the model to predicate q at time instant i), and those that do not include it, satisfy the formula. Similarly, the value of a time dependent variable y at time instant i∈T does not determine the satisfiability of the initial formula if no triple of the form (y, i, a) appears in the tableau. This property can be used to formally characterize the fact that two tableaux abstractly represent models containing the same significant events, but translated by a fixed time distance of the temporal axis, through the notion of superimposable tableaux. Definition 8. Two unmarked tableaux Ξ1 and Ξ2, generated by the same execution of the tableaux algorithm, are said to be superimposable if and only if there exists a number r1 such that, for every time instant i∈T and time dependent predicate q, ( q (v1 .. vn), i, p') ∈ Ξ1

if and only if

( q (v1 .. vn), i + r, p') ∈ Ξ2

and, for every time dependent variable y and every value a∈D(y), (y, i, a) ∈ Ξ1 if and only if

(y, i + r, a) ∈ Ξ2.

The superimposability relation defined above is an equivalence relation; thus, two superimposable tableaux can be considered to actually represent the same model. The following theorem establishes that there actually exists only one model for every history, up to equivalence by superimposability. Its proof is reported in Appendix III.

1 The precise nature of number r in the above definition depends on the nature of the temporal domain. For instance, if

the temporal domain is an integer interval [h..k], number r will be an integer value whose absolute value is in range [1..|k-h|].

37

Theorem 6. The tableaux produced through verification of a history by execution of the tableaux algorithm are all superimposable to each other. Since a history describes one possible evolution of a specified system, the question naturally arises whether the behavior described by the history is consistent or not with the specification. Besides the two obvious answers to such question (yes or no), a third possibility arises: the events described by a history are not in contrast with the specification, but are not sufficient to verify it. That is, the history can become a model of the specification if some more facts are added to it. These intuitive concepts are formally captured by the following definitions. Definition 9. Given a history H and a TRIO specification Σ, the formula H ∧ Σ, resulting from the conjunction of the history with the specification, is called a Σ_specified history, written HΣ. HΣ describes a sequence of events and states that the sequence is compatible with the specification Σ. Being the conjunction of two closed formulas, a Σ_specified history is a closed formula too, and its satisfiability can be verified by means of the tableaux algorithm. Definition 10. A history H is said to be Σ _complete if and only if, by the executing the tableaux algorithm with formula HΣ, it is possible to construct at least one tableau that is superimposable to those of H. H is said to be Σ_incomplete if and only if, by executing the tableaux algorithm, only tableaux that are supersets of those of H can be obtained. H is Σ_compatible if it is either Σ_complete or Σ_incomplete. H is Σ_incompatible if HΣ cannot be satisfied, i.e. the tableaux algorithm fails on it. We point out that the notions of Σ_completeness and Σ_compatibility provide a formal basis to the validation activities on TRIO specifications. In fact, checking Σ_completeness and Σ_compatibility of histories correspond to two familiar operations performed by the system specifier: testing the specification against the trace of a possible evolution of the system, and simulating the behavior of the specified system under given stimuli.

6 Conclusions We presented TRIO, a logic formalism for specifying real-time systems, together with a model theoretic semantics that refers to unbounded temporal domains and total functions. It was shown that the use of the language in a specification environment supporting testing and validation activities requires the possibility of consistently assigning a meaning to the formulas of the language with reference to finite temporal domains, e.g. integer intervals, which can be considered as windows providing a focused picture of the possibly infinite evolution of the specified system. Then, we provided a solution to the problem, in terms of a new, model parametric semantics for the language, that can adjust to a variety of underlying temporal domains. Properties of such semantics have been characterized; in par-

38

ticular we stated the conditions under which a formula that is satisfied in a given temporal structure still holds in its restrictions. We also defined a tableaux-based algorithm for deciding, in case of finite domains, the satisfiability of TRIO formulas; such an algorithm can be the kernel of a set of tools supporting testing, simulation, and prototyping of the specifications. Relevant temporal properties of specifications, such as temporal closure and invariance, and the notions of compatibility and completeness of the history of a system with respect to its specification, were restated in terms of the model parametric semantics. We also discussed, and critically evaluated, other approaches to solving the problem of finite temporal structures, such as assignment of default truth values or the use of many valued logic, where an undefined logic value is used when expressions are evaluated outside the given finite domains. All such approaches have been shown to be inadequate. We are currently extending our research in two complementary directions. One theoretical direction explores issues such as complexity of the algorithms and the possibility of handling different time scales–such as hours and seconds–in the specifications. The other direction concerns the development of a specification support environment for TRIO. These two directions are clearly related. The actual usefulness of a tool for, say, testing the specification depends on the efficiency of the algorithm that implements it, and the flexibility and expressiveness of TRIO as a specification language can be greatly enhanced by allowing the specifier to refer to different time scales inside the same formulas, or by providing consistent ways of interpreting the same specification formula on temporal domains with different time granularities. With reference to complexity issues, we point out that the algorithm given in Section 4.2 provides a solution to the problem of model construction. The results of Section 5, however, suggest that such an algorithm can be specialized to solve the much simpler problem of checking the completeness of a history, or the problem of completing an incomplete, but compatible, history, whose complexity is intermediate between model checking and model generation. Thus it can be reasonably expected that there is a tradeoff between generality and efficiency, so that fast algorithms exist for checking a complete history, whereas the completion of a history can be performed with an efficiency that depends on to the amount of missing information (in terms of events and values of variables) to be generated. On the other hand, the operation of model generation, which, as shown in Section 4.2, supports the proof of properties of the specified system, is computationally expensive. A prototype TRIO interpreter has been developed at the Dipartimento di Elettronica of Politecnico di Milano. Actually, the interpreter is based on two distinct tools: one component verifies the finite satisfiability of TRIO formulas and performs completion of histories; another component, called history checker, can determine with significantly greater efficiency the completeness of a history with respect to a given specification. The history checker has been successfully employed to validate TRIO 39

specifications of real-life systems, like those in [7] and [22], thus demonstrating the feasibility of the approach. Acknowledgements We thank Ernani Crivelli, Elena Ratto, Marco Roncato, and Luigi Zoccolante for many stimulating discussions on the use of TRIO in the specification of real-time systems, and on the features of TRIO-based tools apt to supporting the specification activity. The referees have also provided numerous valuable suggestions and corrections.

Appendix I In the following, we give a TRIO specification of two crossing roads, with semaphores, car arrival and departure, and queues of waiting cars. The example is inspired by a similar one presented in [8]. For readability reasons, formal TRIO specification are intermixed with informal English descriptions. Traffic lights control the intersection of two one way crossing roads. One is a lightly used side road, so that normally the semaphore is green for the main road and red for the side road. The semaphore turns green for the side road upon request, and only if the semaphore on the main road has been green for at least 180 seconds. The green on the side road lasts exactly 30 seconds. For simplicity, we omit modelling the yellow color on both semaphores, and we do not distinguish one car from another; we are only interested in modeling car arrival and departure from the crossing, the changes of color of the semaphores, and the length of the queues at different time instants. The alphabet of the TRIO specification for the crossing includes the following TD predicates and variables: enterSide, exitSide enterMain, exitMain turnsSideGreen, turnsSideRed turnsMainGreen, turnsMainRed sideLine, mainLine

predicates denoting car arrivals and departures on the side road; predicates denoting car arrivals end departures on the main road; predicates denoting changes in the color of the side semaphore; predicates denoting changes in the color of the main semaphore; variables denoting the length of the queues at the side and main roads (their value belongs to N, the set of naturals);

sideSem, mainSem

variables denoting the current color of semaphores (their value belongs to {red, green}).

The relevant properties of the two road crossing system are specified by the following TRIO formulas. The colors of the semaphores are not independent:

40

mainSem = green ↔ sideSem = red ∧ mainSem = red ↔ sideSem = green ∧ turnsSideGreen ↔ turnsMainRed ∧ turnsSideRed ↔ turnsMainGreen.

F1:

The green light lasts exactly 30 seconds on the side road: F2:

turnsSideGreen ↔ NextTime (turnsSideRed, 30)

(a corresponding equation for the main road is not needed since the colors are not independent). The color of semaphores changes only as a consequence of the events of the kind turns(Side/Main)(Red/Green). F3:

sideSem=green ↔ Sinceeip (¬turnsSideRed, turnsSideGreen)

F4:

sideSem = red ↔ SinceWeip (¬turnsSideGreen, turnsSideRed)

def where SinceWeip (B, A) = (AlwP(B) ∧ B) ∨ Sinceeip (B, A). Notice that the color of the semaphore is

assumed to change in the same instant when the event that causes it takes place, i.e. turnsMainGreen implies mainSem = green. The two equations above introduce an asymmetry that is in the nature of the represented system: they imply that red is the default color for the side semaphore. The next rule describes the conditions under which the side semaphore turns to green. When a car reaches the crossing point coming from the side road and the semaphore is red, its arrival is detected, and after ∆tt seconds (time elapsing for color turn) the light turns green. More precisely, this happens if the queue is empty when the car arrives and the side semaphore has been red for at least 180 seconds. Otherwise, i.e. if the car arrives when less than 180 seconds elapsed since the semaphore turned to red, the count-down of ∆tt seconds starts after all the 180 seconds have elapsed with the side semaphore red. This also happens in case the semaphore turns to red with a nonempty car queue. F5: turnsSideGreen ↔ Becomes (Lasted (sideLine > 0, ∆tt) ∧ Lasted (sideSem = red, 180 + ∆tt)) When the semaphore is green and the queue is not empty, the cars cross the side road, one every ∆tc time units (∆tc represents the time needed for crossing). A car crosses the road if and only if the semaphore is green and: • •

the car arrived at the current time instant and the queue is empty, or the light turned to green ∆tc seconds before the current time, and the queue was not empty (we assume ∆tc « 30 sec.), or

41

•

a car crossed the road ∆tc seconds before the current time, and the queue did not become empty (we assume that the effect of a crossing on the queue is instantaneous, that is, the queue length is immediately decremented by one).

F6:

exitSide ↔ sideSem = green ∧ ( enterSide ∧ UpToNow (sideLine = 0) ∨ ∨ Past (turnsSideGreen ∧ sideLine > 0, ∆tc ) ∨ ∨ Past (exitSide ∧ sideLine > 0, ∆tc) )

Observe that a car may enter the crossing point (enterSide) in the same instant when the last car of a pre-existing queue exits (exitSide). In this case, according to the first disjunct of the previous formula, the car does not cross the road at the same instant because the queue was not empty in the last preceding instants, as required by the subformula UpToNow (sideLine = 0). Similarly, Formula F 7 models the crossing of the main road. F7:

exitMain ↔ mainSem = green ∧ ( enterMain ∧ UpToNow (mainLine = 0) ∨ ∨ Past (turnsMainGreen ∧ mainLine > 0, ∆tc ) ∨ ∨ Past (exitMain ∧ mainLine > 0, ∆tc) )

The following formulas model changes in the queue length. The queue is empty if no car ever arrived with the red semaphore, or if no car arrived with a red light since the last time a car crossed leaving an empty queue, that is with the queue of length one up to that time instant. F8:

sideLine = 0 ↔ SinceWeip ( ¬(enterSide ∧ sideSem = red), exitSide ∧ ∧ ¬enterSide ∧ UpToNow (sideLine = 1) )

The length of the queue is incremented by 1 when a car enters and no car exits; it is decremented by 1 when a car exits but no car enters. F9: ∀ln ( ln > 0 ∧ sideLine = ln ↔ UpToNow (sideLine = ln - 1) ∧ enterSide ∧ ¬exitSide ∨ ∨ UpToNow (sideLine = ln + 1) ∧ exitSide ∧ ¬enterSide ∨ ∨ Sinceeip ( ¬ (enterSide ⊕ exitSide), Becomes (sideLine = ln ) ) ) For the main road, two rules F 10 and F11 apply, similar to F8 and F9 but with "main" in place of "side". The specification of the whole road crossing system requires properties expressed by formulas F1÷F11 to hold simultaneously and at all time instants, and thus corresponds to the following TRIO formula

42

Always ( ∧i Fi ) The TRIO language can be used to express not only the behavior of the specified system, but also its desirable properties, and to state under which conditions these may be guaranteed. For instance, in case of limitations on the incoming traffic on the side road, the length of the queue will not diverge, and one should be able to prove that the following formula is implied by the above specification: Always ( ∀t (enterSide ∧ Futr (enterSide, t) → t ≥ 14 ) ) → ∃ le Always (sideLine < le ).

Appendix II This appendix provides a proof of Theorem 4. The proof is divided into two lemmas, corresponding to the two main steps of the algorithm: construction of the evaluability tree and of the tableaux tree. The purpose of the construction of the evaluability tree is to obtain the evaluation kernels and domains of all structures, with the given frame, where formula F is evaluable at time instant i. To do so, we first define the set of assignments to time dependent and time independent variables that can be associated to the unmarked evaluability leaf nodes; then we prove that they are respectively equal to the evaluation kernels and domains of all structures where the formula is evaluable. Let x1..xn be the TI variables of the initial formula F, closed by hypothesis. To every evaluability leaf node ne we associate a subset of D(x1) × .. × D(xn), and call it Dom (ne); it will be shown that this set coincides with Dom (F, i, S), for suitable structures S. The set Dom (ne) can be defined "bottom up", starting from the contents of the leaves of the formula tree contained in n e. Initially, a set Dom (nf) is assigned to every node nf of the formula tree, and then Dom(ne) is defined as Dom (nr), nr being the root node of the formula tree in ne. Definition 11. The set Dom (nf) associated to a formula node is defined according to the following inductive rules. 1. If nf is a marked leaf node, Dom (nf) = ∅; if it is an unmarked leaf, let (A, i, asg) be the triple contained in it. The set of TI variables that are assigned a value in asg is composed exactly of all TI variables being argument of quantifiers whose scope includes, in the original formula F, the atomic formula A. Dom (nf) is then defined as the singleton set composed of the tuple of values assigned by asg to such TI variables. 2. If a formula node nf contains a formula of the form A∧B, then the node has two sons, call them nA and nB, which contain formulas A and B, respectively. Let x1..xc be the TI variables that are the arguments of quantifiers whose scope, in the original formula F, includes formula A∧B; let xc+1..xd be the variables that are the arguments of quantifiers in formula A, and let x d+1..xe be the variables that are argument of quantifiers in formula B. Then

43

Dom(nf) def = {(a1..acac+1..adad+1..ae) | ∃dA∈Dom(nA), ∃dB∈Dom(nB) such that a1..ac is the value assigned to x1..xc by dA and dB ac+1..ad is the value assigned to xc+1..xd by dA ad+1..ae is the value assigned to xd+1..xe by dB } Since dA and dB agree on assignments to variables x1...xc, whose values a1...ac are “inherited” because their quantification is global with respect to formula A∧B, the cardinality of the resulting domain is equal to the product of the cardinalities of the domains associated to the son nodes: | Dom (nf) | = | Dom (nA) | ⋅ | Dom (nB) |. Notice that these rules are defined if nodes nA and nB are both unmarked. If one of the two is marked, nf is marked too, and Dom (nf) = ∅. 3. If nf contains a formula of the type ∀xA , then it has |D(x)| sons, of which u are unmarked; each of them contains the formula Aaxi with ai∈D(x), for i∈1..u. We then define (remind that an empty set is associated to each marked node) Dom (nf) def ∪ Dom (ni) = ∀i∈1..|D(x)| ∪ Dom (ni) = ∀i∈1..u The domains Dom (ni) associated with distinct unmarked sons are pairwise disjoint, because they differ in the value assigned to variable x; thus | Dom (nf) | =

Σ

i∈1..u

|Dom (ni) |.

4. Every node nf containing a formula of the type Futr (A, t), where t may or may not contain TD variables, certainly has only one formula son node, call it ns; in this case we define Dom (nf) = Dom (ns) Every unmarked evaluability leaf node is associated with a set of values for TI variables of the original formula F, equal to the domain associated (according to the above introduced rules) to the root of the formula tree contained in the evaluability leaf. Similarly, each evaluability leaf ne is associated with a set of assignments to TD variables, called RelTDV (ne), which is also inductively defined in a “bottom up” way, starting from the formula tree included in the node. Again, for a generic formula node n f, we call RelTDV(nf) the set of TD assignments associated with such node. For the evaluability node that contains the formula tree the associated set of TD assignments is equal to that of the root of the formula tree.

44

Definition 12. The set RelTDV(nf) associated with a formula node is defined according to the following inductive rules. 1. If node nf is a leaf node and is marked, then RelTDV(nf) = ∅; if it is unmarked, let (A, i, asg) be the triple contained in it. We define RelTDV(nf) def = { (y, i, a) | (y, i, a) ∈ asg }. that is, RelTDV (nf) contains the set of TD assignments associated with the formula node. 2. If nf contains a formula of type A∧B and has two son nodes nA and nB, containing A and B respectively, we define RelTDV(nf) def = RelTDV (nA) ∪ RelTDV (nB). 3. If nf contains a formula of the type ∀xA, then it has |D(x)| son nodes, u of which are unmarked. We define RelTDV(nf) def =

∪

∀i∈1..|D(x)|

RelTDV (ni) =

∪

∀i∈1..u

RelTDV (ni).

4. If nf contains a formula of the type Futr (A, t), then it has a unique son ns, and we define RelTDV (nf) def = RelTDV (ns). Finally, every unmarked evaluability leaf node is associated with the set of assignments to TD variables of the original formula F, that is associated (according to the above introduced rules) with the root of the formula tree contained in the evaluability leaf. Remark If ne is an unmarked evaluability leaf node, RelTDV (ne) coincides with the set of assignments to TD variables that are contained in its unmarked formula leaf node, and thus the assignments included in the root tableau by step 1 of the tableaux algorithm, taking ne as a parameter, are the same as those of RelTDV (ne). The correctness of the construction of the evaluability tree is stated by the following lemma. Lemma 5. Given a frame, i.e. parts D, T, Φ, and Π of a temporal structure, a closed TRIO formula F, and a time instant i∈T, the execution of the algorithm for the construction of the evaluability tree, starting with (F, i, ∅) in the root node, produces in the unmarked leaf nodes exactly all the evaluation kernels and domains of all structures S, having that frame, such that Evaluable (F, i, S). That is:

45

a) if there exists a structure S, with the given frame, where Evaluable (F, i, S), then the construction of the evaluability tree produces an unmarked leaf node n e such that RelTDV (ne) = RelTDV (F, i, S), and Dom (ne) = Dom (F, i, S); b) if the execution of the algorithm produces an unmarked leaf node ne then all structures S that provide the assignments to TD variables included in RelTDV (ne) are such that Evaluable (F, i, S), RelTDV (F, i, S) = RelTDV (ne ), and Dom (F, i, S) = Dom (n e ). We first prove part a) of the lemma. The proof is by induction on the structure of formula F. Base: Let F = A (t1 ...t n ). Then F is evaluable in any structure S adequate to it and RelTDV (F, i, S) = ∅ because the formula does not include temporal operators. Dom (F, i, S) = {()}, since the formula is closed by hypothesis. The execution of the algorithm terminates immediately, with Dom (ne) = {()} and RelTDV (ne) = ∅. Inductive step. 1. Let F = ¬A. The evaluability algorithm substitutes formula ¬A with formula A. The proof follows form the inductive hypothesis and from the fact that, for every structure S, RelTDV(¬A,i,S) = RelTDV (A, i, S), and Dom (¬A, i, S) = Dom (A, i, S). 2. Let F = A∧B. The algorithm generates, from formula node n A∧B containing F, two son formula nodes, nA and nB, that contain A and B. These two sons are then expanded independently, except for the consistency checks of step 4 of the algorithm. If Evaluable (A∧ B, i, S) then Evaluable (A, i, S) and Evaluable (B, i, S). By the inductive hypothesis, executing the algorithm with formula A yields an evaluability leaf node, containing RelTDV (A, i, S) and Dom (B, i, S), whereas for formula B an evaluability leaf node would be obtained, containing RelTDV (B, i, S) and Dom (B, i, S). In case the execution starts with A∧B in the root node nA∧B, since nA and nB are expanded independently, in the evaluability leaf nodes we obtain all combinations of the subtrees that can be obtained from nA and nB. In particular, one of the resulting nodes will contain RelTDV (nA∧B) = RelTDV (nA) ∪ RelTDV (nB) (ind=hp) RelTDV (A, i, S) ∪ RelTDV (B, i, S) = (by definition 4) RelTDV (A∧B, i, S), and similarly Dom (nA∧B) = Dom (nA ) × Dom (nB) = 1 (ind hp) Dom (A, i, S) × Dom (B, i, S) = (by Lemma 1) Dom (A∧B, i, S) .

1 Here and in the sequel we use the notation = (ind hp) to indicate an equality that can be justified by invoking the

induction hypothesis.

46

3. Let F = ∀xA. The evaluability algorithm generates, from formula node n ∀ containing formula ∀xA, |D(x)| son formula nodes containing (Aax , i, {(x, a)} ∪ asg). Let us call na the son node containing Aax . If there exists structure S such that Evaluable (∀ xA, i, S), then V a r ( x , ∀ x A , i , S ) ≠ ∅ . By the induction hypothesis, for each of the values a∈Var(x, ∀xA, i, S) the algorithm, executed starting from A xa , would terminate successfully, that is, with an unmarked evaluability leaf node. Thus, for all values a∈Var (x, ∀xA, i, S), node na is not marked, and the algorithm terminates successfully. Moreover, from the induction hypothesis, it follows that for a certain value a, if node na is marked then a∉Var(x, ∀xA, i, S): in fact, if a∈Var(x, ∀xA, i, S), then node na would not be marked. Thus it is proved that the set of values a∈D(x) for which node na is not marked corresponds exactly to Var (x, ∀xA, i, S). By the induction hypothesis, executing the algorithm with only Aax (with a∈Var(x, ∀xA, i, S) ) an evaluability leaf node is obtained, that contains RelTDV (Aax , i, S) and Dom (Aax , i, S). In this case, however, the son nodes na are expanded starting from a set of assignments that is not empty, because it already contains assignment (x, a); thus at the end of the execution {(a)}× Dom(Aax ,i, S) is associated to node na, not simply Dom (Aax , i, S). Dom (n ∀ ) =

∪ {(a)} × a∈Var(x, ∀xA, i, S)

Dom (Aax, i, S) is thus associated to node n∀ ; but by

Lemma 2 this is equal to Dom (∀xA, i, S). As far as assignments to time dependent variables are concerned,

∪

a∈Var(x, ∀xA, i, S)

RelTDV

(n∀ ) =

∪

a∈ Var(x, ∀ xA, i, S)

RelTDV (n a ) =

RelTDV (Aax, i, S) = (by definition 4) RelTDV (∀xA, i, S).

4. Let F = Futr (A, t) (a similar argument can be applied to the case when F = Past (A, t) ). 4.1. If term t contains a TD variable y, the algorithm creates |D(y)| evaluability son nodes, with (Futr(A, t ay), i, {(y, i, a)} ∪ asg) in a formula node ns that is son of node nf containing F. One of the |D(y)| evaluability nodes is the node where variable y is associated, at time instant i, with the value ηi(y) = Si(y). By the inductive hypothesis1, node ns, and thus also node nf, is associated with the set of TD assignments RelTDV (Futr (A, tay ), i, S) ∪ {(y, i, a)} that is equal to RelTDV (Futr (A, t), i, S). Dom (Futr(A, t), i, S) = Dom (nf) follows from the in-

1 Actually, by substituting in term t a constant for TD variable y, the structure of the formula does not change, since it

remains of the form Futr (A, t'); thus the used argument is not a proper induction on the structure of the formula. Nevertheless, the number of TD variables in t is finite, and hence, after a certain number of substitutions have been performed, the situation of case 4.2, where term t does not contain TD variables, is obtained. Therefore, this is precisely an argument by induction on the number of TD variables in term t (case 4.2 is the base) which is performed inside the induction on the structure of the formula.

47

ductive hypothesis and from Dom (n f ) = Dom (ns ) and Dom (Futr (A, t), i, S) = Dom (Futr(A, tay ), i, S). 4.2.

If term t does not contain TD variables, then it is evaluated. Let v be its value; since there exists a structure S such that Evaluable (Futr(A, t), i, S), then i + v = k ∈ T. Thus the algorithm creates a son node n s with (A, k, asg). Evaluable (Futr (A, t), i, S) implies Evaluable (A, k, S), and the inductive hypothesis applies: RelTDV (n s ) = RelTDV (A, k, S) = RelTDV (Futr (A, t), i, S) = RelTDV (nf). Similarly, Dom (ns ) = Dom (A, k, S) = Dom (Futr (A, t), i, S) = Dom (nf).

We now prove part b) of the Lemma: if the algorithm terminates successfully, (i.e., there exists an unmarked evaluability leaf node ne) then, for every structure S that performs the assignments to TD variables contained in RelTDV (ne), Evaluable (F, i, S) holds, RelTDV (ne) = RelTDV (F, i, S), and Dom (ne) = Dom (F, i, S). The proof is again by induction on the structure of formula F. Base: Let F = A (t1 ...t n ). The algorithm terminates successfully and, for all structures S, Evaluable (F, i, S), RelTDV (F, i, S) = ∅ = RelTDV (ne ) and Dom (F, i, S) = {()}= Dom (ne), where ne is the only node constructed by the algorithm. Induction step. 1. Let F = ¬A. The algorithm substitutes F with A. The proof follows from the inductive hypothesis from Dom (¬A, i, S) = Dom (A, i, S), and from RelTDV (¬A, i, S) = RelTDV (A, i, S). 2. Let F = A ∧ B. From node nA∧B containing A∧B two son nodes nA and nB are created, containing A and B respectively, that are then expanded independently, except for the consistency checks of step 4. If the algorithm terminates successfully then there exists an evaluability leaf where the root nA∧B of the formula tree is unmarked, and thus neither n A nor nB are marked. Since the two nodes are developed independently, by the induction hypothesis in every structure S A or SB that includes assignments of nA or nB, Evaluable (A, i, SA ) and Evaluable (B, i, SB) hold. By step 4 of the algorithm, the unmarked evaluability leaf node does not contain conflicting assignments to TD variables; thus there exist structures that perform all the assignments to TD variables contained either in RelTDV (n A ) or in RelTDV (nB ). For every such structure, call it S A∧B , both Evaluable (A, i, SA∧B ) and Evaluable (B, i, SA∧B ) hold, and thus Evaluable (A∧B, i, SA∧B ) also holds. Moreover, RelTDV (nA∧B) = RelTDV (nA) ∪ RelTDV (nB) (ind=hp) RelTDV (A, i, S) ∪ RelTDV (B, i, S), and Dom (nA∧B ) = Dom (nA ) × Dom (nB ) (ind=hp) Dom (A, i, SA∧B ) × Dom (B, i, S A∧B ). 3. Let F = ∀xA. From node n∀, that contains ∀xA, |D(x)| son nodes are created, each containing formula Aax for a different a∈D(x); let us call na the node with Aax. All nodes are expanded inde48

pendently, except for consistency checks of step 4. Call Sa any structure that performs the assignments of RelTDV (na). By the induction hypothesis, for every unmarked node n a, and for every Sa, Evaluable (Aax, i, Sa), RelTDV (na) = RelTDV (Aax , i, Sa), and, for the same reasons as in the proof of part a), Dom (na) = {(x, a)} ∪ Dom (A ax , i, Sa ). From step 4, the different RelTDV (na) do not contain conflicting assignments to TD variables, hence there exists a structure S∀ that simultaneously performs the assignments of RelTDV (na) for all unmarked na. The values a for which na is not marked are exactly those of Var (x, ∀xA, i, S), since the values for which na is marked do not belong to Var (x, ∀xA, i, S∀ ). This is because if a∈Var(x, ∀xA, i, S∀ ) then Evaluable (Aax , i, S∀ ) and, by the proof of part a), node n a would not be marked. From the respective definitions, the following equalities hold. RelTDV (n∀) = =

(ind hp)

∪

a∈Var(x, ∀xA, i, S∀ )

∪

a∈Var(x, ∀xA, i, S∀)

RelTDV (na) =

RelTDV (Aax, i, Sa) = RelTDV (∀xA, i, S∀).

Moreover Dom (n∀) = =

(ind hp)

∪

∪

a∈Var(x, ∀xA, i, S∀ )

a∈Var(x, ∀xA, i, S∀)

Dom (na) =

{(a)} × Dom (Aax, i, Sa) = Dom (∀xA, i, S∀).

4. Let F= Futr (A, t) (a similar argument can be applied to the case when F = Past (A, t) ). 4.1 If term t contains a TD variable y, |D(y)| evaluability son nodes are created, having a node with (Futr(A, t ay ), i, {(y, i, a)}) as a son of the node with F. The algorithm terminates successfully, then, for at least one value a∈D(y), the corresponding son node is not marked. An execution of the algorithm with (Futr (A, tay), i, ∅) in the root node nr, would then terminate successfully, and by the induction hypothesis, for any structure S a with the assignments of RelTDV (n r ), the equalities RelTDV (Futr (A, t ay ) , i , S a ) = RelTDV (n r ) and Dom (Futr (A, tay ), i, Sa ) = Dom (nr ) would hold. Starting with Futr (A, t) in the initial node n, we obtain instead RelTDV (n) = {(y, i, a)} ∪ RelTDV (Futr (A, tay ), i, Sa ) = RelTDV (Futr (A, t), i, S), where S is a structure with the assignments of RelTDV (Futr (A, tay ), i, Sa ) plus (y, i, a). For any such S, Evaluable (Futr (A, t), i, S) holds, and Dom (Futr (A, t), i, S) = Dom (Futr (A, t ay), i, Sa) = Dom (nr) = Dom (n). 4.2

If term t does not contain TD variables, the evaluations v = S(t) and k = i + v take place. Successful termination implies k∈T: a node ns is created, with (A, k, asg) and by the inductive hypothesis every structure S with the assignments to TD variables of RelTDV (n s) ensures

49

Evaluable (A, k, S), RelTDV (n) = RelTDV (ns) = RelTDV (A, k, S) = RelTDV (Futr (A, t), i, S) and Dom (n) = Dom (ns) = Dom (A, k, S) = Dom (Futr (A, t), i, S). QED A second lemma states the correctness of the Semantic Tableaux Algorithm, that constitutes the second part of the algorithm for the verification of the satisfiability of TRIO formulas. Lemma 6. Given a closed TRIO formula F, let F = {F1,...Fn} be a set of subformulas of F, possibly with variables instantiated by constants, that appear (deprived of the outermost negation when they have the form Fj = ¬Aj) in a formula node of an unmarked evaluability leaf node ne of the evaluability tree built starting from F, a frame D, T, Φ, Π, and a time instant i∈T, each subformula Fj being associated with time instant ij∈Τ. Let the Semantic Tableaux Algorithm be initialized by including in the root tableau (Fj, ij, pj), for each j, where pj is a reference to the formula node, inside n e, that contains Fj (possibly deprived of the outermost negation) and the assignments to TD variables contained in the unmarked formula leaf nodes of ne. Then there exists a structure S, that performs those assignments to TD variables and such that S, ij Fj for all j, if and only if the execution of the Semantic Tableaux Algorithm terminates successfully. We prove the if and only if parts separately and by induction on the structure of formulas F j. If part: if the algorithm terminates successfully then there exists a structure satisfying all formulas. Base. Let the various Fj be literals (that do not contain TI variables, from the assumption of closure of the initial formula F). Step 3 of the tableaux algorithm, repeatedly executed, substitutes values of the TD variables, in all possible combinations, but without contradictions and consistently with the assignments to TD variables already present in the tableau, since step 5 marks the tableaux containing inconsistent assignments. After step 6, if there exists an unmarked tableau and if it contains a literal p(v1..vn), p being a TI predicate, then (v1..vn)∈Π(p). If it contains ¬p(v1 ..v n ) then (v1 ..v n )∉Π(p). Moreover, the tableau does not contain both (q(v1..vm), i, p') and (¬q(v1..vm), i, p"), q being a TD predicate. Hence, all formulas Fj are verified by any structure S such that η i(y) = a if (y, i, a) is in the unmarked tableau, (v 1 ..vm )∈Π i(q) if (q(v1 ..vm ), i, p') is there, and (v1 ..vm )∉Π i(q) if (¬q(v1 ..vm ), i, p") appears. Induction step. 1. Let Fj = ¬¬A. Step 2.1 of the algorithm expands formula F into A. By the induction hypothesis, successful termination implies there exists S s.t. S, i j A. For the same S, we then have S, ij ¬¬A.

50

2. Let Fj = A∧B. Step 2.2 of the algorithm creates two son nodes with (A, ij, pA) and (B, ij, pB). From the induction hypothesis and successful termination it follows that there exists S s.t. S, ij A and S, ij B. For the same S, we have S, ij A∧B. 3. Let Fj = ¬(A∧B). Step 2.3 creates two son nodes containing ¬A and ¬B. Successful termination implies that at least one of the sons is not marked. By the induction hypothesis, there exists a structure SA s.t. SA, ij ¬A, that is SA ij / A, or there exists a structure S B s.t. SB, ij ¬B, that is SB i j / B. By choosing S = SA in the first case (S = SB in the second) we have S , i j / A∧B, that is, S, ij ¬(A∧B). 4. Let Fj = ∀xA. Step 2.4 creates a tableau with as many (Aax , ij, pa) as there are unmarked son nodes in the formula tree of the evaluability leaf node, each corresponding to a different a∈Var(x, ∀xA, ij, S) for all structures S with the evaluation kernel defined by the node. By the induction hypothesis the successful termination of the algorithm implies that there exists a structure S s.t. S, ij Aax for all such a. By choosing any S' equal to S everywhere, except possibly in the value assigned to TI variable x–that is, with ξ '(x) = a, for any value a ∈Var (x, ∀xA, ij, S)–we have S', ij ∀xA. 5. Let Fj = ¬∀xA. Step 2.5 of the algorithm creates as many son tableaux with (¬Aax, ij, pa) as there are unmarked son nodes in the formula tree. As in point 4 above, such values of a are exactly those of Var(x, ∀xA, ij, S), for every structure S with the evaluation kernel defined by the node. By the induction hypothesis, successful termination implies that there exists a structure S where S, ij ¬Aax for some of such a, that is S, ij / A ax. By choosing S' as in point 4 above, we have S', ij / Aax and hence S', ij / ∀xA, that is, S', ij

¬∀xA.

6. Let Fj = Futr (A, t) y 6.1 If term t contains a TD variable y, step 2.6.1 creates a son with Futr(A, t a ) where (y, ij, a) belongs to the evaluation kernel determined by the evaluability leaf node. By the induction hypothesis, successful termination implies that there exists a structure S s.t. S, ij Futr(A, t ay) and Sij (y) = a. In the same structure S, we have S, ij Futr (A, t). 6.2

If term t does not contain any TD variable, step 2.6.2 evaluates v = S(t) and k = i + v, and creates a son tableau with (A, k, ps), where ps refers to p’s son. By the induction hypothesis, successful termination implies that there exists a structure S s.t. S, k A and Sij (t) = v. In the same structure S, we have S, ij

Futr (A, t).

The cases Fj = ¬Futr (A, t) and Fj = Past (A, t) can be defined accordingly. Only if part: if there exists a structure S then the algorithm terminates successfully.

51

Base. Let F be composed of literals. Step 3 of the algorithm, repeatedly applied, performs substitutions for the variables occurring in the literals, in all possible ways. Among these are the substitutions of S; the tableau resulting from such substitutions includes literal L iff L is true, and ¬L iff L is false is S, because substitution of values for variables preserves the truth values of formulas. Moreover, if p(t 1..tn) is true, p being a TI predicate, p(v1..vn) is obtained, with (v1..vn)∈Π(p), and if ¬p(t1..tn) leads to ¬p(v1..vn) then (v1..vn)∉Π(p). Finally, according to TRIO’s semantics, the tableau cannot contain both (q(t1..tm), i, p') and (¬q(t1..tm), i, p"), so that (q(v1 ..vm ), i, p') and (¬q(v1 ..vm ), i, p") cannot be both present after substitution. For these reasons, the tableau where the substitutions of S are performed is not marked, and the algorithm terminates successfully. Induction step. 1. Let Fj = ¬¬A. If there exists structure S s.t. S, i j ¬¬A then S, ij A. Step 2.1 creates a son tableau with (A, ij, pf) that by the induction hypothesis is not marked. Hence the father tableau is not marked, and the algorithm terminates successfully. 2. Let Fj = A∧B. Step 2.2 creates a son tableau with (A, ij, pA) and (B, ij, pB). S, ij A∧B implies S , i j A and S, ij B; then, by the induction hypothesis the son tableau is not marked and the algorithm terminates successfully. 3. Let Fj = ¬(A∧B). Step 2.3 creates two son tableaux with ¬A and ¬B. If there exists a structure S s.t. S, ij ¬(A∧B), then S, ij / A or S, i j / B, that is, S, ij ¬A or S, ij ¬B. In any case, one of the two son tableaux is not marked, and this leads to successful termination. 4. Let Fj = ∀xA. Step 2.5 creates a son tableau with (Aax, ij, pa) for all a∈Var (x, ∀xA, ij, S). The existence of a structure S s.t. S, ij

∀xA implies that S, ij

Aax for all a∈Var(x, ∀xA, i j, S);

thus, the son tableau is not marked, and the algorithm terminates successfully. 5. Let Fj = ¬∀xA. Step 2.5 creates several son tableaux (¬A ax , ij, pa ), one for each different a ∈ Var (x, ∀xA, i, S). If there exists a structure S s.t. S, i j ¬∀xA, then S, ij / ∀xA; that is, there exists an a∈Var (x, ∀xA, ij, S) such that S, ij / Aax, which implies S, ij

¬Aax. By the

inductive hypothesis the son corresponding to value a is not marked, and the algorithm terminates successfully. 6. Let Fj = Futr (A, t). x 6.1 If term t contains a TD variable y, step 2.6.1 creates a son node with Futr (A, t a ), i, ps ), where (y, a, ij) belongs to the evaluation kernel defined by the evaluability leaf. If there exists a structure S s.t. S, ij Futr (A, t), then S, ij Futr (A, tay), with a = Sij(y). Thus the son node is not marked, and the algorithm terminates successfully.

52

6.2

If term t does not contain TD variables, step 2.6.2 evaluates v = Sij(t), k = i + v, and creates a son tableau with (A, k, ps). The existence of a structure S where S, i j Futr (A, t) implies that S, k A; by the induction hypothesis the son tableau is not marked, and the algorithm terminates successfully. QED

As a special case, if F = {F}, we can immediately prove that the Semantic Tableaux Algorithm is correct for any closed TRIO formula. Theorem 4, asserting the correctness of the algorithm for constructively verifying the satisfiability of a closed TRIO formula, is a straightforward consequence of the above two lemmas.

Appendix III Proof of Theorem 5 The theorem will be proved by induction on the structure of the temporally closed formula, taking points i) and ii) of definition 5 as the base of induction. p(t1..tn); this implies that (Si(t1), .. Si(tn)) ∈ Π(p). Since all terms in the formula contain only time independent variables, (Si(t1), .. Si(tn)) = (Sj(t1), .. Sj(tn)) for every j∈T; hence S, j p(t1..tn).

For case i), assume that S, i

For case ii), consider the normal form of Sometimes(A): A ∨ SomP (A) ∨ SomF (A) ≡ A ∨ ¬∀s (s>0 → Past (¬A, s)) ∨ ¬∀t (t>0 → Futr (¬A, t)). If S, i

Sometimes (A) than one of the three above disjuncts is satisfied. But S, i S, i

SomP (A) SomF (A)

⇒ ⇒

∃ j ∈ T s.t. j < i, Evaluable (A, j, S), and S, j ∃ j ∈ T s.t. j > i, Evaluable (A, j, S), and S, j

In any case, there exists a j∈T such that Evaluable (A, j, S) and S, j

A, and A.

A. Take then any i1 such that

Evaluable (Sometimes(A), i1, S); since T is totally ordered, either i 1=j, or i1>j, or i1 0 → Past (¬P, s) ) ∨ ¬∀t (t > 0 → Futr (¬P, t) ). The execution of the algorithm for the construction of the evaluability tree on a history formula Sometimes (∧j Futr (Fj, tj) ∧ ∧k Past (Pk, tk)) with reference to time instant i where the formula is evaluable, builds the trivial evaluability tree that has a single node and determines, for variables s and t, an evaluation domain composed of all values which, when added or subtracted to i, give a value h such that Evaluable (∧j Futr (Fj, tj) ∧ ∧k Past (Pk, tk), h, S). Disjunction A∨B is defined as ¬(¬A∧¬B), so the tableaux algorithm with the history formula in the root tableau eventually produces, by execution of steps 2.3 and 2.1, three distinct tableaux containing respectively, formulas ∧ j Futr (Fj, tj) ∧ ∧ k Past (Pk, tk), SomP(∧ j Futr (Fj, tj) ∧ ∧ k Past (Pk, tk)), and SomF(∧j Futr (Fj, tj) ∧ ∧k Past (Pk, tk)). The successive steps in the execution of the algorithm will then create as many distinct tableaux, each one containing formula ∧ j Futr (Fj , tj ) ∧

∧k Past (Pk, tk), as there are time instants in the temporal domain where such formula is evaluable. To show that such tableaux will be created, let us consider the tableau containing formula SomF( ∧ j Futr (Fj, tj) ∧ ∧ k Past (Pk, tk))–the case of SomP(∧ j Futr (Fj, tj) ∧ ∧ k Past (Pk, tk)) is dealt with accordingly. Any formula of the type SomF (P) can be rewritten as ¬∀t(t>0→Futr(¬P,t)), and, since implication is defined as A→B ≡ ¬A∨B ≡ ¬(¬¬A∧¬B), the formula SomF(P), can be rewritten as ¬∀t¬(¬¬t>0∧¬Futr(¬P,t)). Execution of step 2.5 of the tableaux algorithm generates one tableau containing formula ¬¬(¬¬t->0∧¬Futr(¬P,t-)) for every value t- in the variability domain of variable t. By executing steps 2.1 and 2.2 of the algorithm, a son tableau with the two formulas t>0 and ¬Futr (¬P, t-) is generated for each of the above tableaux. Then, all tableaux containing a value t≤0 are marked, and execution of steps 2.6 and 2.1 generates tableaux containing formula P associated with every time instant j ∈ Τ such that j > i and formula ∧j Futr (Fj, tj) ∧ ∧k Past (Pk, tk) is evaluable at time instant j. It is now evident, from steps 2.2, 3, and 6 of the tableaux algorithm, that all final unmarked tableaux will be superimposable. QED

54

References 1. 2. 3. 4. 5. 6.

7.

8. 9.

10.

11. 12. 13. 14. 15. 16.

Andrews, P.B. An introduction to mathematical logic and type theory: to truth through proofs Academic Press, Harcourt Brace Jovanovich Publishers, New York, 1986. Attiya, H., Lynch, N.A. Time Bounds for Real-Time Process Control in the Presence of Timing Uncertainty. IEEE Symposium on Real-Time Systems (1989). Barringer, H., Cheng, J.H., and Jones, C.B. A Logic Covering Undefinedness in Program Proofs, Acta Informatica 21, (1984) 251-269. Ben-Ari, M., Pnueli, A., and Manna, Z. The Temporal Logic of Branching Time. Acta Informatica 20, (1983), 207-226. Bernstein, A., and Harter, P.K. Proving real-time properties of programs with temporal logic. Proceedings. of the 8th ACM Symposium on Operating Systems, (1981), 1-11. Clarke, E.M., and Emerson, A.E., Design and synthesis of synchronization skeletons using branching time temporal logic. in IBM Logics of Programs Workshop, Springer Verlag Lecture Notes in Computer Science 131, (1981). Coen, A., Morzenti, A., and Sciuto, D. Specification and Verification of Hardware Systems using the Temporal Logic Language TRIO. in Borrione, D., and Waxman, R. Eds. Proceedings of IFOP 10th International Conference on Hardware Description Languages and their Applications, North Holland, Amsterdam, 1991, 43-61. Gehani, N. Ada, an advanced introduction Prentice-Hall, Englewood Cliffs, NJ, (1983). Ghezzi, C., Mandrioli, D., and Morzenti, A. TRIO, a Logic Language for Executable Specifications of Real-Time Systems. Journal of Systems and Software, 12, 2 (May 1990), 107-123. Ghezzi, C., Mandrioli, D., and Morzenti, A. TRIO, a Logic Language for Executable Specifications of Real-Time Systems. in Proceedings of 10th French-Tunisian Seminar on Computer Science, (1989), 322-349. Guttag, J.V., Horowitz, E., Musser, D. The design of Data Type Specifications, in R. T. Yeh Ed. Current Trends in Programming Methodologies 4, Prentice Hall, (1978). Halpern, J., Manna, Z., and Moszkowski, B., A Hardware Semantics Based on Temporal Intervals. in Lecture Notes on Computer Science, 154, 1983, 278-291. Kemmerer, R.A. Testing Software Specifications to Detect Design Errors. Transactions on Software Engineering, 11, 1, (Jan 1985), 32-43. Koymans R., and De Roever, W.P. Examples of a Real–time Temporal Logic Specification, in Lecture Notes in Computer Science, 207, 1985, 231-251. Koymans, R. Specifying Message Passing and Time-Critical Systems with Temporal Logic. Ph.D. Dissartation, Eindhoven University of Technology, 1989. Koymans, R., Kuiper, and R., Zijlstra, E., Specifying message passing and real-time systems with real-time temporal logic. in ESPRIT ’87 Achievement and Impact, North Holland, 1987, 311-324.

55

17. Kröger, F. Temporal Logic of Programs EATCS Monographs on Theoretical Computer Science, Springer Verlag, 1987. 18. Lynch, N., and Attiya, H Using Mappings to Prove Timings Properties. in Proceedings of ACM Conference on Principles of Distributed Computing, 1990. 19. Manna, Z., and Wolper, P. Synthesis of Communication Processes from Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 6, 1, (Jan. 1984), 68-93. 20. Mendelson, E. Introduction to mathematical logic Van Nostrand Reinold Company, New York, 1963. 21. Morzenti, A. The specification of real–time systems: proposal of a logical formalism. Ph.D. Dissertation, Dipartimento di Elettronica, Politecnico di Milano, (in Italian), 1989. 22. Morzenti, A., and San Pietro, P. TRIO Specification of manoeuvre regulation in pondage power stations. Politecnico di Milano/ENEL-CRA research report (in Italian), June 1990. 23. Morzenti, A., Ratto, E., Roncato, M., and Zoccolante, L. TRIO, a Logic Formalism for the Specification of Real-Time Systems. in Proceedings of IEEE Euromicro Workshop on real-time, (1989), 26-30. 24. Moszkowski, B. A Temporal Logic for Multilevel Reasoning about Hardware. IEEE Computer Magazine, (Feb.1985) 10-19. 25. Narayana, K.T., and Aaby, A.A. Specification of Real-Time Systems in Real-Time Temporal Interval Logic. Proceedings of IEEE Symposium on Real-Time Systems, (1988), 86-95. 26. Ostroff, J.S. Modelling, Specifying and verifying Real-time Embedded Computer Systems. in Proceedings of IEEE Symposium on Real-Time Systems, (1987), 124-132. 27. Ostroff, J.S., Temporal Logic for Real-Time Systems, Advanced Software Development Series, Research Studies Press, John Wiley & sons, Taunton, Somerset, England, 1989. 28. Owicki, S., and Lamport, L., Proving Liveness Properties of Concurrent Programs. ACM Transactions on Programming Languages and Systems, 4, 3, (July 1982), 455-495. 29. Pnueli, A. The temporal semantics of concurrent programs. Theoretical Computer Science 13, North Holland Publishing Company, (1981), 45-60. 30. Rescher, N., and Urquhart, A., Temporal Logic Springer Verlag, Vienna-New York, 1971. 31. Schwartz, R.L., Melliar-Smith, P.M., and Vogt, F.H. An Interval-Based Temporal Logic. in Proceedings of Logics of Programs, Lecture Notes on Computer Science 164, 1984, 443-457. 32. Smullian, R.M., First order Logic Springer Verlag, New York, 1968. 33. Wirth, N. Towards a Discipline in Real-Time Programming. Comm. ACM 20-8, (Aug. 1977), 577-583. 34 Wolper, P. Temporal logic can be more expressive. Information and Control 56, (1983), 72-99.

56