Campenhout. Reasoning with temporal logic on truncated paths

发布时间:2021-10-23 22:00:19

Reasoning with Temporal Logic on Truncated Paths
Cindy Eisner1 Dana Fisman1,2? John Havlicek3 1 4 Yoad Lustig Anthony McIsaac David Van Campenhout5
1 3

??

2 IBM Haifa Research Lab Weizmann Institute of Science 4 Motorola, Inc. STMicroelectronics, Ltd. 5 Verisity Design, Inc.

Abstract. We consider the problem of reasoning with linear temporal logic on truncated paths. A truncated path is a path that is ?nite, but not necessarily maximal. Truncated paths arise naturally in several areas, among which are incomplete veri?cation methods (such as simulation or bounded model checking) and hardware resets. We present a formalism for reasoning about truncated paths, and analyze its characteristics.

1

Introduction

Traditional ltl semantics over ?nite paths [15] are de?ned for maximal paths in the model. That is, if we evaluate a formula over a ?nite path under traditional ltl ?nite semantics, it is because the last state of the path has no successor in the model. One of the consequences of extending ltl [16] to ?nite paths is that the next operator has to be split into a strong and a weak version [15]. The strong version, which we denote by X!?, does not hold at the last state of a ?nite path, while the weak version, which we denote by X?, does. In this paper, we consider not only ?nite maximal paths, but ?nite truncated paths. A truncated path is a ?nite path that is not necessarily maximal. Truncated paths arise naturally in incomplete veri?cation methods such as simulation or bounded model checking. There is also a connection to the problem of describing the behavior of hardware resets in temporal logic, since intuitively we tend to think of a reset as somehow cutting the path into two disjoint parts a ?nite, truncated part up until the reset, and a possibly in?nite, maximal part after the reset. Methods of reasoning about ?nite maximal paths are insu?cient for reasoning about truncated paths. When considering a truncated path, the user might want to reason about properties of the truncation as well as properties of the model. For instance, the user might want to specify that a simulation test goes on long enough to discharge all outstanding obligations, or, on the other hand, that an
?

??

The work of this author was supported in part by the John Von Neumann Minerva Center for the Veri?cation of Reactive Systems. E-mail addresses: eisner@il.ibm.com (C. Eisner), dana@wisdom.weizmann.ac.il (D. Fisman), john.havlicek@motorola.com (J. Havlicek), yoadl@il.ibm.com (Y. Lustig), anthony.mcisaac@st.com (A. McIsaac), dvc@verisity.com (D. Van Campenhout).

2

obligation need not be met if it “is the fault of the test” (that is, if the test is too short). The former approach is useful for a test designed (either manually or by other means) to continue until correct output can be con?rmed. The latter approach is useful for a test which has no “opinion” on the correct length of a test - for instance, a monitor running concurrently with the main test to check for bus protocol errors. At ?rst glance, it seems that the strong operators (X! and U) can be used in the case that all outstanding obligations must be met, and the weak operators (X and W) in the case that they need not. However, we would like a speci?cation to be independent of the veri?cation method used. Thus, for instance, for a speci?cation [p U q], we do not want the user to have to modify the formula to [p W q] just because she is running a simulation. In such a situation, we need to de?ne the semantics over a truncated path. In other words, at the end of the truncated path, the truth value must be decided. If the path was truncated after the evaluation of the formula completed, the truth value is already determined. The problem is to decide the truth value if the path was truncated before the evaluation of the formula completed, i.e., where there is doubt regarding what would have been the truth value if the path had not been truncated. For instance, consider the formula Fp on a truncated path such that p does not hold for any state. Another example is the formula Gq on a truncated path such that q holds for every state. In both cases we cannot be sure whether or not the formula holds on the original untruncated path. We term a decision to return true when there is doubt the weak view and a decision to return false when there is doubt the strong view. Thus in the weak view the formula Fp holds for any ?nite path, while Gq holds only if q holds at every state on the path. And in the strong view the formula Fp holds only if p holds at some state on the path, while the formula Gq does not hold for any ?nite path. Alternatively, one can take the position that one should demand the maximum that can be reasonably expected from a ?nite path. For formulas of the form Fp, a pre?x on which p holds for some state on the path is su?cient to show that the formula holds on the entire path, thus it is reasonable to demand that such a pre?x exist. In the case of formulas of the form Gq, no ?nite pre?x can serve as evidence that the formula holds on the entire path, thus requiring such evidence is not reasonable. Under this approach, then, the formula Fp holds only if p holds at some state on the path, while the formula Gq holds only if q holds at every state on the path. This is exactly the traditional ltl semantics over ?nite paths [15], which we term the neutral view. In this paper, we present a semantics for ltl over truncated paths based on the weak, neutral, and strong views. We study properties of the truncated semantics for the resulting logic ltltrunc , as well as its relation to the informative pre?xes of [12]. We examine the relation between truncated paths and hardware resets, and show that our truncated semantics are mathematically equivalent to the reset semantics of [3]. The remainder of this paper is structured as follows. Section 2 presents our truncated semantics. Section 3 studies properties of our logic as well as its relation

3

to the informative pre?xes of [12]. Section 4 shows the relation to hardware resets. Section 5 discusses related work. Section 6 concludes.

2

The truncated semantics

Recall that ltl is the logic with the following syntax: De?nition 1 (ltl formulas). – Every atomic proposition is an ltl formula. – If ? and ψ are ltl formulas then the following are ltl formulas: ? ?? ? ?∧ψ ? X! ? ? [? U ψ] Additional operators are de?ned as syntactic sugaring of the above operators: def def def ? ? ∨ ψ = ?(?? ∧ ?ψ) ? ? → ψ = ?? ∨ ψ ? X ? = ?(X! ??) ? F ? = [true U ?]
def

? G ? = ?F ??

def

? [? W ψ] = [? U ψ] ∨ G?

def

According to our motivation presented above, the formula ? holds on a truncated path in the weak view if up to the point where the path ends, “nothing has yet gone wrong” with ?. It holds on a truncated path in the neutral view according to the standard ltl semantics for ?nite paths. In the strong view, ? holds on a truncated path if everything that needs to happen to convince us that ? holds on the original untruncated path has already occurred. Intuitively then, our truncated semantics are related to those of standard ltl on ?nite paths as follows: the weak view weakens all operators (e.g. U acts like W, X! like X), the neutral view leaves them unchanged, and the strong view strengthens them (e.g. W acts like U, X like X!). We de?ne the truncated semantics of ltl formulas over words1 from the alphabet 2P . A letter is a subset of the set of atomic propositions P such that true belongs to the subset and false does not. We will denote a letter from 2P by ? and an empty, ?nite, or in?nite word from 2P by w. We denote the length of word w as |w|. An empty word w = ? has length 0, a ?nite word w = (?0 ?1 ?2 · · · ?n ) has length n + 1, and an in?nite word has length ∞. We denote the ith letter of w by wi?1 (since counting of letters starts at zero). We denote by wi.. the su?x of w starting at wi . That is, wi.. = (wi wi+1 · · · wn ) or wi.. = (wi wi+1 · · ·). We denote by wi..j the ?nite sequence of letters starting from wi and ending in wj . That is, wi..j = (wi wi+1 · · · wj ). We make use of an “over?ow” and “under?ow” for the indices of w. That is, wj.. = ? if j ≥ |w|, and wj..k = ? if j ≥ |w| or k < j. For example, in the semantics of [? U ψ] under weak context, when we say “?k”, k is not required to be less than |w|. The truncated semantics of an ltl formula are de?ned with respect to ?nite or in?nite words and a context indicating the strength, which can be either
1

Relating the semantics over words to semantics over models is done in the standard way. Due to lack of space, we omit the details.

4

weak, neutral or strong. Under the neutral context only non-empty words are evaluated; under weak/strong contexts, empty words are evaluated as well. We S use w |= ? to denote that ? is satis?ed under the model (w, S), where S is “?” if the context is weak, null if it is neutral, and “+” if it is strong. We use w to denote an empty, ?nite, or in?nite word, ? and ψ to denote ltl formulas, p to denote an atomic proposition, and j and k to denote natural numbers. holds weakly: For w such that |w| ≥ 0, 1. 2. 3. 4. 5. w w w w w |= p ?? |w| = 0 or p ∈ w0 ? + |= ?? ?? w |= ? / ? ? ? |= ? ∧ ψ ?? w |= ? and w |= ψ ? ? |= X! ? ?? w1.. |= ? ? ? ? |= [?Uψ] ?? ?k such that wk.. |= ψ, and for every j < k, wj.. |= ?
?

holds neutrally: For w such that |w| > 0, 1. 2. 3. 4. 5. w w w w w |= p ?? p ∈ w0 |= ?? ?? w |= ? / |= ? ∧ ψ ?? w |= ? and w |= ψ |= X! ? ?? |w| > 1 and w1.. |= ? |= [?Uψ] ?? ?k < |w| such that wk.. |= ψ, and for every j < k, wj.. |= ?

holds strongly: For w such that |w| ≥ 0, 1. 2. 3. 4. 5. w w w w w |= p ?? |w| > 0 and p ∈ w0 + ? |= ?? ?? w |= ? / + + + |= ? ∧ ψ ?? w |= ? and w |= ψ + + |= X! ? ?? w1.. |= ? + + + |= [?Uψ] ?? ?k such that wk.. |= ψ, and for every j < k, wj.. |= ?
+

Our goal was to give a semantics to ltl formulas for truncated paths, but we have actually ended up with two parallel semantics: the neutral semantics, and the weak/strong semantics. The weak/strong semantics form a coupled dual pair because the negation operator switches between them. Before analyzing these semantics, we ?rst unify them by augmenting ltl with truncate operators that connect the neutral semantics to the weak/strong semantics. Intuitively, trunc w truncates a path using the weak view, while trunc s truncates using the strong view. Formally, ltltrunc is the following logic, where we use the term boolean expression to refer to any application of the standard boolean operators to atomic propositions, and we associate satisfaction of a boolean expression over a letter wi with satisfaction of the boolean expression over the word wi..i . De?nition 2 (ltltrunc formulas). – Every atomic proposition is an ltltrunc formula.

5

– If ? and ψ are ltltrunc formulas and b is a boolean expression, then the following are ltltrunc formulas: ? ?? ? ?∧ψ ? X! ? ? [? U ψ] ? ? trunc w b We also add the dual of the trunc w operator as syntactic sugar as follows: ? trunc s b = ?(?? trunc w b) The semantics of the standard ltl operators are as presented above. The semantics of the truncate operator are as follows: – w |= ? trunc w b ?? w |= ? or ?k < |w| s.t. wk |= b and w0..k?1 |= ? – w |= ? trunc w b ?? w |= ? or ?k < |w| s.t. wk |= b and w0..k?1 |= ? – w |= ? trunc w b ?? w |= ? or ?k < |w| s.t. wk |= b and w0..k?1 |= ? Thus, trunc w performs a truncation and takes us to the weak view, and, as we show below, trunc s performs a truncation and takes us to the strong view. There is no way to get from the weak/strong views back to the neutral view. This corresponds with our intuition that once a path has been truncated, there is no way to “untruncate” it.
+ + ? ? ? ? ?

def

3

Characteristics of the truncated semantics

In this section, we study properties of the truncated semantics as well as its relation to the informative pre?xes of [12]. All theorems are given here without proof; the proofs can be found in the full version of the paper. We ?rst examine relations between the views. The ?rst theorem assures that the strong context is indeed stronger than the neutral, while the neutral is stronger than the weak. Theorem 3 (Strength relation theorem). Let w be a non-empty word. 1. w |= ? =? w |= ? ? 2. w |= ? =? w |= ? The proof, obtained by induction on the structure of the formula, relies on the following lemma. Lemma 4 Let ? be a formula in ltltrunc . Then both ? |= ? and ? |= ?. / The following corollary to Theorem 3 states that for in?nite paths, the weak/neutral/strong views are the same. Recall that the neutral view without the trunc w operator is that of standard ltl over ?nite and in?nite paths. Thus, for ltltrunc formulas with no truncation operators (that is, for ltl formulas), Corollary 5 implies that all three views are equivalent over in?nite paths to standard ltl semantics. Corollary 5 If w is in?nite, then w |= ? i? w |= ? i? w |= ?.
? + ? + +

6

Intuitively, a truncated path w satis?es ? in the weak view if w “carries no evidence against” ?. It should then follow that any pre?x of w “carries no evidence against” ?. Similarly, w satis?es ? in the strong view if it “supplies all the evidence needed” to conclude that ? holds on the original untruncated path. Hence any extension of w should also “supply all evidence needed” for this conclusion. The following theorem con?rms these intuitive expectations. We ?rst formalize the notions of pre?x and extension. De?nition 6 (Pre?x, extension). u is a pre?x of v, denoted u v, if there exists a word u′ such that uu′ = v. w is an extension of v, denoted w v, if there exists a word v ′ such that vv ′ = w. Theorem 7 (Pre?x/extension theorem). 1. v |= ? ?? ?u + 2. v |= ? ?? ?w
? ?

v, u |= ? + v, w |= ?

We now examine our intuitions regarding some derived operators. Since the trunc w operator takes us to the weak view, we expect the trunc s operator to take us to the strong view. The following observation con?rms our intuition by capturing directly the semantics of the trunc s operator. Observation 8 – w |= ? trunc s b ?? w |= ? and ?k < |w| if wk |= b then w0..k?1 |= ? + – w |= ? trunc s b ?? w |= ? and ?k < |w| if wk |= b then w0..k?1 |= ? + + + – w |= ? trunc s b ?? w |= ? and ?k < |w| if wk |= b then w0..k?1 |= ? The following observation shows that our intuitions regarding F and G on truncated paths hold. In particular, F? holds for any formula ? in weak context on a truncated path, and G? does not hold for any formula ? in strong context on a truncated path. Observation 9 ? w |= F? ?? ?k s.t. wk.. |= ? ? w |= F? ?? ?k < |w| s.t. wk.. |= ? ? w |= F? ?? ?k s.t. wk.. |= ?
+ + ? ? ? ? +

? w |= G? ?? ?k, wk.. |= ? ? w |= G? ?? ?k < |w|, wk.. |= ? ? w |= G? ?? ?k, wk.. |= ?
? + + +

?

?

Note that for k ≥ |w|, wk.. = ? and by Lemma 4, ? |= ? and ? |= ? for every ?. / Thus Observation 9 shows that for every formula ? and for every ?nite word w, ? + w |= F? and w |= G?. / We have already seen that for in?nite words, the semantics of the weak/neutral/strong contexts are equivalent and, in the absence of truncation operators, are the same as those of standard ltl. The following observations show that for ?nite words, the strength of an operator matters only in the neutral context since in a weak context every operator is weak (U acts like W and X! acts like X) and in a strong context every operator is strong (W acts like U and X acts like X!).

7

Observation 10 Let w be a ?nite word. ? w |= X? ?? w |= ?(X! ??) ? w |= X? ?? w |= X! ? ? w |= X? ?? w |= X! ?
? ? + +

? w |= [?Uψ] ?? w |= ?[?ψW(?? ∧ ?ψ)] ? w |= [?Uψ] ?? w |= [?Wψ] ? w |= [?Uψ] ?? w |= [?Wψ]
? ? + +

A consequence of this is that under weak context it might be the case that both ? and ?? hold, while under strong context it might be the case that neither ? nor ?? holds. It follows immediately that ?∧?? may hold in the weak context, while ?∨?? does not necessarily hold in the strong context. For example, let ? = XXp. ? + Then on a path w of length 1, w |= ? ∧ ??, and w |= ? ∨ ??. This property of / the truncated semantics is reminiscent of a similar property in intuitionistic logic [6], in which ? ∨ ?? does not necessarily hold. We now argue that the truncated semantics formalizes the intuition behind the weak, neutral and strong views. Recall that one of the motivating intuitions for the truncated semantics is that if a path is truncated before evaluation of ? “completes”, then the truncated path satis?es ? weakly but does not satisfy ? strongly. If the evaluation of ? “completes” before the path is truncated, then the truth value on the truncated path is the result of the evaluation. Thus, in order to claim that we capture the intuition we need to de?ne when the evaluation of a formula completes. In other words, given a word w and a formula ? we would like to detect the shortest pre?x of w which su?ces to conclude that ? holds or does not hold on w. We call such a pre?x the de?nitive pre?x of ? with respect to w. De?nition 11 (De?nitive pre?x). Let w be a non-empty path and ? a formula. The de?nitive pre?x of w with respect to ?, denoted dp(w, ?), is the shortest ?nite pre?x u w such that ? + u |= ? ?? u |= ? ?? u |= ? if such u exists and ? otherwise. Intuitively, if w is ?nite and dp(w, ?) = ?, then even after examination of all of w, our decision procedure leaves doubt about the dispositions of both ? and ?? on w. Therefore, both are satis?ed weakly on w, neither is satis?ed strongly on w, and all of w is needed to determine which one is satis?ed neutrally on w. If dp(w, ?) = ?, then for ?nite or in?nite w, examination of dp(w, ?) is exactly enough for our decision procedure to resolve without doubt the truth value of ? over any pre?x v of w such that v dp(w, ?). Therefore, any proper pre?x of dp(w, ?) satis?es weakly both ? and ??, while dp(w, ?) satis?es strongly exactly one of ? or ??, as do all of its extensions. The following theorem states this formally: Theorem 12 (De?nitive pre?x theorem). Let v be a non-empty word and ? an ltltrunc formula. – If dp(v, ?) = ? then ? ? ? u ? dp(v, ?) =? u |= ? and u |= ??

8

? u dp(v, ?) =? u |= ? or u |= ?? – Otherwise ? ? + + ? for every ?nite u v, (u |= ? and u |= ??) and (u |= ? and u |= ??) / / Plainly, dp(w, ?) = dp(w, ??). If u is the de?nitive pre?x of w with respect to ?, then it is its own de?nitive pre?x with respect to ?. That is: Proposition 13 Let w be a non-empty word and ? an ltltrunc formula. Then dp(w, ?) = ? =? dp(w, ?) = dp(dp(w, ?), ?) The de?nitive pre?x of the truncated semantics is closely related to the concept of informative pre?x in [12]. That work examines the problem of model checking safety formulas for standard ltl over maximal paths. Let a safety formula be a formula ? such that any path w violating ? contains a pre?x w0..k all of whose in?nite extensions violate ? [15]. Such a pre?x is termed a bad pre?x by [12]. Our intuitive notion of a bad pre?x says that it should be enough to fully explain the failure of a safety formula. However, [12] showed that for ltl over maximal paths, there are safety formulas for which this does not hold. For instance, consider the formula ? = (G(q ∨ FGp) ∧ G(r ∨ FG?p)) ∨ Gq ∨ Gr. In standard ltl semantics, ? is equivalent to Gq ∨ Gr, and the bad pre?xes are exactly the ?nite words satisfying ?(Gq ∨ Gr). However, we somehow feel that such a pre?x is too short to “tell the whole story” of formula ? on path w, because it does not explain that (FGp) ∧ (FG?p) is unsatis?able. The concept of a pre?x which tells the whole story regarding the failure of formula ? on path w is formalized by [12] as an informative pre?x. The precise de?nition in [12] is inductive over the ?nite path and the structure of ??, which is assumed to be in positive normal form. The de?nition accomplishes an accounting of the discharge of the various sub-formulas of ?? and is omitted due to lack of space. From the intuitive description, if u is an informative pre?x + ? for ?, then we should have that u |= ??, or equivalently, u |= ?. The following / theorem con?rms this expectation and its converse. Theorem 14 (Informative pre?x theorem). Let w be a non-empty ?nite word and ? an ltl formula. w |= ? ?? w is informative for ? / Notice that Theorem 14 shows that the notion of informative pre?x for ?, de?ned in terms of syntactic structure, is captured semantically by the weak/strong truncated semantics. Furthermore, the de?nitive pre?x does not require formulas to be in positive normal form, as does the informative pre?x, and is symmetric in ? and ??, as opposed to the informative pre?x, which is de?ned only for formulas that do not hold. The precise relation of de?nitive pre?xes to informative pre?xes is given by the following corollary. Corollary 15 Let w be a non-empty path and let ? be an ltl formula. If dp(w, ?) = ?, then w has no informative pre?x for either ? or ??. Otherwise, dp(w, ?) is the shortest informative pre?x of w for either ? or ??.
?

+

+

9

4

Relation to hardware resets

There is an intimate relation between the problem of hardware resets and that of truncated vs. maximal paths: a hardware reset can be viewed as truncating the path and canceling future obligations; thus it corresponds to the weak view of truncated paths. We now consider the relation between the semantics given to the hardware reset operators of ForSpec [3] (termed the reset semantics by [2]) and of Sugar2.0 [8] (termed the abort semantics by [2]) and the truncated semantics we have presented above. We show that the truncated semantics are equivalent to the reset semantics, thus by [2], di?erent from the abort semantics. Reset semantics The reset semantics are de?ned as follows, where [3] uses accept on as the name of the trunc w operator. Let a and r be mutually exclusive boolean expressions, where a is the condition for truncating a path and accepting the formula, and r is the condition for rejection. Let w be a non-empty word2 . As before, we use ? and ψ to denote ltltrunc formulas, p to denote an atomic proposition, and j and k to denote natural numbers. The reset semantics are de?ned in terms of a four-way relation between words, contexts a and r, and formulas, denoted |= . The de?nition of the reset semantics makes use of a twoR way relation between letters and boolean expressions which is de?ned in the obvious manner. 1. w, a, r |= p ?? w0 |= a ∨ (p ∧ ?r) R R 2. w, a, r |= ?? ?? w, r, a |= ? / R R 3. w, a, r |= ? ∧ ψ ?? w, a, r |= ? and w, a, r |= ψ R R R 4. w, a, r |= X! ? ?? w0 |= a or ( w0 |= r and |w| > 1 and w1.. , a, r |= ? ) / R R R R 5. w, a, r |= [? U ψ] ?? there exists k < |w| such that wk.. , a, r |= ψ, and R R for every j < k, wj.. , a, r |= ? R 6. w, a, r |= ? trunc w b ?? w, a ∨ (b ∧ ?r), r |= ? R R Abort semantics The abort semantics are de?ned in [8] as the traditional ltl semantics over ?nite and in?nite (non-empty) paths, with the addition of a truncate operator (termed there abort), as follows, where we use |= to denote A satisfaction under these semantics: w |= ? trunc w b ?? either w |= ? or there exist j < |w| and word w′ such A A that wj |= b and w0..j?1 w′ |= ? A A Intuitively, the reset and abort semantics are very similar. They both specify that the path up to the point of reset must be “well behaved”, without regard to
2

In [3], the reset semantics are de?ned over in?nite words. We present a straightforward extension to (non-empty) ?nite as well as in?nite words.

10

the future behavior of the path. The di?erence is in the way future obligations are treated, and is illustrated by the following formulas: (G(p → F(? ∧ ??))) trunc w b (G?p) trunc w b (1) (2)

Formulas 1 and 2 are equivalent in the abort semantics, because the future obligation ?∧?? is not satis?able. They are not equivalent in the reset semantics, because the reset semantics “do not care” that ? ∧ ?? is not satis?able. Thus there exist values of w, a, and r such that Formula 1 holds under the reset semantics, while Formula 2 does not. For example, consider a word w such that p holds on w5 and for no other letter and b holds on w6 and on no other letter. If a = r = false, then Formula 1 holds on word w in the reset semantics under contexts a and r, while Formula 2 does not. As shown in [2], the di?erence between the reset and the abort semantics causes a di?erence in complexity. While the complexity of model checking the reset semantics is pspace-complete, the complexity of model checking the abort semantics is space(exp(k, n))-complete where n is the length of the formula and k is the nesting depth of trunc w. Unlike the abort semantics, the truncated and reset semantics make no existential requirements of a path after truncation. The truncated semantics discard the remainder of the path after truncation, while the reset semantics accumulate the truncate conditions for later use. Theorem 16 states that they are the same. Theorem 16 (Equivalence theorem). Let ? be a formula of ltltrunc , a and r mutually exclusive boolean expressions, and w a non-empty word. Then, w, a, r |= ? ?? w |= (? trunc w a) trunc s r R In particular, for an in?nite w, w, false, false |= ? in the reset semantics if R and only if w |= ? in the truncated semantics. It follows easily that the truncated semantics are not more expressive or harder to decide than the reset semantics, which were shown in [2] to have the same expressiveness and complexity as ltl.

5

Related work

Semantics for ltl is typically de?ned over in?nite paths. Often ?nite paths are dealt with by in?nitely repeating the last state (see e.g. [7]). Lichtenstein et al. [14] were the ?rst to extend the semantics of ltl to ?nite paths. In particular, they introduced the strong next operator (see also [13],[15, pages 272-273]). However, they consider only ?nite maximal paths, and the issue of truncated paths is not considered. The issue of using temporal logic speci?cations in simulation is addressed by [1]. They consider only a special class of safety formulas [4] which can be translated into formulas of the form Gp, and do not distinguish between maximal and truncated paths.

11

The idea that an obligation need not be met in the weak view if it “is the fault of the test” is directly related to the idea of weak clocks in [8], in which obligations need not be met if it “is the fault of the clock”. The weak/strong clocked semantics of [8] were the starting point for investigations that have led to [9], which proposes a clocked semantics in which the clock is strengthless, and to the current work, which preserves much of the intuition of the weak/strong clocked semantics in a simpler, unclocked setting. The work described here is the result of discussions in the LRM sub-committee of the Accellera Formal Veri?cation Technical Committee. Three of the languages (Sugar2.0, ForSpec, CBV [10]) examined by the committee enhance temporal logic with operators intended to support hardware resets. We have discussed the reset and abort semantics of ForSpec and Sugar2.0 in detail. The operator of CBV, while termed abort, has semantics similar to those of ForSpec’s accept on/reject on operators. As we have shown, our truncated semantics are mathematically equivalent to the reset semantics of ForSpec. However, the reset semantics take the operational view in that they tell us in a fairly direct manner how to construct an alternating automaton for a formula. Our approach takes the denotational view and thus tells us more directly the e?ect of truncation on the formula. This makes it easy to reason about the semantics in a way that is intuitively clear, because we can reason explicitly about three constant contexts (weak/neutral/strong) which are implicit in the operational view. Bounded model checking [5] considers the problem of searching for counterexamples of ?nite length to a given ltl formula. The method is to solve the existential model checking problem for ψ = ??, where ? is an ltl formula to be checked. An in?nite path π of a model M that shows that M |= Eψ is called a witness for ψ. The existence of a witness has to be demonstrated by exhibiting an appropriate path πk of ?nite length k. In some cases, this can be done by ?nding a path πk with a loop (two identical states); this can be expanded to an in?nite path in which the loop is repeated in?nitely often. But a ?nite path πk can also demonstrate the existence of a witness, even if it is not known to have a loop. This can be understood in the framework of the truncated semantics as follows: The bounded semantics without a loop of [5] is the strong semantics for ltl formulas in positive normal form. If πk satis?es ψ in this semantics, then by Theorems 7 and 3, every extension of πk satis?es ψ in the neutral semantics. Assuming there is at least one transition from every state in M , there is an in?nite extension π of πk that is a computation path of M . Then π is a witness for ψ. Conversely, if there is no path of length k satisfying ψ in the bounded semantics without a loop, then every path of length k weakly satis?es ?. As noted in [5], the bounded semantics without a loop break the duality between strong and weak operators. The truncated semantics provide the missing dual weak semantics, and therefore render unnecessary the restriction of [5] to positive normal form. The completeness threshold (CT ) of [11] is reminiscent of our de?nitive pre?x. However, CT is de?ned with respect to a model and a formula while the de?nitive pre?x is de?ned with respect to a word and a formula. Even if we try to compare the de?nitions by taking for a word w a model Mw that accepts w alone, the

12

de?nitions do not coincide: the de?nitive pre?x for any word with respect to the formula Gp is ? but there exists a model Mw accepting Gp with a bounded CT . In [17] the problem of determining the value of a formula over ?nite paths in simulation is also considered. Their semantics can be formulated using the notion of bad/good pre?xes by de?ning a 3-valued satisfaction that returns true if a good pre?x [12] is seen, false if a bad pre?x is seen and pending otherwise. The resulting semantics is di?erent than the truncated semantics and is quite similar to the abort semantics.

6

Conclusion and future work

We have considered the problem of reasoning in temporal logic over truncated as well as maximal paths, and have presented an elegant semantics for ltl augmented with a truncate operator over truncated and maximal paths. The semantics are de?ned relative to three views regarding the truth value of a formula when the truncation occurs before the evaluation of the formula completes. The weak view is consistent with a preference for false positives, the strong view with a preference for false negatives, and the neutral view with the desire to see as much evidence as can reasonably be expected from a ?nite path. We have studied properties of the truncated semantics for the resulting logic ltltrunc , as well as its relation to the informative pre?xes of [12]. We have examined the relation between truncated paths and hardware resets, and have shown that our truncated semantics are mathematically equivalent to the reset semantics of [3]. Future work is to investigate how the weak/neutral/strong paradigm can be generalized: in particular, whether there are useful correspondences between alternative weak/neutral/strong semantics and other decision procedures for ltl, analogous to that between the truncated semantics and the classical tableau construction. Having a generalized framework, we might be able to ?nd a logic that has the acceptable complexity of the truncated semantics, while allowing rewrite def rules such as (?∧?? = false), which are prohibited in the truncated semantics. In addition, we would like to combine the truncated semantics with those of ltl@ [9], to provide an integrated logic which supports both hardware clocks and hardware resets for both complete and incomplete veri?cation methods.

Acknowledgements
The IBM authors would like to thank Ishai Rabinovitz for many interesting and fruitful discussions, and Shoham Ben-David, Avigail Orni, and Sitvanit Ruah for close review and important comments on an earlier version of this work.

References
1. Y. Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, and Y. Wolfsthal. FoCs - automatic generation of simulation checkers from formal speci?cations. In Proc. 12th International Conference on Computer Aided Veri?cation (CAV), 2000.

13 2. R. Armoni, D. Bustan, O. Kupferman, and M. Y. Vardi. Aborts vs resets in linear temporal logic. In TACAS’03, 2003. To appear. 3. R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M. Y. Vardi, and Y. Zbar. The ForSpec temporal logic: A new temporal property-speci?cation language. In TACAS’02, volume 2280 of LNCS. Springer, 2002. 4. I. Beer, S. Ben-David, and A. Landver. On-the-?y model checking of RCTL formulas. In Proc. 10th International Conference on Computer Aided Veri?cation (CAV), LNCS 1427, pages 184–194. Springer-Verlag, 1998. 5. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 1579. Springer-Verlag, 1999. 6. L. Brouwer. On the Foundations of Mathematics. PhD thesis, Amsterdam, 1907. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics, Amsterdam: North Holland / New York: American Elsevier (1975): 11-101. 7. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Progress on the state explosion problem in model checking. In Informatics - 10 Years Back. 10 Years Ahead (Informatics’01), 2001. 8. C. Eisner and D. Fisman. Sugar 2.0 proposal presented to the Accellera Formal Veri?cation Technical Committee, March 2002. At http://www.haifa.il.ibm.com/ projects/veri?cation/sugar/Sugar 2.0 Accellera.ps. 9. C. Eisner, D. Fisman, J. Havlicek, A. McIsaac, and D. Van Campenhout. The definition of a temporal clock operator. 13th International Colloquium on Automata, Languages and Programming (ICALP), June 2003. To appear. 10. J. Havlicek, N. Levi, H. Miller, and K. Shultz. Extended CBV statement semantics, partial proposal presented to the Accellera Formal Veri?cation Technical Committee, April 2002. At http://www.eda.org/vfv/hm/att-0772/01-ecbv statement semantics.ps.gz. 11. D. Kroening and O. Strichman. E?cient computation of recurrence diameters. In L. Zuck, P. Attie, A. Cortesi, and S. Mukhopadhyay, editors, 4th International Conference on Veri?cation, Model Checking, and Abstract Interpretation, volume 2575 of LNCS, pages 298–309. Springer Verlag, January 2003. 12. O. Kupferman and M. Y. Vardi. Model checking of safety properties. In Proc. 11th International Conference on Computer Aided Veri?cation (CAV), 1999. 13. O. Lichtenstein. Decidability, Completeness, and Extensions of Linear Time Temporal Logic. PhD thesis, Weizmann Institute of Science, 1990. 14. O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Proc. Conf. on Logics of Programs, LNCS 193, pages 196–218. Springer-Verlag, 1985. 15. Z. Manna and A. Pnueli. Temporal Veri?cation of Reactive Systems: Safety. Springer-Verlag, New York, 1995. 16. A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13:45–60, 1981. 17. J. Ruf, D. Ho?mann, T. Kropf, and W. Rosenstiel. Simulation-guided property checking based on a multi-valued ar-automata. In Proceedings of the DATE 2001 on Design, automation and test in Europe, pages 742–748, March 2001.


相关文档

  • Situated nonmonotonic temporal reasoning with BABY-SIT
  • Temporal Reasoning with Abductive Logic Programming
  • Combining propositional logic with maximum entropy reasoning on probability models
  • Diagnosis of Repeated Failures For Discrete Event Systems With Linear-Time Temporal Logic
  • Reasoning with Multi-Version Ontologies A Temporal Logic Approach
  • Temporal reasoning with constraints on fluents and events
  • Executable Temporal Logic for Nonmonotonic Reasoning
  • Formal Reasoning about Actor Programs Using Temporal Logic
  • A Tableau Calculus for a Temporal Logic with Temporal Connectives
  • First-order logic with two variables and unary temporal logic
  • 猜你喜欢

    电脑版