# A Tableau Calculus for a Temporal Logic with Temporal Connectives

发布时间:2021-11-29 05:59:18

A Tableau Calculus for a Temporal Logic with Temporal Connectives

Wolfgang May

Institut f r Informatik, Universit t Freiburg, Germany,

may@informatik.uni-freiburg.de

Abstract. The paper presents a tableau calculus for a linear time temporal logic for reasoning about processes and events in concurrent systems. The logic is based on temporal connectives in the style of Transaction Logic BK94] and explicit quanti cation over states. The language extends rst-order logic with sequential and parallel conjunction, parallel disjunction, and temporal implication. Explicit quanti cation over states via state variables allows to express temporal properties which cannot be formulated in modal logics. Using the tableau representation of temporal Kripke structures presented for CTL in MS96] which represents states by pre x terms, explicit quanti cation over states is integrated into the tableau calculus by an adaptation of the -rule from rst-order tableau calculi to the linear ordering of the universe of states. Complementing the CTL calculus, the paper shows that this tableau representation is both suitable for modal temporal logics and for logics using temporal connectives.

1 Introduction

When extending rst-order logic to temporal logic, most approaches are based on modal operators, such as LTL/CTL or Dynamic Logic. Here, formulas are modi ed via modalities inducing an implicit quanti cation over states. Formulas are evaluated wrt. states or (in nite) paths, thus they do not support an intuitive notion of sequentiality or parallelism. For reasoning about processes and events in concurrent systems, temporal connectives such as sequential, parallel, and alternative composition or iteration are well-known from process algebraic formalisms. First-order-logic based formalisms using temporal connectives (which implies evaluating formulas wrt. nite path segments) are rare, although they have obvious advantages when reasoning about temporal behavior of processes. For Transaction Logic BK94], it has been shown how to write executable speci cations in such a formalism. There are some temporal constraints which cannot be expressed in temporal modal logics, e.g., that if some state is reached such that a given predicate p has the same extension as now, then q holds in this state (cf. TN96,CT98]). In CT98], it is shown that this can be expressed in 2-FOL which is a two-sorted rst order language for dealing with a linear temporal state space by

8 1

s ; s2 : ( x : p(x; s1 )

8

$

p(x; s2 ) s1 < s2 )

^

!

q(s2 ) :

This example motivates that an explicit quanti cation and addressing of states via state variables would be useful in a temporal logic. In MS96], a tableau semantics for rst-order Kripke structures has been presented, together with a tableau calculus for rst-order CTL. There, states have been described by pre x terms which provide a natural way to adapt the and -rule to quanti cation by state variables. In the present paper, it is shown how the same approach applies for this temporal logic based on temporal connectives and explicit quanti cation over states. The paper is structured as follows: After introducing some basic notions in Section 2, a (linear-time) logic for formulating complex events and dynamic constraints is presented in Section 3. Section 4 contains the tableau semantics for linear Kripke structures, and the tableau calculus is given in Section 5. Section 6 closes with some concluding remarks.

Related Work. Most of the work in Temporal Logics focuses on modal logics, e.g., CTL, modal -calculus, or Dynamic Logic. An overview of tableau calculi for (modal) temporal logics have been summarized in Wol85], a recent one is described in MP95]. Interval Logics contain operators for sequential composition and iteration similar to those known from programming languages Mos86]. A tableau method for interval logic has, e.g., been presented in BT98]. Other formalisms for expressing temporal constraints in non-modal logics are dealt with in Sin95], BK94], Pra90], Jab94], and TN96,CT98].

2 Basic Notions

Let be a signature consisting of a set func of function symbols a set pred of predicate symbols with xed arities ord(f ) resp. ord(p), and Var := x1 ; x2 ; : : : an in nite set of variables. Let Term denote the set of terms over and Var. The notions of bound and free variables are de ned as usual, free( ) denoting the set of variables occurring free in a set of formulas. A substitution (over a signature ) is a mapping : Var Term where (x) = x for only nitely many x Var, here denoted by (x)=x]. Substitutions are extended to terms and formulas as usual. A rst-order structure I = (I; U ) over a signature consists of a universe U and a rst-order interpretation I of which maps every function symbol f to a function I (f ) : U ord(f ) U and every predicate symbol p to a relation I (p) U ord(p) . A variable assignment is a mapping : Var U . For a variable assignment , a variable x, and d U , the modi ed variable assignment d is identical with x except that it assigns d to x. Let denote the set of variable assignments. Every interpretation induces an evaluation I : Term U s.t. I (x; ) := (x) for x Var, and I (f (t1 ; :::; tn ); ) := (I (f ))(I (t1 ; ); :::; I (tn ; )) for f , ord(f ) = n and t1 ; :::; tn Term . The truth of a formula F in a rst-order structure I under a variable assignment , (I ; ) = F is de ned as usual.

f g F F ! 6 2 2 ! 2 ! 2 ! 2 2 2 j

3 Temporal Connectives and Quanti cation

Temporal speci cations consist of combining subformulas by temporal connectives. The logic presented here incorporates the following facilities: denotes sequential conjunction via subsequent path segments and denotes a parallel conjunction on the same path segment. e? denotes nite iteration, mostly limited by a rst-order condition on a state which is tested between each two iterations. Constraints are speci ed by constraint formulas in an if-then-style. In temporal context, there are three possible implication constructs (if : : : then before/later/sometimes : : : ). With a suitable synchronization formalism, they can be formulated by a single causal implication e ; f. Via temporal quanti cation, formulas introduce private synchronization points which represent agreements local to processes. From the modeling point of view, synchronization points are virtual entities. This idea shows some similarities with rst-order existential quanti cation of a variable x: there is a local agreement (binding), which entity is meant by x, without identifying it extensionally. This information is kept local to the scope of the quanti er. Following this idea, synchronization points are handled via a set SVar of state variables si which can be bound to states. The logic is interpreted by linear rst-order Kripke structures which are augmented by a transition oracle (cf. BK94]) representing the actions which are executed in the state transitions. A linear rst-order Kripke structure over a signature is a pair K = (U ; M ), where U is a universe and M is a mapping from the natural numbers to rst-order interpretations M (n) over . Since a constant universe is presumed, the notion of a variable assignment is de ned as in the rst-order case. For every transition from n to n+1, the transition oracle yields an interpretation N (n) of a set A of action symbols similar to predicates. Having (u1 ; : : : un) (N (n))(a) for a A in the transition oracle means that a(u1 ; : : : ; un) is executed in the transition from n to n+1. De nition 1 (Action Formulas). Action formulas are rst-order formulas over the signature A func . Action formulas are evaluated wrt. transitions K i; i+1 as (K i; i+1 ; ) = a(t1 ; : : : ; tn ) (M (i)(t1 ; ); : : : ; M (i)(tn ; )) N (n)(a), using the transition oracle.

2 2 h i h i j , 2

rst-order signature and an action signature A is de ned inductively. With every ECL formula e, a length len(e) IN f1g, is associated; the addition + on subsets of IN f1g is de ned as N +M := fk : 9n 2 N; m 2 N j k = n+mg. 1. Every rst-order formula ' is an ECL formula of length len(') = f0g. 2. @ and ? are ECL formulas with length len(@ ) = len(?) = IN f1g. @ denotes idling for an arbitrary time, ? denotes an action which can never be executed successfully (often called deadlock).

De nition 2 (ECL-Event Formulas). The language of ECL formulas over a

3. Every action formula e is an ECL formula of length len(e) = f1g. 4. With s a state variable and e an ECL formula such that s is not free in e, s e is an ECL formula with len(s e) = len(e), and if len(e) \ IN 6= ;, e s is an ECL formula with len(e s) = len(e) \ IN. Then, s is free in s e and e s (pre xing or post xing with a synchronization point). 5. With e an ECL formula with len(e) \ IN 6= ; and f an ECL formula, e f is an ECL formula, len(e f) = (len(e) \ IN)+len(f) (sequential composition). 6. With e and f ECL formulas with len(e) \ len(f) 6= ;, e f is an ECL formula with len(e f) = len(e) \ len(f) P (parallel composition). 7. With e1 ; : : : ; en ECL formulas, 1 i n ei is an ECL formula with S P len( 1 i n ei ) = 1 i n len(ei ) (alternative composition). 8. With e an ECL formula, e? is an ECL formula with len(e? ) = fn j 9k 2 I ; n1 ; : : : ; nk 2 len(e) and n = n1 + : : : +nk g ( nite iteration). N 9. With e an ECL formula and x a variable, 8x : e and 9x : e are ECL formulas, len(8x : e) = len(9x : e) = len(e). 10. With s a state variable and e an ECL formula, s : e and if 1 2 len(e) s : e are ECL formulas, len( s : e) = len(e), len( s : e) = f1g (introducing a state variable). Each of the above ECL formulas is an ECL-event formula.

ECL-event formulas hold on a segment of a Kripke structure. For a linear Kripke structure K and i j such that i IN, j IN , the expression K i; j ] denotes the whole structure, with the focus on the segment i; j ].

2 2 f1g

ture, an assignment of state variables is a function which maps every state variable to a state of K , i.e., a natural number. The modi cation of an assignment of state variables at one element is de ned in the same way as for rst-order variable-assignments: For an assignment of n state variables, a state variable x, and n 2 IN, the modi cation s is identical with except that it assigns n to the state variable s: t 7! (t) if t 6= s ; n s : SVar ! IN : s 7! n otherwise .

De nition 3 (Assignment of State Variables). For a linear Kripke struc-

De nition 4 (Semantics of Event Formulas). Let K be a linear Kripke

structure with a universe U , a variable assignment, an assignment of state variables. Then, j= is extended to ECL formulas as follows: 1. For ' a rst-order formula: (K i; j ]; ) j= ' :, i = j and (M (i); ) j= ' . 2. (K i; j ]; ; ) j= @ for all i j , and (K i; j ]; ; ) j= ? for no i; j . 3. For ' an action formula: (K i; j ]; ) j= ' :, j = i+1 and (K hi; j i; ) j= '. 4. (K i; j ]; ; ) j= s e :, (s) = i and (K i; j ]; ; ) j= e , and (K i; j ]; ; ) j e = s :, (s) = j 2 IN and (K i; j ]; ; ) j= e . 5. (K i; j ]; ; ) j= e f :, there is a k 2 IN s.t. (K i; k]; ; ) j= e and (K k; j ]; ; ) j= f .

i; j ]; ; ) j= e and (K i; j ]; ; ) j= f . there is a 1 k n s.t. (K i; j ]; ; ) j= ek . e? :, there is a k 0 s.t. (K i; j ]; ; ) j= | e {z: : : e . e } (note that for k = 0, this means true) k-times 9. (K i; j ]; ; ) j= 9x : e :, there is a d 2 U s.t. (K i; j ]; d ; ) j= e , x (K i; j ]; ; ) j 8x : e :, for all d 2 U , (K i; j ]; d ; ) j e . = x = k 10. (K i; j ]; ; ) j= s : e :, there is a k : i k j and (K i; j ]; ; s ) j= e, k ) j= e . (K i; j ]; ; ) j = s : e :, j = 1 and for all k i, (K i; j ]; ; s P As short notations, e f := e @ f and e1 + + en := i2f1;:::;ng ei are used.

6. 7. 8.

(K (K (K )j = )j = )j =

i; j ]; ; i; j ]; ; i; j ]; ;

e f P

1:::n ei

:, (K :,

Remark 1 (Semantics of ECL). Note, that in this de nition, if f is an ECL formula and e is a subformula of f, the segment of the Kripke structure which is looked at for e is always contained in the segment which is looked at for f. This will not be the case in De nition 6 where the semantics of temporal implication is de ned. ECL-event formulas without universal temporal quanti cation describe nitely detectable events: Proposition 1 (Finite Satis ability). Let e be an ECL-event formula which does not contain s. Then, if a (possibly in nite computation) satis es e (i.e., an event described by e occurs in the computation) then already a nite pre x of this computation satis es e. Formally, (K i; j ]; ; ) j= e implies that there is a (unique least) i k j such that k < 1 and (K i; k]; ; ) j= e. For the proof, one must consider that an in nite sequence only satis es formulas which contain either or a nal delay (this will change with the introduction of temporal implication in Sec. 5). As a consequence, events of in nite length, i.e., len(e) = f1g (note that these are exactly those events which contain in all their alternatives), cannot be post xed: there is no state where an action raising such an event can be terminated. Example 1 (Event Formulas). Iteration: a state will be reached where F holds, an then, e is iterated until G is satis ed: @ F e? G . Conditional execution: If the set of elements for which some ECL formula e(x) should be satis ed should be restricted by some rst-order formula '(x), this can be formulated as s : 8x : (('(x) e(x)) + (:'(x) @ )) s . Consider a work ow, consisting of several jobs, each of them can be performed by several ways, consisting of a rst and a second part. The additional condition is that all rst parts are nished before some second part is started: This is done by a synchronization variable local to the process: Work ow = s : (Job1 Job2 : : : Jobn ) ; Jobi = Wayi;1 + + Wayi;ki ; Wayi;j = @ Firsti;j @ s @ Secondi;j @ :

Constraints can be used for describing processes from another point of view: in a declarative way, computations not satisfying a given set of constraints can be ruled out. Temporal constraints are speci ed by constraint formulas in an ifthen-style. With the above synchronization formalism, the temporal implication constructs if : : : then before/later/sometimes : : : can be formulated by a single implication and state variables. De nition 5 (Constraint Formulas). For expressing temporal constraints, an additional connective is added to the syntax of ECL formulas: 11. For ECL formulas e; f, e ; f is an ECL (constraint) formula with len(e ; f) = 0 (temporal implication).

3.1 Constraints

De nition 6 (Semantics of Constraints). Let K be a linear Kripke structure, a variable assignment, an assignment of state variables. Then, = is extended to ; as follows: 11. (K i; j ]; ; ) = (e ; f) : i = j and if (K i; k ]; ; ) = e for some k ,

j j ,

then (K 0; k2 ]; ; ) j= f for some k2 . Note that e ; ? is ECL's negation, i.e., requires that an event e is not detected. In contrast to ECL-event formulas (cf. Remark 1), for a general ECL-constraint formula, the whole path has to be considered for evaluating the consequence. For negation via temporal implication, the focused segment has not to be extended. A constraint is evaluated wrt. one state and has length 0. Proposition 2 (Connectives of Jab94]). The constraint connectives used in Jab94] can be de ned as derived symbols: Deadline : eventually D will be satis ed, and before, C has to be satis ed:

1

j

1

D < C : (@ D @ ) s : ((@ s D) ; (@ C @ s)) : Delay : C can only occur if D occured before: C>D : s : (@ s C ) ; ((@ D @ s)) :

, ,

Example 2 (Constraints). (assume e; f, and g to be action formulas) After f, e will never be satis ed: (@ f e) ; ? , if e and later f are satis ed, then between them, g must eventually be satis ed: s1 ; s2 : (@ e s1 s2 f) ; (@ s1 @ g @ s2 ) . between e and the next f, g is not satis ed:

? ?

s1 ; s2 : ((@ e s1 s2 f) ((@ s1 @ f @ s2 ) ; )) ; ((@ s1 @ g @ s 2 ) ; ) : if e is satis ed, in the state before, F holds: s : (@ s e) ; (@ F s). s s p(x)) @ (s2 p(x)) @ ) + ( p(x))) @ (s2 ( p(x))) @ ))) ; @

: :

Example 3 (2-FOL). The 2-FOL formula given in the introduction which is not expressible in LTL, CTL etc. can be expressed in ECL by

s1 ; s2 ( x((@ (@

8

( 1 ( 1

( 2

s

q) :

4 Tableau Semantics for Linear Kripke Structures

The tableau semantics and -calculus is a linear-time adaptation of the one presented for rst-order CTL in MS96] which uses branching time rst-order Kripke structures as underlying semantics. For the rst-order part, the wellknown rst-order tableau calculus is embedded into the tableau calculus which is constructed. It is necessary to describe many individual states as well as the relations between them in the tableau, including the ordering of states. Thus, three kinds of entities have to be described: Elements of the universe inside states, states, and the path with its transitions. In the chosen semantics, elements of the universe and states will be explicitly named when their existence is stated by a formula: Elements of the universe: a new constant resp. function symbol is introduced by the usual -rule when an existential quanti er is processed. States: states are named when their existence is required by a complex event. In general, between two known states there can be many other still unknown states. These can be named when needed. Thus, a straightforward resolving of eventualities at any time is possible. A similar approach for PLTL where only the relevant states are generated has been used in SGL97]. To allow the naming of states at any position of the model, the description of the path contains, apart from the (partial) ordering of known states, additional information about formulas which have to be true in still unknown states on the segments in-between. These are used when new states are explicitly named.

Representation. As a conceptional extension of rst-order tableaux, every branch of the tableau corresponds to a linear Kripke structure with a transition oracle. Apart from the rst-order portion, information about the frame and the transitions has to be coded in tableau nodes. For distinguishing and naming of states, a tableau calculus based on the free variable tableau calculus given in Fit90] augmented with pre xes is employed: A formula F , assumed to be true in a certain state, occurs in the tableau as state pre xed formula :F . Additionally, path information formulas contain the information about the pre xes situated on the path. Thus, the signature T used in the tableau is partitioned into L ( rst-order part), A (action symbols), and F (pre x symbols). L is obtained by augmenting with a countable in nite set of n-ary skolem function symbols for every n IN and a countable in nite set of variables Xi . F is a set of pre x symbols containing an in nite set of n-ary pre x symbols for every n IN. The construction of pre xes corresponds to the use of skolem functions in the rst-order tableau calculus. Here the pre x symbols take the role of the skolem function symbols. Analogously to the skolem terms containing free variables resulting from invocations of the -rule, pre xes are terms consisting of a pre x symbol ^ of an arity n and an n-tuple of terms as arguments. Additionally, there is a 0-ary symbol ^ which is no pre x symbol but is used in a similar way.

2 2 1

De nition 7. Let

F be the set of pre x symbols and c the subset of which is interpreted state-independently. Then the following sets L and ? are simultaneously recursively de ned: c; 2 ? g ; ff j f an n-ary skolem function symbolg ff j f 2 n L := with ord(f ) = ord(f ) and skolem functions and all f interpreted state-independently, thus c c ff j f an n-ary skolem function symbolg ff j f 2 n c ; 2 ? g: L := The set of pre xes is given as c ? := f^(t1 ; : : : ; tn ) j ^ 2 F is an n-ary pre x symbol, t1 ; : : : ; tn 2 Term L g. For ? Term T , it is precisely the leading function symbol which is a pre x c c symbol taken from F , and all argument terms are in Term L . For L , K induces a state-independent interpretation (K; U ). An interpretation of T describing a Kripke structure K = (U ; M ) is accordingly partitioned: The interpretation of L is taken over by the set fM (i) j i 2 I g of N rst-order interpretations, and the symbols of A are interpreted by the transition oracle. Complementary to this, an interpretation of the pre x symbols in F is de ned. The corresponding evaluation maps pre xes to natural numbers: De nition 8. A pre x interpretation of a set F of pre x symbols to a linear Kripke structure K = (U ; M ) is a mapping : ( F f1g) ! U m ! IN f1g ^ which maps every m-ary pre x symbol ^ 2 F to a function (^) : U m ! I N f1g with ( )=1 , = 1 . De ning ^ K := ( K; IN f1g), is organized similarly to a rst-order interpretation I = (I; U ) with a mapping c and the universe IN f1g, inducing an evaluation K : (? f1g) Term L ! ^ I N f1g of pre xes as follows: c For = ^(t1 ; : : : ; tn ) 2 ? (thus ti 2 Term L evaluated state-independently by K ),

Finally, the interpretation of the derived function symbols f is de ned stateindependently for all i 2 IN as

(M ( ))(

K( ;

) := ( (^ ))(K ( 1

t ; ); : : : ; K (tn ;

))

:

n f (t1 ; : : : ; tn );

) := (M (

K( ;

)))( ( 1

f t ; : : : ; tn );

)

:

Tableau formulas. Logical formulas occur in the tableau as pre xed formulas, additionally, the Kripke frame is encoded in path information formulas (pif s): An additional symbol O can occur instead of pre xes and state variables as an auxiliary generic pre x . O is instantiated by a pre x when a state on the respective segment is explicitly named.

De nition 9 (Syntax of

TE

1. For an ECL formula P with state variables s1 ; : : : ; sn and pre xes 1 ; : : : ; n 2 ? fOg, P 1 =s1 ; : : : ; n =sn] is a TE -path formula. 2. With s : P and s : P a TE -path formula and a pre x, s : P and s : P are TE -path formulas.

Tableau Formulas).

3. For a TE -path formula P and 2 ? fOg, :P is a TE -pre xed formula. 4. Every TE -pre xed formula which does not contain O is also a TE -node formula. 5. With 0 ; 1 ; : : : pre xes and Li a conjunction of TE -pre xed formulas, ^ 0 ; L0 ; 1 ; L1 ; : : : ; n ; Ln ; 1] is a TE -path information formula. 6. Every TE -path information formula is a TE -node formula. Remark 2 (Properties of TE formulas). Note that, TE -path formulas do not contain any free state variables, and the restricted quanti ers s and s occur only in the outermost positions of TE -path formulas.

De nition 10 (Semantics of TE Tableau Formulas). The relation j= of a j = linear Kripke structure with a transition oracle K = (U ; M ), a pre x interpretation , a variable assignment , and a TE -node formula is de ned as follows: For every TE -path formula e neither containing O nor beginning with s or s and every pre x : let 1 ; : : : ; n be the pre xes occurring in e, s1 ; : : : ; sn new state variables and =fsj 7! ( j ; ) j 1 j ng. Then, (K ; ; ) jj = :e :, there is an i 2 I = N f1g s.t.

(K (

; ); ( ; )+1 ; ) = e ; i.e., if the transition from ( ; ) to ( ; )+1 satis es e under .) For every -path formula beginning with s or s and every pre x ,

(K ) jj = = :

(In particular, for an action formula e,

; ); i]; ;

(

)j =

e s1 =

1

; : : : ; sn = n ] :

j

; ;

e

:,

(K h

i

TE

(K

; ; (K ; ;

P ^=s] for some i ( ; ); ^ ) = = : : ) = = :P ^=s] for all i ( ; ) : For every path information formula I = 0 ; L0; 1 ; L1 ; : : : ; n ; Ln; ^ ]: (K ; ; ) = = 0 ; L 0 ; 1 ; L 1 ; : : : ; n ; Ln ; ^ ] i ( 0 ; ) = 0 and for all 0 i n: ( i; ) < ( i+1 ; ) , and for all j with ( i; ) < j < ( i+1 ; ) : ^ (K ; j ; ) = Li ^=O] with ^ a new 0-ary pre x symbol. = This condition means that for all ( nitely, but arbitrary many) states j situated between ( i ; ) and ( i+1 ; ) in K , the instantiation of Li for a new pre x which is mapped to j holds in K . Note that Li = false implies ( i+1 ; ) = ( i ; )+1.

) jj = =

jj

:

s :P s :P

:, (K

,

; (K ;

jj

f ^7! g

f 7! g

i; i;

) jj = =

jj

:

1

1

f

7!

g

jj

Note that the semantics for -pre xed formulas containing O is not de ned. They occur only in the list components of path information formulas, and O is instantiated by a pre x when the list is used. A set of path information formulas and pre xed formulas is valid in a linear Kripke structure K = (U ; M ) under a variable assignment if there is

TE F

a pre x-interpretation such that (K ; ; ) = . Since a branch of a tableau = is a set of formulas like this, validity is a relation on Kripke structures with transition oracles and branches. The construction of Kripke structures and consistent pre x-interpretations to a given set of formulas plays an important role in the proof of correctness.

jj F

5 The Tableau Calculus TE

As usual, the tableau is initialized with a set of formulas which should be proven to be inconsistent, i.e., it is shown that there is no linear Kripke 0 structure K = (U ; M ) such that F does holds in M (0). Thus ^; true; ] ^:F 0 the initialization of the tableau is

1

The -, -, -, -rules for rst-order formulas are as usual (extended with prexes), boolean combinations of pre xed formulas are resolved analogously. Atomic Closure Rule. For a substitution and a pre x , is the localization, i.e. (X ) is obtained from (X ) by replacing every function symbol c by its localized symbol f . So f :A the substitutes in contain only func:B tion symbols which are interpreted state(A) = (B ) independently. In the rule shown at the close right, is a substitution and A; B are atomic apply to the whole tableau. formulas. For resolving modalities, the information about the frame of the Kripke structure, which is encoded in the pif s, is used. In a single step, a pre xed formula is resolved along a pif, inducing the following form of tableau rules: pre xed formula where the premise takes the latest pif on the path information formula current branch. The connection between the prexed formula being resolved and the pif is espre xed formulas path information formulas tablished by the pre x.

2 n :

In the sequel, T denotes the current branch of the tableau, free(T ) the free variables on T , ^ is a new pre x symbol, and e is an ECL-formula. Pre xed Event Formulas. For a pre xed event formula, the pre x must coincide with the respective pre x of the pre xed formula in the :( e) tableau (i.e., : e) requires .1 (Here and in the following, evaluates to close if and are di erent :e pre xes, and to true otherwise.) Post xed Event Formulas. For a post xed formula e , it has to be distinguished whether e is elementary, i.e., a delay, a deadlock, an action formula,

1

here, the reader is asked to distinguish between a pre x post xing a formula by e or e .

:

e

and pre xing or

or a rst-order formula, or whether it is itself a complex event. The post xingoperator associates a synchronization point with the last elementary component of an event. Thus, post xes can only be resolved if this nal event is associated with a transition, otherwise, the formula has to be rewritten. The base cases also act as closure rules if the assignment of pre xes is inconsistent: :e ; len(e) = 1 ; :@ :F ; len(F ) = 0

:::; ; L; ; :::] :::; ; false; ; :::]

:

f g f g

:

F

:::;

close

; :::; ; :::]

e

De nition 11 (Normal Form wrt. Post xes). The syntactic operator rewrites post xed complex ECL formulas such that len(e) \ f2; 3; :::g 6= ; by moving the post x inside the outermost event connective: ) if len(e) ((e t) s) := (e( (te s) s) otherwise2;ff0g; f1gg ; t ((t e) s) := t (e s) ; ((e? ) s) := true s + e? (e s) ;

((e

f) f) ((e + f)

((e

s) := e (f s) ; s) := (e s) (f s) ; s) := (e s) + (f s) ;

((9

((8 ((

f g

x : e) s) := x : e) s) := s0 : e) s) :=

9

8

x : (e s) ; x : (e s) ; s0 : (e s) :

f g

Note that formulas of length len(e) = 0 are (possibly pre- or post xed) rstorder formulas or temporal implications, and formulas of len(e) = 1 are (possibly pre- or post xed) action formulas. Thus, is the identity on temporal implications e ; f (since len(e ; f) = 0 ). Post xing of formulas of the form s : e is not de ned. @ is not a complex event formula. The above de nition is not recursive, but denotes only a one-level rewriting of the parse-tree of the formula (which is typical for tableau calculi) does not occur on the right hand side. Only when is iterated, a normal form is obtained:

f g

Proposition 3 (Normal Form wrt. Pre xes and Post xes). For every lin-

These connectives are disjunctive and conjunctive, respectively, and are resolved analogously to the - and -rules of rst-order tableau calculi:

Alternative and parallel compositions.

:

ear Kripke structure K , ECL formula e, variable assignment and assignment of state variables, (K i; j ]; ; ) j= e , (K i; j ]; ; ) j= (e) and iterated application of yields an expression where only formulas e s.t. len(e) 2 ff0g; f1gg or delays are post xed. In non-base cases, the operator is :e ; len(e) \ f2; 3; :::g 6= ; applied for rewriting the formula: : (e )

e1

:

P

i=1:::n ei ::: : en

: (e1 : :

.. .

e1 en

:::

en )

f. Semantically, the brackets around composite events of the form ( :::ei ) and (e1 ::: en ) can be regarded as synchronization points, i.e., (virtual) entities in the sense of the tableau representation: Detecting an event e f in is equivalent to the event :e f s : (e s) (s f) where s must be bound to a state after the current state. : s : (e s) (s f) With the rules for (see below), the state variable in : s : (e s) (s f) is instan: (e ) ( f) tiated systematically with the pre xes. Then, :e the resulting formula : (e ) ( f) can be :f split into two parts ( sequential conjunction ). Shortcuts can be de ned when one of the events is a base case, i.e., a delay, a rst-order formula, or an action formula. Iterative Composition. Iterative composition is : e? reduced to sequential composition: : true :e e?

Sequential Composition: e P

Due to the fact that there is a linear ordering between states, the - and -rules cannot be adapted to temporal quanti cation of synchronization points; instead, every synchronization point must be integrated into this ordering. For this, analogous to the resolving of eventuality formulas in the tableau calculus for CTL, synchronization points are shifted along path formulas. The rules correspond to a systematic application of the - or -rules, known from rst-order tableau calculi for universal and existential quanti cation, along the state sequence. : s :e Expl.: e O=s] holds for all : s:e :::; ; L; ; :::] subsequent states i.e., : s :e for , for all unknown :::; ; L : e O=s]; ; :::] states between and , : e =s] : s:e and for all states . if = : : s : e : s :e

^ 6 1

Temporal Quanti cation.

state between and which becomes named in this case, or some state . Here, the second part of the consequence of the rule for s names a state ^(free(T )) which is considered to be relevant (since it is a possible instantiation of s). In this case, the list L in the path information formula states some requirements on all states on a path segment thus, also on ^(free(T )). These are made explicit by instantiating L with ^(free(T ))=O.

s :e ; L; ; :::] : e =s] :::; ; L : e O=s] ; ; if = : ^(free(T )); L; ; :::] :::; ; L : e O=s] ; ; ; :::] : e =s] ; L ^(free(T ))=O] : s :e : (e =s] ; ) ^(free(T ))=s] :e Expl.: e O=s] holds for some subsequent state thus, this must be , or some

:::;

:

^ ? 6 1 ^ ? ? ?

Temporal Implication. When resolving constraints e ; f, in the base case,

e

is a rst-order formula or an action formula or a delay: for e a rst-order formula :e;f or an action formula: : e :e

:

^: 0

f

: ^ 0:

@;f

f

By applying the following rules, constraints are rewritten until the antecedent consists only of a rst-order formula or an action formula:

:( :

e) ; f

6

: (e+f) :

e;f

e;g :f;g

;g

:( :

s

s : e) ; f

: (e

; f)

4

: (e ^ : (f 0 :

;

e

?)

; f) ; g :e;f

^: 0

g

Expl.: if e implies f then g holds, if either e ; : s : ((e s) ; (@ s f ; g)) f does not hold i.e, e is detected and f cannot be : ((e f) ; g) detected, or e ; f hold : s : (( e s) ; (@ f s ; g)) and g can be detected. Post xed event formulas require additional attention: base cases can be resolved immediately, non-base cases have to be rewritten: : (e ) ; f ; len(e) = 0 : (@ );f

: (e

f) ; g

f g

6

: : (e

e;f

^: 0

f

6

; L; ; :::] ^(free(T )); L; ; :::] :::; ; false; ; :::] :::; ; false; L ^(free(T ))=O]

:

:::;

)

; f ; len(e) =

f1g

Expl.: First case: is the next known state thus, is later than +1, then e cannot be detected in . Second case: = is the next known state, but not the successor state.

6

e;f

:::;

:(

@

^: 0

; :::; ; :::]

f

)

;f

:::;

:(

@

close

; :::; ; :::]

)

;f

len(e) \ f2; 3; :::g 6= ;

: (e )

: (e

)

;f

;f

f

Some constraints show a special behavior: Since e? has trivial occurrences, e? ; f reduces to 0 : f:

:

^: 0

e?

;f

Events of the form s : e cannot be nitely detected, thus, implications containing them in the antecedent have to be resolved in a di erent way. : ( s : e) ; f is equivalent to the fact that either there is a state : ( s : e) ; f later than such that : e =s] does not occur, or : s : (e ; ) ^ : f 0 K satis es f:

?

Remark 3 (Properties of ). has some special properties which can easily be veri ed when carefully looking at the rules: every pre x symbol is introduced exactly once, with a given arity and the current free variables of the branch as arguments. Thus, for every pre x symbol, at every time, there is exactly one pre x which is built from it. every pre x which occurs as pre x or post x in some formula (i.e., as e or e ) of a branch occurs also in the most recent path information formula of the branch. if a branch of the tableau contains a formula of the form : or : :P , = , the most recent path information formula on this branch is of the form : : : ; ; : : : ; ; : : : ]. there are no free state variables in the calculus: Whereas rst-order variables are replaced by free variables or Skolem terms, state variables are always replaced by pre xes (see the rules for and ).

TE TE 6

(a) If a tableau T is satis able and T 0 is created from T by an application of any of the rules mentioned above, then T 0 is also satis able. (b) If there is any closed tableau for F , then F is unsatis able.

Theorem 1 (Correctness of TE ).

The proof (see May98]) of (a) is done by case-splitting separately for each of the rules. By assumption, there is a Kripke structure K with a transition oracle and a pre x interpretation such that for every variable assignment there is a branch T in with (K ; ; ) = T . In all cases apart from the atomic = closure rule, K and are extended such that they witness the satis ability of 0 . In case of the atomic closure rule, a Substitution Lemma guarantees the existence of a satisfying branch for every variable assignment to free( 0 ). (b) follows directly from (a). Since rst-order ECL is not compact, no calculus for it can be complete. The calculus is complete modulo inductive properties. For such cases, induction rules for temporal properties and well-founded data structures have to be included. In this setting, the notion of completeness has to be relativized to that any proof done in a mathematical way can be completely redone formally.

T jj T T

6 Conclusion

This paper presents a tableau calculus for a linear time temporal logic which is based on temporal connectives instead of modal operators. The underlying Kripke semantics is explicitely encoded into the tableau, based on the ideas of the tableau representation of branching-time structures in MS96,May97]. In both calculi, exactly those states which are required to construct a potential model of the given formula are named explicitly, all states in-between are characterized intensionally within the path information. From the conceptual point of view, the contribution of the paper is that this tableau representation is both suitable

for modal temporal logics and for logics using temporal connectives and explicit temporal quanti cation. Focusing on temporal connectives, the logic and the calculus show how temporal connections between events can be modeled explicitly by synchronization points. The calculus integrates this synchronization smoothly into the tableau semantics via the introduction of state variables. With the and operators, the handling of state variables is closely related to the strategy for resolving the CTL modalities 2 and 3, making up one more connection between the calculus presented here and the CTL calculus. Due to its path-orientation, the language is signi cantly di erent from CTL which is based on state-formulas. Although, the tableau semantics and calculus shares its basic ideas with the CTL calculus, allowing a potential integration of both calculi.

References

BK94. A. J. Bonner and M. Kifer. An Overview of Transaction Logic. Theoretical Computer Science, 133(2):205 265, 1994. BT98. H. Bowman and S. Thompson. A Tableau Method for Interval Temporal Logic with Projection. In Tableaux'98, LNCS 1397, pp. 108 123, Springer, 1998. CT98. J. Chomicki and D. Toman. Temporal Logic in Information Systems. In Logics for Databases and Information Systems, Ch. 3, pp. 31 70. Kluwer, 1998. Fit90. M. Fitting. First Order Logic and Automated Theorem Proving. Springer,1990. Jab94. S. Jablonski. Functional and Behavioural Aspects of Process Modelling in Work ow Management Systems. Proc. CON '94: Work ow Management,1994. May97. W. May. Proving Correctness of Labeled Transition Systems by Semantic Tableaux. In Tableaux'97, LNCS 1227, pp. 261 275. Springer, 1997. May98. W. May. Integrated Static and Dynamic Modeling of Processes. PhD thesis, Institut f r Informatik, Universit t Freiburg, Logos Verlag, 1998. Mos86. B. Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, 1986. MP95. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer, 1995. MS96. W. May and P. H. Schmitt. A Tableau Calculus for First-Order Branching Time Logic. In Intl. Conf. on Formal and Applied Practical Reasoning, FAPR'96, LNCS 1085, pp. 399 413. Springer, 1996. Pra90. V. R. Pratt. Action Logic and Pure Induction. In Logics in AI: Europ. Workshop Jelia 90, LNCS 478, pp. 97 120, 1990. SGL97. P. H. Schmitt and J. Goubault-Larrecq. A Tableau System for Linear-Time Temporal Logic. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1217, Springer, pp. 130 144, 1997. Sin95. M. P. Singh. Semantical Considerations on Work ows: An Algebra for Intertask Dependencies. In Intl. Workshop on Database Programming Languages, Electronic Workshops in Computing, Gubbio, Italy, 1995. Springer. TN96. D. Toman and D. Niwinski. First-Order Queries over Temporal Databases Inexpressible in Temporal Logic. In Proc. Int. Conf. on Extending Database Technology, LNCS 1057, pp. 307 324. Springer, 1996. Wol85. P. Wolper. The Tableau Method for Temporal Logic. Logique et Analyse, 28:110 111, 1985.