# Terminal Satisfiability in GSTE

Authors: Yongsheng Xu; Guowu Yang; Zhengwei Chang; Desheng Zheng; Wensheng Guo
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

Generalized symbolic trajectory evaluation (GSTE) is an extension of symbolic trajectory evaluation (STE) and a method of model checking. GSTE specifications are given as assertion graphs. There are four efficient methods to verify whether a circuit model obeys an assertion graph in GSTE, Model Checking Strong Satisfiability (SMC), Model Checking Normal Satisfiability (NMC), Model Checking Fair Satisfiability (FMC), and Model Checking Terminal Satisfiability (TMC). SMC, NMC, and FMC have been proved and applied in industry, but TMC has not. This paper gives a six-tuple definition and presents a new algorithm for TMC. Based on these, we prove that our algorithm is sound and complete. It solves the SMC’s limitation (resulting in false negative) without extending from finite specification to infinite specification. At last, a case of using TMC to verify a realistic hardware circuit round-robin arbiter is achieved. Avoiding verifying the undesired paths which are not related to the specifications, TMC makes it possible to reduce the computational complexity, and the experimental results suggest that the time cost by SMC is 3.14× with TMC in the case.


---

## Body

## 1. Introduction

Logic errors found in finite state concurrent systems are extremely important problems for both circuit designers and programmers [1] (i.e., sequential circuit designs and communication protocols). Model checking is a technique for verifying finite state concurrent systems [1]. Symbolic trajectory evaluation is a lattice-based model checking technique based on a form of symbolic simulation [2–4]. STE has shown great promise in verifying medium to large scale industrial hardware designs with a high degree of automation at both the gate level and the transistor level [4–7].Generalized symbolic trajectory evaluation [3, 8] is an extension of symbolic trajectory evaluation [9, 10]. STE is very limited in the types of properties that it can specify and verify. GSTE can handle ω-regular properties and maintain the efficiency and capacity of STE [9–13]. GSTE is originally developed at Intel and has been used successfully on Intel’s next-generation microprocessors [14].The main disadvantage of model checking is the state explosion, which motivates the need for algorithms such as abstract technology and the data structure of BDD and so forth to alleviate it [2, 15–18]. Although a lot of effort has been spent on improving this weakness, the efficient and effective method has yet to be developed. GSTE is a method of model checking and it also has the problem of state explosion. In GSTE, specifications are given as assertion graph and a model is induced by transition relation. Each edge in the model represents a state transition and atrace in the model is a state sequence, while apath in the assertion graph is an edge sequence. In SMC, NMC, and FMC, a model satisfies an assertion graph if all the traces (finite or infinite) in the model are accepted by all the paths of the same length in the assertion graph [3, 8, 19]. Results shown in [1, 9, 15, 17, 20–22] indicate that the method of enumeration usually leads to state explosion and increases the complexity of computing. As we know, traces are induced by model, and the number of traces is directly proportional to the size of model. Furthermore, paths are related to specifications. Thus, it will not need to verify each trace or path. Therefore, the key to alleviating the state explosion lies in deleting some undesired paths and traces. Aiming at this situation, this paper puts forward the filtering approach for TMC (Terminal Satisfiability Model Checking).Previous studies have shown or suggested that a tool is needed to tell the difference between desired paths and undesired paths. One possible method is to chooseE
T as the filter condition, where E
T is the set of edges in assertion graph. Our approach only adds some restricted conditions into assertion graphs without changing the structure of models and assertion graphs. Each edge in the assertion graph is labeled by an antecedent ant
(
e
) and consequent cons
(
e
). Ant
(
e
) and cons
(
e
) are sets of states in the model, so we can assign the states related to specifications to the ant
(
e
) of edge which is in E
T. Then, we can delete undesired paths by E
T. A fuller discussion of TMC will appear in a later section.In this paper, we focus on the need for alleviating state explosion and present a new algorithm for TMC based on GSTE. In Section2, we introduce the basic definitions in GSTE. In Section 3, some concepts such as terminal assertion graph, terminal path, and terminal satisfiability are defined. After a statement of the basic concepts, related properties and a theorem are given. In Section 4, we present an algorithm for verifying terminal satisfiability with an example which cannot be verified by SMC but by TMC. In the end, we use TMC to successfully verify a hardware circuit round-robin arbiter, and the time cost by SMC is 3.14× with TMC in the case. In Section 5, we prove that our algorithm is sound and complete. Section 6 is the conclusion of the paper.


## 2. Preliminaries

We introduce some basic definitions in GSTE [3, 8]. We assume a universal set of finite states, denoted by S.


### 2.1. Model

Definition 1 (transition relation; see [3, 8]).
A relationT
⊆
S
×
S is a transition relation if for all s
∈
S, ∃
s
′
∈
S, (
s
,
s
′
)
∈
T.Definition 2 (model; see [3, 8]).
The modelM induced by the transition relation T is the pair (
pre
,
post
), where(1)
the preimage transformer pre:2
S
→
2
S is defined as
(1)
pre
(
Q
)
=
{
s
∣
∃
s
′
∈
Q
,
(
s
,
s
′
)
∈
T
}
∀
Q
∈
2
S
,
(2)
and the postimage transformer post:2
S
→
2
S is defined as
(2)
post
(
Q
)
=
{
s
′
∣
∃
s
∈
Q
,
(
s
,
s
′
)
∈
T
}
∀
Q
∈
2
S
.Definition 3 (trace; see [3, 8]).
A traceσ in model M
=
(
pre
,
post
) is a state sequence such that σ
[
i
+
1
]
∈
post
(
σ
[
i
]
) for all 1
≤
i
≤
|
σ
|.


### 2.2. Assertion Graph

Definition 4 (assertion graph; see [3, 8]).
An assertion graph is a quintupleG
=
(
V
,
v
0
,
E
,
ant
,
cons
), where V is a finite set of vertices, v
0 is the initial vertex, E
⊆
V
×
V is a set of edges satisfying for all u
∈
V, ∃
v
∈
V, (
u
,
v
)
∈
E, ant is a mapping:   E
→
2
S, and cons is a mapping:    E
→
2
S.Definition 5 (path; see [3, 8]).
A pathρ in assertion graph G is an edge sequence such that ρ
[
i
] ends at a vertex from which ρ
[
i
+
1
] starts for all 1
≤
i
≤
|
ρ
|.Definition 6 (a trace is accepted by a path; see [3, 8]).
An execution traceσ in a model is accepted by a path ρ in an assertion graph if (suppose the length of trace and path is n)
(3)
∀
i
1
≤
i
≤
n
σ
[
i
]
∈
ant
(
ρ
[
i
]
)
⟹
∀
i
1
≤
i
≤
n
σ
[
i
]
∈
cons
(
ρ
[
i
]
)
,
where σ
[
i
] is the ith state of the trace σ and ρ
[
i
] is the ith edge of the path ρ.


### 2.3. Four Kinds of Verifying Algorithms

Based on Definition6, GSTE has four kinds of acceptance [19].Definition 7 (SMC (model checking strong satisfiability)).
A modelM strongly satisfies an assertion graph G if for all finite initial paths ρ in G and all finite traces σ in M of the same length σ is accepted by ρ, denoted by M
⊨
G.Definition 8 (NMC (model checking normal satisfiability)).
A modelM normally satisfies an assertion graph G if for every infinite initial path ρ
ω in G and every infinite trace σ
ω in M of the same length σ
ω is accepted by ρ
ω, denoted by M
⊨
G.Definition 9 (FMC (model checking fair satisfiability)).
A modelM fairly satisfies an assertion graph G under F (fairness constraint) if for every infinite fair path ρ
ω in G and every infinite trace σ
ω in M, σ
ω is accepted by ρ
ω, denoted by M
⊨
F
G.Definition 10 (TMC (model checking terminal satisfiability)).
A modelM terminally satisfies an assertion graph G under E
T (terminal edge set) if for all finite terminal paths ρ
T in G and all finite traces σ in M of the same length σ is accepted by ρ
T, denoted by M
⊨
T
G.We use the following notations in the rest of the paper,ρ
=
[
e
1
,
e
2
,
…
] be an arbitrary sequence of elements, |
ρ
| be the length of the sequence, and ρ
[
i
] be the ith element e
i in the sequence. Further, (
ρ
:
e
) denotes the sequence by appending element e to the end of ρ when ρ is finite, and (
e
:
ρ
) is the sequence by appending element e to the head of ρ.


## 2.1. Model

Definition 1 (transition relation; see [3, 8]).
A relationT
⊆
S
×
S is a transition relation if for all s
∈
S, ∃
s
′
∈
S, (
s
,
s
′
)
∈
T.Definition 2 (model; see [3, 8]).
The modelM induced by the transition relation T is the pair (
pre
,
post
), where(1)
the preimage transformer pre:2
S
→
2
S is defined as
(1)
pre
(
Q
)
=
{
s
∣
∃
s
′
∈
Q
,
(
s
,
s
′
)
∈
T
}
∀
Q
∈
2
S
,
(2)
and the postimage transformer post:2
S
→
2
S is defined as
(2)
post
(
Q
)
=
{
s
′
∣
∃
s
∈
Q
,
(
s
,
s
′
)
∈
T
}
∀
Q
∈
2
S
.Definition 3 (trace; see [3, 8]).
A traceσ in model M
=
(
pre
,
post
) is a state sequence such that σ
[
i
+
1
]
∈
post
(
σ
[
i
]
) for all 1
≤
i
≤
|
σ
|.


## 2.2. Assertion Graph

Definition 4 (assertion graph; see [3, 8]).
An assertion graph is a quintupleG
=
(
V
,
v
0
,
E
,
ant
,
cons
), where V is a finite set of vertices, v
0 is the initial vertex, E
⊆
V
×
V is a set of edges satisfying for all u
∈
V, ∃
v
∈
V, (
u
,
v
)
∈
E, ant is a mapping:   E
→
2
S, and cons is a mapping:    E
→
2
S.Definition 5 (path; see [3, 8]).
A pathρ in assertion graph G is an edge sequence such that ρ
[
i
] ends at a vertex from which ρ
[
i
+
1
] starts for all 1
≤
i
≤
|
ρ
|.Definition 6 (a trace is accepted by a path; see [3, 8]).
An execution traceσ in a model is accepted by a path ρ in an assertion graph if (suppose the length of trace and path is n)
(3)
∀
i
1
≤
i
≤
n
σ
[
i
]
∈
ant
(
ρ
[
i
]
)
⟹
∀
i
1
≤
i
≤
n
σ
[
i
]
∈
cons
(
ρ
[
i
]
)
,
where σ
[
i
] is the ith state of the trace σ and ρ
[
i
] is the ith edge of the path ρ.


## 2.3. Four Kinds of Verifying Algorithms

Based on Definition6, GSTE has four kinds of acceptance [19].Definition 7 (SMC (model checking strong satisfiability)).
A modelM strongly satisfies an assertion graph G if for all finite initial paths ρ in G and all finite traces σ in M of the same length σ is accepted by ρ, denoted by M
⊨
G.Definition 8 (NMC (model checking normal satisfiability)).
A modelM normally satisfies an assertion graph G if for every infinite initial path ρ
ω in G and every infinite trace σ
ω in M of the same length σ
ω is accepted by ρ
ω, denoted by M
⊨
G.Definition 9 (FMC (model checking fair satisfiability)).
A modelM fairly satisfies an assertion graph G under F (fairness constraint) if for every infinite fair path ρ
ω in G and every infinite trace σ
ω in M, σ
ω is accepted by ρ
ω, denoted by M
⊨
F
G.Definition 10 (TMC (model checking terminal satisfiability)).
A modelM terminally satisfies an assertion graph G under E
T (terminal edge set) if for all finite terminal paths ρ
T in G and all finite traces σ in M of the same length σ is accepted by ρ
T, denoted by M
⊨
T
G.We use the following notations in the rest of the paper,ρ
=
[
e
1
,
e
2
,
…
] be an arbitrary sequence of elements, |
ρ
| be the length of the sequence, and ρ
[
i
] be the ith element e
i in the sequence. Further, (
ρ
:
e
) denotes the sequence by appending element e to the end of ρ when ρ is finite, and (
e
:
ρ
) is the sequence by appending element e to the head of ρ.


## 3. Terminal Satisfiability

In this section, we define some concepts such as terminal assertion graph and terminal path and give some related properties on them.In GSTE, the set of states in modelM is finite (
|
S
|
is
finite
), but each state has its successor states so that traces in the model can be extended to infinite length. Each edge in the assertion graph has its successor edges so that assertion graphs can specify infinite properties. It should be noted that in our daily life, most of the properties which have been verified are finite rather than infinite. In particular, some properties are terminated at some states and these states are not involved. In GSTE existing theories, the SMC algorithm is the only one used to handle finite properties [3, 8]; it cannot stop at some edges whose labels ant
(
e
) are not related to the specifications and there are many redundant calculations. The program proves that we can predict the behavior of the model; these observations lead us to hypothesize that finite specifications will terminate at some states which we can predict. Corresponding to terminal specifications, the paths will also terminate at some edges, which are named terminal edge. Our algorithm will make the labels ant
(
e
) on the edges, which cannot reach terminal edges, equal to ∅. The method outlined here can be used to reduce the complexity of computation.For convenience, we expanded the assertion graph into six-tuple.Definition 11 (terminal assertion graph).
A terminal assertion graph is a six-tupleG
=
(
V
,
v
0
,
E
,
ant
,
cons
,
E
T
), where V, v
0, E, ant, and cons are the same as in preliminaries; E
T
⊆
E is a set of terminal edges.Definition 12 (terminal path).
A terminal path is(4)
ρ
T
=
e
0
e
1
e
2
⋯
e
|
ρ
T
|
(
e
i
∈
E
,
i
=
0,1
,
2
,
…
,
|
ρ
T
|
)
,
where e
0 is an initial edge, it starts from v
0, and e
|
ρ
T
| is a terminal edge, e
|
ρ
T
|
∈
E
T. The last edge of path ρ
T must be terminal edge.Definition 13 (a trace is accepted by a terminal path; see [3, 8, 19]).
LetG
=
(
V
,
v
0
,
E
,
ant
,
cons
,
E
T
) be a terminal assertion graph and M
=
(
pre
,
post
) be a model. Given an edge labeling γ
:
E
→
2
S where γ is either ant or cons, a trace σ in M satisfies a terminal path ρ
T of the same length under γ if for every 1
≤
i
≤
|
σ
|, σ
[
i
]
∈
γ
(
ρ
T
[
i
]
), denoted by
(5)
(
M
,
σ
)
⊨
γ
(
G
,
ρ
T
)
(
γ
=
ant
or
cons
)
.
The trace σ is accepted by the terminal path ρ
T if
(6)
(
M
,
σ
)
⊨
ant
(
G
,
ρ
T
)
⟹
(
M
,
σ
)
⊨
cons
(
G
,
ρ
T
)
,
denoted by (
M
,
σ
)
⊨
T
(
G
,
ρ
T
).Definition 14 (model satisfies terminal assertion graph).
A modelM satisfies a terminal assertion graph G if for all terminal paths ρ
T in G and all traces σ in M of the same length one has (
M
,
σ
)
⊨
T
(
G
,
ρ
T
), denoted by
(7)
M
⊨
T
G
.Definition 15 (model strongly satisfies assertion graph; see [3, 8]).
A modelM strongly satisfies an assertion graph G (E
T
=
∅) if for all finite paths ρ in G and all traces σ in M of the same length one has (
M
,
σ
)
⊨
(
G
,
ρ
), denoted by
(8)
M
⊨
G
.
The Difference between Finite Path and Terminal Path. Note that there is a key difference between finite path and terminal path; unlike terminal path, which must be end up with a terminal edge e
∈
E
T, finite path can end up with any edge e
∈
E. Given our analysis, this suggests a terminal path will be a finite path; however, a finite path may not be a terminal path.LetA
=
{
ρ
∣
ρ is a finite initial path and the length of ρ is |
ρ
|, where |
ρ
|
=
1,2
,
…
} and B
=
{
ρ
T
∣
ρ
T is a terminal path and the length of ρ
T is |
ρ
T
|, where |
ρ
T
|
=
1,2
,
…
}. The last edge of ρ
T must be a terminal edge, ρ
T
[
|
ρ
T
|
]
∈
E
T; however, the last edge of ρ does not have this restriction, it just needs to meet ρ
[
|
ρ
|
]
∈
E, E
T
⊆
E, so one has B
⊆
A.Theorem 16.
For any assertion graphG
=
(
V
,
v
0
,
E
,
a
n
t
,
c
o
n
s
,
E
T
) and any model M, one has
(9)
M
⊨
G
⟹
M
⊨
T
G
.Proof.
According to Definition15
(10)
M
⊨
G
⟺
∀
ρ
∈
A
,
(
M
,
σ
)
⊨
(
G
,
ρ
)
⟹
∀
ρ
T
∈
B
,
(
M
,
σ
)
⊨
T
(
G
,
ρ
T
)
(
using
B
⊆
A
)
⟺
M
⊨
T
G
(
using
Definition
14
)
.Theorem16 describes the relationship between SMC and TMC. If SMC returns true, then TMC returns true, but not vice versa. When E
T
=
E, terminal satisfiability behaves as strong satisfiability. When E
T
⊆
E, E
T
≠
E, we can remove some undesired paths in the assertion graph.


## 4. Model Checking with Terminal Satisfiability

In this section, we describe a model checking method for verifying terminal satisfiability. The concept of terminal satisfiability was proposed in [19] but was not given any algorithm. In this paper, we present an algorithm and prove it.


### 4.1. The TMC Algorithm

In [3, 8], the algorithms for SMC, NMC, and FMC were given. Our TMC algorithm is similar. First, we should define the backward simulation sequence.Definition 17.
Given an assertion graphG
=
(
V
,
v
0
,
E
,
ant
,
cons
,
E
T
) and a model M
=
(
pre
,
post
), the backward simulation sequence is as below
(11)
[
φ
1
,
φ
2
,
φ
3
,
…
]
,
where φ
n
:
E
→
2
S  (n
≥
1) is the n-step backward simulation relation. It is defined as
(12)
φ
1
(
e
)
=
{
⋃
e
+
∈
out
(
e
)
∩
E
T
(
pre
(
ant
(
e
+
)
)
∩
ant
(
e
)
)
∀
e
∈
E
-
E
T
,
ant
(
e
)
∀
e
∈
E
T
,
φ
n
(
e
)
=
{
φ
n
(
e
)
∪
(
⋃
e
+
∈
out
(
e
)
(
pre
(
φ
n
(
e
+
)
)
∩
ant
(
e
)
)
)
∀
e
∈
E
-
E
T
,
ant
(
e
)
∀
e
∈
E
T
.Based on this result, when we verify finite properties, we simply verify those traces that can reach some states inant
(
e
), where e
∈
E
T. These states, which are related to the property, are assigned to the label ant of the terminal edge. Then we emulate the model’s behavior backwards starting from the terminal edge. The n-step backward simulation relation φ
n is the set of the states that can reach the terminal edge within n-step.Obviously, the backward simulation relation sequence is nondecreasing and has a least fix-point upper limit bounded byant. We denote the least fix-point by φ
T
*. Now we propose a terminal satisfiability model checking algorithm that first performs a series of graph transformations and then checks strong satisfiability on the resulting graph.


### 4.2. The Application of TMC

In order to describe TMC clearly, let us look at the following example [23].Example 18.
Consider the modelM in Figure 1, where S
=
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
,
s
5
,
s
6
}.Figure 1
A simple model.Suppose we want to specify the following property: if the system is in the states
5, then it must have been in s
3 the last time when it was neither in s
5 nor s
6. The model satisfies this property. Now, let us catch this property using the assertion graph in Figure 2.Figure 2
An assertion graph.The fact that SMC cannot verify this property is due to undesired paths, such as the finite initial pathρ
1
=
[
(
v
0
,
v
1
)
] and the finite trace σ
1
=
[
s
4
], σ
1
⊨
ant
ρ
1, but the first state s
4 of σ
1 is not in the cons
(
(
v
0
,
v
1
)
)
=
{
s
3
}. Thus, the model does not strongly satisfy the assertion graph. If we use SMC, the SMC algorithm will return false. In order to deal with this situation in the former, [3, 8] introduce NMC and FMC. As we know, NMC and FMC have been used to deal with ω-regular properties. If we want to solve the SMC’s limitation, we should expand finite specifications to infinite specifications. This is the key that leads to the increasing complexity of the model checking. However, the algorithm of using TMC to verify this property is more suitable. TMC can be accomplished without expanding finite specifications to infinite specifications. The following example is constructed only for the purpose of illustrating the computational procedure discussed.Step 1.
Construct the terminal assertion graph and figure out the terminal edges (Figure3).Figure 3
A terminal assertion graph.Step 2.
First, the fix-pointφ
T
* of every edge is computed according to Definition 17; then the label ant of every edge is replaced by the corresponding φ
T
*; lastly, the resulting assertion graph G
′ is gotten.Step 3.
This step behaves as the algorithmSMC
:
SMC
(
M
,
G
′
). The edge which is marked by the blue line is the terminal edge. Supposing E
T
=
{
(
v
1
,
v
2
)
}, there is only one terminal edge in the case (Figure 3). Thus, the terminal path can be grouped into two cases (as follows):
(13)
ρ
T
1
=
[
(
v
0
,
v
1
)
(
v
1
,
v
2
)
]
(
|
ρ
T
1
|
=
2
)
,
ρ
T
2
=
[
(
v
0
,
v
1
)
(
v
1
,
v
1
)
⋯
(
v
1
,
v
1
)
(
v
1
,
v
2
)
]
(
|
ρ
T
2
|
≥
3
)
.
Because the terminal path must end up with the terminal edge, there is only one terminal edge in Figure 3 and the vertex v
2 to v
1 is unreachable. Thus, if a path reaches the edge (
v
2
,
v
2
) that is not a terminal path, then all terminal paths are finite. As we know, the length of a terminal path must be greater than or equal to 2. Thus, we can eliminate the path ρ
1 and the trace σ
1, which will lead to SMC returning false negative, since |
ρ
1
|
=
|
σ
1
|
=
1. The trace in model M (Figure 1), if not starting from s
3, ultimately would violate the label ant
(
(
v
1
,
v
2
)
) on the edge (
v
1
,
v
2
); therefore the model M (Figure 1) terminally satisfies the terminal assertion graph G (Figure 3). The calculation is as follows (after one iteration, every edge can be reached to the fix-point).The first iteration (initialization):(14)
φ
1
(
v
1
,
v
2
)
=
ant
(
(
v
1
,
v
2
)
)
=
{
s
5
}
,
φ
1
(
v
1
,
v
1
)
=
pre
(
ant
(
(
v
1
,
v
2
)
)
)
∩
ant
(
(
v
1
,
v
1
)
)
=
pre
(
{
s
5
}
)
∩
{
s
5
,
s
6
}
=
{
s
3
,
s
5
}
∩
{
s
5
,
s
6
}
=
{
s
5
}
,
φ
1
(
v
0
,
v
1
)
=
pre
(
ant
(
(
v
1
,
v
2
)
)
)
∩
ant
(
(
v
0
,
v
1
)
)
=
{
s
3
,
s
5
}
∩
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
}
=
{
s
3
}
,
φ
1
(
v
2
,
v
2
)
=
∅
.The second iteration:(15)
φ
2
(
v
1
,
v
2
)
=
{
s
5
}
,
φ
2
(
v
1
,
v
1
)
=
φ
1
(
v
1
,
v
1
)
∪
(
pre
(
φ
1
(
v
1
,
v
1
)
)
∩
ant
(
(
v
1
,
v
1
)
)
)
∪
(
pre
(
φ
1
(
v
1
,
v
2
)
)
∩
ant
(
(
v
1
,
v
1
)
)
)
=
{
s
5
}
∪
(
pre
{
s
5
}
∩
{
s
5
,
s
6
}
)
=
{
s
5
}
,
φ
2
(
v
0
,
v
1
)
=
φ
1
(
v
0
,
v
1
)
∪
(
pre
(
φ
1
(
v
1
,
v
1
)
)
∩
ant
(
(
v
0
,
v
1
)
)
)
∪
(
pre
(
φ
1
(
v
1
,
v
2
)
)
∩
ant
(
(
v
0
,
v
1
)
)
)
=
{
s
3
}
∪
(
pre
{
s
5
}
∩
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
}
)
∪
(
pre
{
s
5
}
∩
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
}
)
=
{
s
3
}
,
φ
2
(
v
2
,
v
2
)
=
∅
.
After replacing the label ant of each edge with the corresponding fix-point φ
T
*, the resulting assertion graph G
′ is shown as Figure 4.Figure 4
The resulting assertion graphG
′.As can be seen,ant of each edge has been reached by the minimum, and TMC returns true. Thus, the model satisfies the terminal assertion graph.


### 4.3. A Hardware Verification Case of TMC

In this section, we present a case study of TMC on hardware verification. The circuit we choose for this study is a round-robin arbiter, which is the core component in many real network systems [24]. An arbiter has N inputs and the output is a vector encoding of arbitration results. Request with highest priority in round-robin order is granted in each cycle, and the priority of the request which is granted in last arbitration will become the lowest in the next round; this protocol guarantees a dynamic priority assignment to requestors without starvation. We consider the arbiter with 4 inputs (shown in Figure 5). First, the priority of inputs is placed in descending order from req
[
0
] to req
[
3
] [25, 26]. Thus, req
[
0
] has the highest priority, req
[
1
] has the next priority, and so on. Each input of the arbiter in Figure 5 is connected to a switch cell; only one of the four inputs will succeed each clock cycle. Others are rejected and must retry later. routeEnable is enable signal.Figure 5
An arbiter with 4 inputs.We model this arbiter as a finite state machine (shown in Figure6) according to its truth table in paper [24]. The input req
[
3
:
0
] is a vector of ternary-valued variables; each variable can take 0, 1, or X. X indicates that variable can take 0 or 1. Figure 6 is the model of this arbiter. Consider
(16)
trans
⁡
_
0
_
0
=
req
1
=
0
&
req
2
=
0
&
req
3
=
0
&
routeEnable
=
1
,
trans
⁡
_
0
_
1
=
req
1
=
1
&
ruoteEnable
=
1
,
trans
⁡
_
0
_
2
=
req
1
=
0
&
req
2
=
1
&
routeEnable
=
1
,
trans
⁡
_
0
_
3
=
req
1
=
0
&
req
2
=
0
&
req
3
=
1
&
routeEnable
=
1
,
trans
⁡
_
1
_
1
=
req
2
=
0
&
req
3
=
0
&
req
0
=
0
&
routeEnable
=
1
,
trans
⁡
_
1
_
2
=
req
2
=
1
&
routeEnable
=
1
,
trans
⁡
_
1
_
3
=
req
2
=
0
&
req
3
=
1
&
routeEnable
=
1
,
trans
⁡
_
1
_
0
=
req
2
=
0
&
req
3
=
0
&
req
0
=
1
&
routeEnable
=
1
,
trans
⁡
_
2
_
2
=
req
3
=
0
&
req
0
=
0
&
req
1
=
0
&
routeEnable
=
1
,
trans
⁡
_
2
_
3
=
req
3
=
1
&
routeEnable
=
1
,
trans
⁡
_
2
_
0
=
req
3
=
0
&
req
0
=
1
&
routeEnable
=
1
,
trans
⁡
_
2
_
1
=
req
3
=
0
&
req
0
=
0
&
req
1
=
1
&
routeEnable
=
1
,
trans
⁡
_
3
_
3
=
req
0
=
0
&
req
1
=
0
&
req
2
=
0
&
routeEnable
=
1
,
trans
⁡
_
3
_
0
=
req
0
=
1
&
routeEnable
=
1
,
trans
⁡
_
3
_
1
=
req
0
=
0
&
req
1
=
1
&
routeEnable
=
1
,
trans
⁡
_
3
_
2
=
req
0
=
0
&
req
1
=
0
&
req
2
=
1
&
routeEnable
=
1
.
Safety property: once a request reqi is set high from a state and kept high, then the request will be granted after several cycles. Suppose a state where the value of grant is [
1,0
], which means that the last request granted is req2; if the request req2 is set high again and kept high, then the request will be granted after at most 4 cycles. We use the terminal assertion graph to specify this property (shown as in Figure 7) [24]. Consider
(17)
ant
_
V
I
_
V
set
=
req
0
=
0
&
req
1
=
0
&
req
2
=
1
&
req
3
=
0
,
ant
_
V
set
_
V
1
=
req
2
=
1
&
req
3
=
0
&
req
0
=
0
&
req
1
=
1
,
ant
_
V
set
_
V
3
=
req
2
=
1
&
req
3
=
1
,
ant
_
V
set
_
V
0
=
req
2
=
1
&
req
3
=
0
&
req
0
=
1
,
ant
_
V
1
_
V
2
=
req
2
=
1
,
ant
_
V
0
_
V
1
=
req
2
=
1
&
req
1
=
1
,
ant
_
V
0
_
V
2
=
req
2
=
1
&
req
1
=
0
,
ant
_
V
3
_
V
0
=
req
2
=
1
&
req
0
=
1
,
ant
_
V
3
_
V
1
=
req
2
=
1
&
req
0
=
0
&
req
1
=
1
,
ant
_
V
3
_
V
2
=
req
2
=
1
&
req
0
=
0
&
req
1
=
0
,
ant
_
V
2
_
V
end
=
grant
1
=
0
&
grant
0
=
1
,
cons
=
grant
1
=
0
&
grant
0
=
1
.
The edge (
V
2
,
V
end
) is the terminal edge. We only verify those paths that end up with the edge (
V
2
,
V
end
). If we use SMC to verify this property, we must verify all finite paths. If using TMC, we only need to verify terminal paths. In the terminal assertion graph (Figure 7), all finite paths are as follows:
(18)
ρ
1
=
[
V
I
,
V
set
]
,
ρ
2
=
[
V
I
,
V
set
]
[
V
set
,
V
1
]
,
ρ
3
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
,
ρ
4
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
,
ρ
5
=
[
V
I
,
V
set
]
[
V
set
,
V
1
]
[
V
1
,
V
2
]
,
ρ
6
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
1
]
,
ρ
7
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
1
]
,
ρ
8
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
,
ρ
9
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
2
]
,
ρ
10
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
1
]
[
V
1
,
V
2
]
,
ρ
11
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
1
]
,
ρ
12
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
,
ρ
13
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
2
]
,
ρ
14
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
,
ρ
15
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
2
]
,
ρ
16
=
[
V
I
,
V
set
]
[
V
set
,
V
1
]
[
V
1
,
V
2
]
[
V
2
,
V
end
]
,
ρ
17
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
[
V
2
,
V
end
]
,
ρ
18
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
2
]
[
V
2
,
V
end
]
,
ρ
19
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
1
]
[
V
1
,
V
2
]
[
V
2
,
V
end
]
,
ρ
20
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
2
]
[
V
2
,
V
end
]
,
ρ
21
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
2
]
[
V
2
,
V
end
]
,
ρ
22
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
×
[
V
2
,
V
end
]
.
If we use SMC, we must verify 22 paths: ρ
1
,
…
,
ρ
22. But we use TMC only to verify ρ
16
,
…
,
ρ
22. Therefore, the time cost by SMC is 3.14× with TMC in this case.Figure 6
The behavior of arbiter.Figure 7
The terminal assertion graph.


## 4.1. The TMC Algorithm

In [3, 8], the algorithms for SMC, NMC, and FMC were given. Our TMC algorithm is similar. First, we should define the backward simulation sequence.Definition 17.
Given an assertion graphG
=
(
V
,
v
0
,
E
,
ant
,
cons
,
E
T
) and a model M
=
(
pre
,
post
), the backward simulation sequence is as below
(11)
[
φ
1
,
φ
2
,
φ
3
,
…
]
,
where φ
n
:
E
→
2
S  (n
≥
1) is the n-step backward simulation relation. It is defined as
(12)
φ
1
(
e
)
=
{
⋃
e
+
∈
out
(
e
)
∩
E
T
(
pre
(
ant
(
e
+
)
)
∩
ant
(
e
)
)
∀
e
∈
E
-
E
T
,
ant
(
e
)
∀
e
∈
E
T
,
φ
n
(
e
)
=
{
φ
n
(
e
)
∪
(
⋃
e
+
∈
out
(
e
)
(
pre
(
φ
n
(
e
+
)
)
∩
ant
(
e
)
)
)
∀
e
∈
E
-
E
T
,
ant
(
e
)
∀
e
∈
E
T
.Based on this result, when we verify finite properties, we simply verify those traces that can reach some states inant
(
e
), where e
∈
E
T. These states, which are related to the property, are assigned to the label ant of the terminal edge. Then we emulate the model’s behavior backwards starting from the terminal edge. The n-step backward simulation relation φ
n is the set of the states that can reach the terminal edge within n-step.Obviously, the backward simulation relation sequence is nondecreasing and has a least fix-point upper limit bounded byant. We denote the least fix-point by φ
T
*. Now we propose a terminal satisfiability model checking algorithm that first performs a series of graph transformations and then checks strong satisfiability on the resulting graph.


## 4.2. The Application of TMC

In order to describe TMC clearly, let us look at the following example [23].Example 18.
Consider the modelM in Figure 1, where S
=
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
,
s
5
,
s
6
}.Figure 1
A simple model.Suppose we want to specify the following property: if the system is in the states
5, then it must have been in s
3 the last time when it was neither in s
5 nor s
6. The model satisfies this property. Now, let us catch this property using the assertion graph in Figure 2.Figure 2
An assertion graph.The fact that SMC cannot verify this property is due to undesired paths, such as the finite initial pathρ
1
=
[
(
v
0
,
v
1
)
] and the finite trace σ
1
=
[
s
4
], σ
1
⊨
ant
ρ
1, but the first state s
4 of σ
1 is not in the cons
(
(
v
0
,
v
1
)
)
=
{
s
3
}. Thus, the model does not strongly satisfy the assertion graph. If we use SMC, the SMC algorithm will return false. In order to deal with this situation in the former, [3, 8] introduce NMC and FMC. As we know, NMC and FMC have been used to deal with ω-regular properties. If we want to solve the SMC’s limitation, we should expand finite specifications to infinite specifications. This is the key that leads to the increasing complexity of the model checking. However, the algorithm of using TMC to verify this property is more suitable. TMC can be accomplished without expanding finite specifications to infinite specifications. The following example is constructed only for the purpose of illustrating the computational procedure discussed.Step 1.
Construct the terminal assertion graph and figure out the terminal edges (Figure3).Figure 3
A terminal assertion graph.Step 2.
First, the fix-pointφ
T
* of every edge is computed according to Definition 17; then the label ant of every edge is replaced by the corresponding φ
T
*; lastly, the resulting assertion graph G
′ is gotten.Step 3.
This step behaves as the algorithmSMC
:
SMC
(
M
,
G
′
). The edge which is marked by the blue line is the terminal edge. Supposing E
T
=
{
(
v
1
,
v
2
)
}, there is only one terminal edge in the case (Figure 3). Thus, the terminal path can be grouped into two cases (as follows):
(13)
ρ
T
1
=
[
(
v
0
,
v
1
)
(
v
1
,
v
2
)
]
(
|
ρ
T
1
|
=
2
)
,
ρ
T
2
=
[
(
v
0
,
v
1
)
(
v
1
,
v
1
)
⋯
(
v
1
,
v
1
)
(
v
1
,
v
2
)
]
(
|
ρ
T
2
|
≥
3
)
.
Because the terminal path must end up with the terminal edge, there is only one terminal edge in Figure 3 and the vertex v
2 to v
1 is unreachable. Thus, if a path reaches the edge (
v
2
,
v
2
) that is not a terminal path, then all terminal paths are finite. As we know, the length of a terminal path must be greater than or equal to 2. Thus, we can eliminate the path ρ
1 and the trace σ
1, which will lead to SMC returning false negative, since |
ρ
1
|
=
|
σ
1
|
=
1. The trace in model M (Figure 1), if not starting from s
3, ultimately would violate the label ant
(
(
v
1
,
v
2
)
) on the edge (
v
1
,
v
2
); therefore the model M (Figure 1) terminally satisfies the terminal assertion graph G (Figure 3). The calculation is as follows (after one iteration, every edge can be reached to the fix-point).The first iteration (initialization):(14)
φ
1
(
v
1
,
v
2
)
=
ant
(
(
v
1
,
v
2
)
)
=
{
s
5
}
,
φ
1
(
v
1
,
v
1
)
=
pre
(
ant
(
(
v
1
,
v
2
)
)
)
∩
ant
(
(
v
1
,
v
1
)
)
=
pre
(
{
s
5
}
)
∩
{
s
5
,
s
6
}
=
{
s
3
,
s
5
}
∩
{
s
5
,
s
6
}
=
{
s
5
}
,
φ
1
(
v
0
,
v
1
)
=
pre
(
ant
(
(
v
1
,
v
2
)
)
)
∩
ant
(
(
v
0
,
v
1
)
)
=
{
s
3
,
s
5
}
∩
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
}
=
{
s
3
}
,
φ
1
(
v
2
,
v
2
)
=
∅
.The second iteration:(15)
φ
2
(
v
1
,
v
2
)
=
{
s
5
}
,
φ
2
(
v
1
,
v
1
)
=
φ
1
(
v
1
,
v
1
)
∪
(
pre
(
φ
1
(
v
1
,
v
1
)
)
∩
ant
(
(
v
1
,
v
1
)
)
)
∪
(
pre
(
φ
1
(
v
1
,
v
2
)
)
∩
ant
(
(
v
1
,
v
1
)
)
)
=
{
s
5
}
∪
(
pre
{
s
5
}
∩
{
s
5
,
s
6
}
)
=
{
s
5
}
,
φ
2
(
v
0
,
v
1
)
=
φ
1
(
v
0
,
v
1
)
∪
(
pre
(
φ
1
(
v
1
,
v
1
)
)
∩
ant
(
(
v
0
,
v
1
)
)
)
∪
(
pre
(
φ
1
(
v
1
,
v
2
)
)
∩
ant
(
(
v
0
,
v
1
)
)
)
=
{
s
3
}
∪
(
pre
{
s
5
}
∩
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
}
)
∪
(
pre
{
s
5
}
∩
{
s
0
,
s
1
,
s
2
,
s
3
,
s
4
}
)
=
{
s
3
}
,
φ
2
(
v
2
,
v
2
)
=
∅
.
After replacing the label ant of each edge with the corresponding fix-point φ
T
*, the resulting assertion graph G
′ is shown as Figure 4.Figure 4
The resulting assertion graphG
′.As can be seen,ant of each edge has been reached by the minimum, and TMC returns true. Thus, the model satisfies the terminal assertion graph.


## 4.3. A Hardware Verification Case of TMC

In this section, we present a case study of TMC on hardware verification. The circuit we choose for this study is a round-robin arbiter, which is the core component in many real network systems [24]. An arbiter has N inputs and the output is a vector encoding of arbitration results. Request with highest priority in round-robin order is granted in each cycle, and the priority of the request which is granted in last arbitration will become the lowest in the next round; this protocol guarantees a dynamic priority assignment to requestors without starvation. We consider the arbiter with 4 inputs (shown in Figure 5). First, the priority of inputs is placed in descending order from req
[
0
] to req
[
3
] [25, 26]. Thus, req
[
0
] has the highest priority, req
[
1
] has the next priority, and so on. Each input of the arbiter in Figure 5 is connected to a switch cell; only one of the four inputs will succeed each clock cycle. Others are rejected and must retry later. routeEnable is enable signal.Figure 5
An arbiter with 4 inputs.We model this arbiter as a finite state machine (shown in Figure6) according to its truth table in paper [24]. The input req
[
3
:
0
] is a vector of ternary-valued variables; each variable can take 0, 1, or X. X indicates that variable can take 0 or 1. Figure 6 is the model of this arbiter. Consider
(16)
trans
⁡
_
0
_
0
=
req
1
=
0
&
req
2
=
0
&
req
3
=
0
&
routeEnable
=
1
,
trans
⁡
_
0
_
1
=
req
1
=
1
&
ruoteEnable
=
1
,
trans
⁡
_
0
_
2
=
req
1
=
0
&
req
2
=
1
&
routeEnable
=
1
,
trans
⁡
_
0
_
3
=
req
1
=
0
&
req
2
=
0
&
req
3
=
1
&
routeEnable
=
1
,
trans
⁡
_
1
_
1
=
req
2
=
0
&
req
3
=
0
&
req
0
=
0
&
routeEnable
=
1
,
trans
⁡
_
1
_
2
=
req
2
=
1
&
routeEnable
=
1
,
trans
⁡
_
1
_
3
=
req
2
=
0
&
req
3
=
1
&
routeEnable
=
1
,
trans
⁡
_
1
_
0
=
req
2
=
0
&
req
3
=
0
&
req
0
=
1
&
routeEnable
=
1
,
trans
⁡
_
2
_
2
=
req
3
=
0
&
req
0
=
0
&
req
1
=
0
&
routeEnable
=
1
,
trans
⁡
_
2
_
3
=
req
3
=
1
&
routeEnable
=
1
,
trans
⁡
_
2
_
0
=
req
3
=
0
&
req
0
=
1
&
routeEnable
=
1
,
trans
⁡
_
2
_
1
=
req
3
=
0
&
req
0
=
0
&
req
1
=
1
&
routeEnable
=
1
,
trans
⁡
_
3
_
3
=
req
0
=
0
&
req
1
=
0
&
req
2
=
0
&
routeEnable
=
1
,
trans
⁡
_
3
_
0
=
req
0
=
1
&
routeEnable
=
1
,
trans
⁡
_
3
_
1
=
req
0
=
0
&
req
1
=
1
&
routeEnable
=
1
,
trans
⁡
_
3
_
2
=
req
0
=
0
&
req
1
=
0
&
req
2
=
1
&
routeEnable
=
1
.
Safety property: once a request reqi is set high from a state and kept high, then the request will be granted after several cycles. Suppose a state where the value of grant is [
1,0
], which means that the last request granted is req2; if the request req2 is set high again and kept high, then the request will be granted after at most 4 cycles. We use the terminal assertion graph to specify this property (shown as in Figure 7) [24]. Consider
(17)
ant
_
V
I
_
V
set
=
req
0
=
0
&
req
1
=
0
&
req
2
=
1
&
req
3
=
0
,
ant
_
V
set
_
V
1
=
req
2
=
1
&
req
3
=
0
&
req
0
=
0
&
req
1
=
1
,
ant
_
V
set
_
V
3
=
req
2
=
1
&
req
3
=
1
,
ant
_
V
set
_
V
0
=
req
2
=
1
&
req
3
=
0
&
req
0
=
1
,
ant
_
V
1
_
V
2
=
req
2
=
1
,
ant
_
V
0
_
V
1
=
req
2
=
1
&
req
1
=
1
,
ant
_
V
0
_
V
2
=
req
2
=
1
&
req
1
=
0
,
ant
_
V
3
_
V
0
=
req
2
=
1
&
req
0
=
1
,
ant
_
V
3
_
V
1
=
req
2
=
1
&
req
0
=
0
&
req
1
=
1
,
ant
_
V
3
_
V
2
=
req
2
=
1
&
req
0
=
0
&
req
1
=
0
,
ant
_
V
2
_
V
end
=
grant
1
=
0
&
grant
0
=
1
,
cons
=
grant
1
=
0
&
grant
0
=
1
.
The edge (
V
2
,
V
end
) is the terminal edge. We only verify those paths that end up with the edge (
V
2
,
V
end
). If we use SMC to verify this property, we must verify all finite paths. If using TMC, we only need to verify terminal paths. In the terminal assertion graph (Figure 7), all finite paths are as follows:
(18)
ρ
1
=
[
V
I
,
V
set
]
,
ρ
2
=
[
V
I
,
V
set
]
[
V
set
,
V
1
]
,
ρ
3
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
,
ρ
4
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
,
ρ
5
=
[
V
I
,
V
set
]
[
V
set
,
V
1
]
[
V
1
,
V
2
]
,
ρ
6
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
1
]
,
ρ
7
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
1
]
,
ρ
8
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
,
ρ
9
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
2
]
,
ρ
10
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
1
]
[
V
1
,
V
2
]
,
ρ
11
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
1
]
,
ρ
12
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
,
ρ
13
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
2
]
,
ρ
14
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
,
ρ
15
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
2
]
,
ρ
16
=
[
V
I
,
V
set
]
[
V
set
,
V
1
]
[
V
1
,
V
2
]
[
V
2
,
V
end
]
,
ρ
17
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
[
V
2
,
V
end
]
,
ρ
18
=
[
V
I
,
V
set
]
[
V
set
,
V
0
]
[
V
0
,
V
2
]
[
V
2
,
V
end
]
,
ρ
19
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
1
]
[
V
1
,
V
2
]
[
V
2
,
V
end
]
,
ρ
20
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
2
]
[
V
2
,
V
end
]
,
ρ
21
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
2
]
[
V
2
,
V
end
]
,
ρ
22
=
[
V
I
,
V
set
]
[
V
set
,
V
3
]
[
V
3
,
V
0
]
[
V
0
,
V
1
]
[
V
1
,
V
2
]
×
[
V
2
,
V
end
]
.
If we use SMC, we must verify 22 paths: ρ
1
,
…
,
ρ
22. But we use TMC only to verify ρ
16
,
…
,
ρ
22. Therefore, the time cost by SMC is 3.14× with TMC in this case.Figure 6
The behavior of arbiter.Figure 7
The terminal assertion graph.


## 5. Correctness Proof

In this section, we formally prove that the TMC algorithm is both sound and complete.


### 5.1. The Logic of Algorithm

M
⊨
T
G
⇔ for all ρ
T in G, for all σ in M of the same length, and (
M
,
σ
)
⊨
T
(
G
,
ρ
T
)
⇔ for all ρ
T in G and for all σ in M of the same length,
(19)
(
M
,
σ
)
⊨
ant
(
G
,
ρ
T
)
⟹
(
M
,
σ
)
⊨
cons
(
G
,
ρ
T
)
.
By analyzing algorithm TMC, in the end, we use SMC
(
M
,
G
′
). Consider
(20)
SMC
(
M
,
G
′
)
returns
true
⟹
M
⊨
G
′
.
It indicates that we can only get
(21)
∀
ρ
in
G
,
∀
σ
in
M
of
the
same
length
,
(
M
,
σ
)
⊨
φ
T
*
(
G
,
ρ
)
⟹
(
M
,
σ
)
⊨
cons
(
G
,
ρ
)
.
But we are aiming at (according to (19))
(22)
∀
ρ
T
in
G
,
∀
σ
in
M
of
the
same
length
,
(
M
,
σ
)
⊨
ant
(
G
,
ρ
T
)
⟹
(
M
,
σ
)
⊨
cons
(
G
,
ρ
T
)
.
Then, if we want to prove TMC is correct, we must prove that (according to (21) and (22))
(23)
∀
ρ
T
in
G
,
∀
σ
in
M
of
the
same
length
,
(
M
,
σ
)
⊨
ant
(
G
,
ρ
T
)
⟹
(
M
,
σ
)
⊨
φ
T
*
(
G
,
ρ
T
)
.


### 5.2. The TMC Algorithm Is Sound

According to Definition17, we get the following lemma.Lemma 19.
For a terminal assertion graphG
=
(
V
,
v
0
,
E
,
a
n
t
,
c
o
n
s
,
E
T
) and a model M
=
(
p
r
e
,
p
o
s
t
), let [
φ
1
,
φ
2
,
φ
3
,
…
] be the backward simulation sequence towards E
T
⊆
E. Then for any n
≥
2, for all finite terminal paths ρ
T, and all finite traces σ of length n
+
1, such that (1)
ρ
T
[
n
+
1
]
∈
E
T
(2)
when
σ
2
⊨
a
n
t
ρ
T
2
and
|
σ
2
|
=
|
ρ
T
2
|
=
n
, we have
σ
[
i
]
∈
φ
n
+
1
-
i
(
ρ
T
[
i
]
)
(
i
=
2,3
,
…
,
n
) (note:
ρ
T
2
represents all paths of length
n
which are obtained by traversing backwards starting from the terminal edge. For example, if
ρ
T
=
e
1
e
2
⋯
e
n
e
n
+
1
and
e
n
+
1
∈
E
T
, then
ρ
T
2
=
e
2
e
3
⋯
e
n
e
n
+
1
,
σ
2
represents all traces of length
n
obtained by traversing backwards starting from the last state of
σ
)
(3)
when
σ
⊨
a
n
t
ρ
T
, we have
σ
[
1
]
∈
φ
n
(
ρ
T
[
1
]
)
,
σ
[
n
+
1
]
∈
φ
1
(
ρ
T
[
n
+
1
]
)
.Proof (mathematical induction).
Suppose|
ρ
T
|
=
|
σ
|
=
k
+
1.
First Step
(
k
=
2
). (1) ρ
T
[
3
]
∈
E
T since ρ
T is a terminal path.
(2) Let us proveσ
[
2
]
∈
φ
1
(
ρ
T
[
2
]
):
(24)
σ
2
⊨
ant
ρ
T
2
⟹
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
,
σ
[
3
]
∈
ant
(
ρ
T
[
3
]
)
,
(25)
σ
[
2
]
∈
pre
(
σ
[
3
]
)
⟹
(
24
)
σ
[
2
]
∈
pre
(
ant
(
ρ
T
[
3
]
)
)
.
According to (24)-(25),
(26)
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
∩
pre
(
ant
(
ρ
T
[
3
]
)
)
⊆
φ
1
(
ρ
T
[
2
]
)
.
(3) Let us proveσ
[
1
]
∈
φ
2
(
ρ
T
[
1
]
), σ
[
3
]
∈
φ
1
(
ρ
T
[
3
]
):
(27)
σ
[
1
]
∈
pre
(
σ
[
2
]
)
⟹
(
26
)
σ
[
1
]
∈
pre
(
φ
1
(
ρ
T
[
2
]
)
)
(28)
σ
⊨
ant
ρ
T
⟹
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
.
According to (27)-(28),
(29)
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
∩
pre
(
φ
1
(
ρ
T
[
2
]
)
)
⊆
φ
1
(
ρ
T
[
1
]
)
∪
(
⋃
e
+
∈
out
(
ρ
T
[
1
]
)
(
pre
(
φ
1
(
e
+
)
)
∩
ant
(
ρ
T
[
1
]
)
)
)
=
φ
2
(
ρ
T
[
1
]
)
,
σ
⊨
ant
ρ
T
⟹
σ
[
3
]
∈
ant
(
ρ
T
[
3
]
)
=
φ
1
(
ρ
T
[
3
]
)
.
Then, the conclusions (1), (2), and (3) are true for k
=
2.
Second Step. We already saw that the conclusions are true for k
=
2. Assume this, for an arbitrary n, the above lemma is true for k
=
n, then we get the following.
(σ represents all traces of length n
+
1 and ρ
T represents all terminal paths of the same length) (1) ρ
T
[
n
+
1
]
∈
E
T. (2) When σ
2
⊨
ant
ρ
T
2, we have σ
[
i
]
∈
φ
n
+
1
-
i
(
ρ
T
[
i
]
) (i
=
2,3
,
…
,
n) (where ρ
T
2 represents all paths of length k obtained by traversing backwards starting from the terminal edge; the terminal edge is the last edge of the terminal path; σ
2 is similar), (3) when σ
⊨
ant
ρ
T, we have σ
[
1
]
∈
φ
n
(
ρ
T
[
1
]
), σ
[
n
+
1
]
∈
φ
1
(
ρ
T
[
n
+
1
]
).
Third Step (let us derive the lemma is true for
k
=
n
+
1
from above assumption). We must consider all terminal paths ρ
T of length n
+
2 and all traces of the same length.
(1)ρ
T
[
n
+
2
]
∈
E
T since ρ
T is a terminal path.
(2) We must proveσ
2
⊨
ant
ρ
T
2
⇒
σ
[
i
]
∈
φ
n
+
2
-
i
(
ρ
T
[
i
]
) (i
=
2,3
,
…
,
n
,
n
+
1) at this step, |
ρ
T
2
|
=
|
σ
2
|
=
n
+
1
(30)
σ
2
⊨
ant
ρ
T
2
⟹
σ
3
⊨
ant
ρ
T
3
,
where ρ
T
3 represents all paths of length n obtained by traversing starting from the terminal edge and σ
3 is obtained by deleting the first two states of σ, |
σ
|
=
n
+
2
⇒
|
σ
3
|
=
n, and |
ρ
T
|
=
n
+
2
⇒
|
ρ
T
3
|
=
n. By the induction hypothesis we have the following conclusion:
(31)
σ
3
⊨
ant
ρ
T
3
⟹
σ
[
i
]
∈
φ
n
+
1
-
i
(
ρ
T
[
i
]
)
⊆
φ
n
+
2
-
i
(
ρ
T
[
i
]
)
,
(
i
=
3,4
,
…
,
n
,
n
+
1
)
.
According to (31),
(32)
σ
[
3
]
∈
φ
n
-
1
(
ρ
T
[
3
]
)
,
(33)
σ
[
2
]
∈
pre
(
σ
[
3
]
)
⟹
(
32
)
σ
[
2
]
∈
pre
(
φ
n
-
1
(
ρ
T
[
3
]
)
)
,
(34)
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
⟹
(
33
)
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
∩
pre
(
φ
n
-
1
(
ρ
T
[
3
]
)
)
⊆
φ
n
-
1
(
ρ
T
[
2
]
)
∪
(
⋃
e
+
∈
out
(
ρ
T
[
2
]
)
(
pre
(
φ
n
-
1
(
e
+
)
)
∩
ant
(
ρ
T
[
2
]
)
)
)
=
φ
n
(
ρ
T
[
2
]
)
,
namely, σ
2
⊨
ant
ρ
T
2
⇒
σ
[
i
]
∈
φ
n
+
2
-
i
(
ρ
T
[
i
]
) (i
=
2,3
,
…
,
n
,
n
+
1).
(3) Consider(35)
σ
⊨
ant
ρ
T
⟹
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
,
(36)
σ
⊨
ant
ρ
T
⟹
σ
2
⊨
ant
ρ
T
2
⟹
(
34
)
σ
[
2
]
∈
φ
n
(
ρ
T
[
2
]
)
,
(37)
σ
[
1
]
∈
pre
(
σ
[
2
]
)
⟹
(
36
)
σ
[
1
]
∈
pre
(
φ
n
(
ρ
T
[
2
]
)
)
.
According to (35)–(37),
(38)
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
∩
pre
(
φ
n
(
ρ
T
[
2
]
)
)
⊆
φ
n
(
ρ
T
[
1
]
)
∪
(
⋃
e
+
∈
out
(
ρ
T
[
1
]
)
(
pre
(
φ
n
(
e
+
)
)
∩
ant
(
ρ
T
[
1
]
)
)
)
=
φ
n
+
1
(
ρ
T
[
1
]
)
,
σ
⊨
ant
ρ
T
⟹
σ
[
n
+
2
]
∈
ant
(
ρ
T
[
n
+
2
]
)
=
φ
1
(
ρ
T
[
n
+
2
]
)
which exactly means that the lemma holds for k
=
n
+
1. Therefore, the lemma is true for all n starting with 2.The conclusions of Lemma19 have been used to prove Theorem 20. At the same time, Lemma 19 gives the conclusion that the backward simulation sequence φ
n is a convergent sequence. If the length of the path is n, then the simulation sequence of the ith edges will reach the fixed point through at least n
+
1
-
i iterations.Supposeφ
T
* is the fix-point of the backward simulation sequence based on the terminal set E
T; after replacing the label ant of each edge with the corresponding fix-point φ
T
*, the resulting assertion graph is denoted by G
′.Theorem 20.
Consider(
*
)
M
⊨
T
G
⟺
M
⊨
T
G
′
.Proof.
According to Section5.1 (the logic of algorithm), we know (
*
) holds equivalent to the following (
*
*
). For any n
≥
2, ρ
T represents all terminal paths of length n in assertion graph G (ρ
T is also the terminal path in assertion graph G
′) and σ represents all traces of the same length in model M. Consider
(
*
*
)
σ
⊨
ant
ρ
T
⟺
σ
⊨
φ
T
*
ρ
T
.
The direction ⇐ is obvious, since φ
T
*
(
e
)
⊆
ant
(
e
) for any e
∈
E.
The direction⇒: when σ
⊨
ant
ρ
T, according to Lemma 19,
(39)
σ
[
i
]
∈
φ
T
*
(
ρ
T
[
i
]
)
(
i
=
1,2
,
…
,
n
)
;
therefore, σ
⊨
ant
ρ
T
⇒
σ
⊨
φ
T
*
ρ
T.G
′ can be obtained through a series of transformations on G. Theorem 20 guarantees that these transformation operations will not change the model’s features on terminal satisfiability.Theorem 21.
For any terminal assertion graphG
=
(
V
,
v
0
,
E
,
a
n
t
,
c
o
n
s
,
E
T
) and any model M,
(40)
T
M
C
(
M
,
G
)
r
e
t
u
r
n
s
t
r
u
e
⟹
M
⊨
T
G
.Proof (G
′ is defined in Theorem 20).
Consider(41)
TMC
returns
true
⟺
SMC
(
M
,
G
′
)
returns
true
⟹
M
⊨
G
′
(
SMC
is
complete
[
3,8
]
)
⟹
M
⊨
T
G
′
(
Theorem
16
)
⟺
M
⊨
T
G
(
Theorem
20
)
.
Theorem21 proves that the TMC algorithm is sound.


### 5.3. The TMC Algorithm Is Complete

Now let us prove the completeness of the algorithm. First, we need the following lemma.Lemma 22 (see [3, 8]).
For anyn
≥
1, e
∈
E, and any s
∈
ψ
n
(
e
), there is a finite initial path ρ and a finite trace σ of some length l
≤
n such that
(42)
ρ
[
l
]
=
e
,
σ
[
l
]
=
s
,
σ
⊨
a
n
t
ρ
.Lemma22 provides a counterexample for the proof of Theorem 25. We can find a path ρ and a trace σ satisfying σ
⊨
ant
ρ but σ
⊭
cons
ρ when TMC returns false. [
ψ
1
,
ψ
2
,
…
,
ψ
n
,
…
] is the simulation sequence used in SMC algorithm; for more, please read [3, 8].Lemma 23 (see [3, 8]).
For alln
≥
1 and e
∈
E,
(43)
ψ
n
(
e
)
⊆
ψ
n
+
1
(
e
)
,
ψ
n
(
e
)
⊆
a
n
t
(
e
)
.According to the results of Lemma23, we can conclude that ψ
n
(
e
)
⊆
φ
T
*
(
e
) when ant
(
e
)
=
φ
T
*
(
e
).Lemma 24.
For a terminal assertion graphG
=
(
V
,
v
0
,
E
,
a
n
t
,
c
o
n
s
,
E
T
) and a model M
=
(
p
r
e
,
p
o
s
t
), let [
φ
1
,
φ
2
,
φ
3
,
…
] be the backward simulation sequence towards E
T
⊆
E. Then, for any n
≥
1, for any e
∈
E, and any state s
∈
φ
n
(
e
), there is a finite path ρ
e which starts from e and a finite trace σ
s which starts from s of some length l (1
≤
l
≤
n
+
1) such that
(44)
ρ
e
[
l
]
∈
E
T
,
σ
s
⊨
a
n
t
ρ
e
.Proof (mathematical induction).
k is a subscripted variable of the simulation sequence φ.
(1) (k
=
1): when e
∈
E
T, we have φ
1
(
e
)
=
ant
(
e
); for all s
∈
φ
1
(
e
), there is a path ρ
e
=
[
e
] of length 1 and a trace σ
s
=
[
s
] such that
(45)
ρ
e
[
1
]
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
When e
∈
E
-
E
T, we have two cases.
Case
1. out
(
e
)
∩
E
T
=
∅, φ
1
(
e
)
=
∅, the conclusion is obvious.
Case
2. out
(
e
)
∩
E
T
≠
∅ and φ
1
(
e
)
≠
∅; according to Definition 17:
(46)
∀
s
∈
φ
1
(
e
)
,
∃
e
+
∈
out
(
e
)
∩
E
T
,
s
.
t
.
s
∈
ant
(
e
)
∩
pre
(
ant
(
e
+
)
)
⟹
s
∈
ant
(
e
)
,
s
∈
pre
(
ant
(
e
+
)
)
;
(47)
⟹
(
46
)
∃
s
′
∈
ant
(
e
+
)
,
s
.
t
.
s
∈
pre
(
s
′
)
,
namely, there is a path ρ
e
=
[
e
e
+
] of length 2 and a trace σ
s
=
[
s
s
′
] such that
(48)
ρ
e
[
2
]
=
e
+
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
(2) Suppose the lemma is true fork
=
n (n is an arbitrary integer), we can get for all e
∈
E, for all s
∈
φ
n
(
e
), there is a finite path ρ
e starting from e and a trace σ
s starting from s of some length l (1
≤
l
≤
n
+
1) such that
(49)
ρ
e
[
l
]
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
(3) Supposek
=
n
+
1 for all e
∈
E and for all s
∈
φ
n
+
1
(
e
), according to Definition 17, we also have two cases.
Case
1.
s
∈
φ
n
(
e
); the lemma is obviously true according to induction hypothesis.
Case
2. Consider
(50)
∃
e
+
∈
out
(
e
)
,
s
.
t
.
s
∈
pre
(
φ
n
(
e
+
)
)
∩
ant
(
e
)
⟹
s
∈
ant
(
e
)
,
s
∈
pre
(
φ
n
(
e
+
)
)
;
(51)
⇒
(
50
)
∃
s
′
∈
φ
n
(
e
+
)
s
.
t
.
s
∈
pre
(
s
′
)
by the induction hypothesis, there exists a path ρ
e
+ of length l (1
≤
l
≤
n
+
1) which starts from e
+ and a trace σ
s
′ which starts from s
′ such that
(52)
ρ
e
+
[
l
]
∈
E
T
,
σ
s
′
⊨
ant
ρ
e
+
.
According to (51), there is a path ρ
e
=
(
e
:
ρ
e
+
) of length l
+
1 and a trace σ
s
=
(
s
:
σ
s
′
) of the same length such that
(53)
ρ
e
[
l
+
1
]
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
(1), (2), and (3) show that the lemma is true.Lemma24 ensures that the counterexample path which we find is the terminal path.Theorem 25.
Consider(54)
T
M
C
(
M
,
G
)
r
e
t
u
r
n
s
f
a
l
s
e
⟹
M
⊯
T
G
.Proof.
Consider(55)
TMC
(
M
,
G
)
returns
false
⟹
SMC
(
M
,
G
′
)
returns
false
;
according to the SMC algorithm, there exists an edge e
1
∈
E such that ψ
*
(
e
1
)
⊈
cons
(
e
1
). Let s
1
∈
ψ
*
(
e
1
)
-
cons
(
e
), according to the Lemma 22, there exists a finite path ρ
1 of length l
1 and a trace σ
1 of the same length such that
(56)
ρ
1
[
l
1
]
=
e
1
,
σ
1
[
l
1
]
=
s
1
,
σ
1
⊨
ant
ρ
1
,
but
σ
1
⊯
cons
ρ
1
.
Whene
1
∈
E
T, ρ
1 is the terminal path. Namely, there exists an initial terminal path ρ
1 and a trace σ
1 of the same length such that σ
1
⊨
ant
ρ
1, σ
1
⊭
cons
ρ
1; according to Definition 14, we get M
⊯
T
G.
Whene
1
∈
E
-
E
T, ρ
1 is not the terminal path, we know s
1
∈
ψ
*
(
e
1
), s
1
∉
cons
(
e
1
). By analyzing Algorithm 1, we find that the terminal assertion graph G is already updated to G
′ when we call the SMC, and every edge in G
′ is labeled with φ
T
*
(
e
)
/
cons
(
e
). In G
′, for all e
∈
E, ant
(
e
)
=
φ
T
*
(
e
). According to Lemma 23, we get s
1
∈
ψ
*
(
e
1
)
⊆
φ
T
*
(
e
1
), s
1
∉
cons
(
e
1
). According to Lemma 24, there exists a finite path ρ
e
1 of length l
2 which starts from e
1 and a trace σ
s
1 of the same length which starts from s
1 such that
(57)
ρ
e
1
[
l
2
]
∈
E
T
,
σ
s
1
⊨
ant
ρ
e
1
.
Sinceρ
1
[
l
1
]
=
ρ
e
1
[
1
]
=
e
1, ρ
1 and ρ
e
1 can be spliced into one path ρ of length l
1
+
l
2
-
1. Since σ
1
[
l
1
]
=
σ
s
1
[
1
]
=
s
1 is true, σ
1 and σ
s
1 can be spliced into one trace σ whose length is l
1
+
l
2
-
1. ρ is a terminal path and such that
(58)
ρ
[
l
1
+
l
2
-
1
]
∈
E
T
,
σ
⊨
ant
ρ
,
σ
⊭
cons
ρ
.
According to Definition14, we get M
⊯
T
G.Algorithm 1:TMC(
M
,
G
).
Input: the model M and terminal assertion graph G.
Output: true: model terminally satisfies the terminal assertion graph.
false: model doesn't satisfy the terminal assertion graph.
(1) repeat
(2)G
old
:
=
G;
(3)φ
T
*:= the fix-point of the backward simulation sequence towards E
T;
(4)G:= replace the antecedent function in G with φ
T
*;
(5) untilG
=
G
old;
(6) SMC(
M
,
G
);
(7) end.Theorem25 proves that the TMC algorithm is complete.


## 5.1. The Logic of Algorithm

M
⊨
T
G
⇔ for all ρ
T in G, for all σ in M of the same length, and (
M
,
σ
)
⊨
T
(
G
,
ρ
T
)
⇔ for all ρ
T in G and for all σ in M of the same length,
(19)
(
M
,
σ
)
⊨
ant
(
G
,
ρ
T
)
⟹
(
M
,
σ
)
⊨
cons
(
G
,
ρ
T
)
.
By analyzing algorithm TMC, in the end, we use SMC
(
M
,
G
′
). Consider
(20)
SMC
(
M
,
G
′
)
returns
true
⟹
M
⊨
G
′
.
It indicates that we can only get
(21)
∀
ρ
in
G
,
∀
σ
in
M
of
the
same
length
,
(
M
,
σ
)
⊨
φ
T
*
(
G
,
ρ
)
⟹
(
M
,
σ
)
⊨
cons
(
G
,
ρ
)
.
But we are aiming at (according to (19))
(22)
∀
ρ
T
in
G
,
∀
σ
in
M
of
the
same
length
,
(
M
,
σ
)
⊨
ant
(
G
,
ρ
T
)
⟹
(
M
,
σ
)
⊨
cons
(
G
,
ρ
T
)
.
Then, if we want to prove TMC is correct, we must prove that (according to (21) and (22))
(23)
∀
ρ
T
in
G
,
∀
σ
in
M
of
the
same
length
,
(
M
,
σ
)
⊨
ant
(
G
,
ρ
T
)
⟹
(
M
,
σ
)
⊨
φ
T
*
(
G
,
ρ
T
)
.


## 5.2. The TMC Algorithm Is Sound

According to Definition17, we get the following lemma.Lemma 19.
For a terminal assertion graphG
=
(
V
,
v
0
,
E
,
a
n
t
,
c
o
n
s
,
E
T
) and a model M
=
(
p
r
e
,
p
o
s
t
), let [
φ
1
,
φ
2
,
φ
3
,
…
] be the backward simulation sequence towards E
T
⊆
E. Then for any n
≥
2, for all finite terminal paths ρ
T, and all finite traces σ of length n
+
1, such that (1)
ρ
T
[
n
+
1
]
∈
E
T
(2)
when
σ
2
⊨
a
n
t
ρ
T
2
and
|
σ
2
|
=
|
ρ
T
2
|
=
n
, we have
σ
[
i
]
∈
φ
n
+
1
-
i
(
ρ
T
[
i
]
)
(
i
=
2,3
,
…
,
n
) (note:
ρ
T
2
represents all paths of length
n
which are obtained by traversing backwards starting from the terminal edge. For example, if
ρ
T
=
e
1
e
2
⋯
e
n
e
n
+
1
and
e
n
+
1
∈
E
T
, then
ρ
T
2
=
e
2
e
3
⋯
e
n
e
n
+
1
,
σ
2
represents all traces of length
n
obtained by traversing backwards starting from the last state of
σ
)
(3)
when
σ
⊨
a
n
t
ρ
T
, we have
σ
[
1
]
∈
φ
n
(
ρ
T
[
1
]
)
,
σ
[
n
+
1
]
∈
φ
1
(
ρ
T
[
n
+
1
]
)
.Proof (mathematical induction).
Suppose|
ρ
T
|
=
|
σ
|
=
k
+
1.
First Step
(
k
=
2
). (1) ρ
T
[
3
]
∈
E
T since ρ
T is a terminal path.
(2) Let us proveσ
[
2
]
∈
φ
1
(
ρ
T
[
2
]
):
(24)
σ
2
⊨
ant
ρ
T
2
⟹
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
,
σ
[
3
]
∈
ant
(
ρ
T
[
3
]
)
,
(25)
σ
[
2
]
∈
pre
(
σ
[
3
]
)
⟹
(
24
)
σ
[
2
]
∈
pre
(
ant
(
ρ
T
[
3
]
)
)
.
According to (24)-(25),
(26)
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
∩
pre
(
ant
(
ρ
T
[
3
]
)
)
⊆
φ
1
(
ρ
T
[
2
]
)
.
(3) Let us proveσ
[
1
]
∈
φ
2
(
ρ
T
[
1
]
), σ
[
3
]
∈
φ
1
(
ρ
T
[
3
]
):
(27)
σ
[
1
]
∈
pre
(
σ
[
2
]
)
⟹
(
26
)
σ
[
1
]
∈
pre
(
φ
1
(
ρ
T
[
2
]
)
)
(28)
σ
⊨
ant
ρ
T
⟹
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
.
According to (27)-(28),
(29)
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
∩
pre
(
φ
1
(
ρ
T
[
2
]
)
)
⊆
φ
1
(
ρ
T
[
1
]
)
∪
(
⋃
e
+
∈
out
(
ρ
T
[
1
]
)
(
pre
(
φ
1
(
e
+
)
)
∩
ant
(
ρ
T
[
1
]
)
)
)
=
φ
2
(
ρ
T
[
1
]
)
,
σ
⊨
ant
ρ
T
⟹
σ
[
3
]
∈
ant
(
ρ
T
[
3
]
)
=
φ
1
(
ρ
T
[
3
]
)
.
Then, the conclusions (1), (2), and (3) are true for k
=
2.
Second Step. We already saw that the conclusions are true for k
=
2. Assume this, for an arbitrary n, the above lemma is true for k
=
n, then we get the following.
(σ represents all traces of length n
+
1 and ρ
T represents all terminal paths of the same length) (1) ρ
T
[
n
+
1
]
∈
E
T. (2) When σ
2
⊨
ant
ρ
T
2, we have σ
[
i
]
∈
φ
n
+
1
-
i
(
ρ
T
[
i
]
) (i
=
2,3
,
…
,
n) (where ρ
T
2 represents all paths of length k obtained by traversing backwards starting from the terminal edge; the terminal edge is the last edge of the terminal path; σ
2 is similar), (3) when σ
⊨
ant
ρ
T, we have σ
[
1
]
∈
φ
n
(
ρ
T
[
1
]
), σ
[
n
+
1
]
∈
φ
1
(
ρ
T
[
n
+
1
]
).
Third Step (let us derive the lemma is true for
k
=
n
+
1
from above assumption). We must consider all terminal paths ρ
T of length n
+
2 and all traces of the same length.
(1)ρ
T
[
n
+
2
]
∈
E
T since ρ
T is a terminal path.
(2) We must proveσ
2
⊨
ant
ρ
T
2
⇒
σ
[
i
]
∈
φ
n
+
2
-
i
(
ρ
T
[
i
]
) (i
=
2,3
,
…
,
n
,
n
+
1) at this step, |
ρ
T
2
|
=
|
σ
2
|
=
n
+
1
(30)
σ
2
⊨
ant
ρ
T
2
⟹
σ
3
⊨
ant
ρ
T
3
,
where ρ
T
3 represents all paths of length n obtained by traversing starting from the terminal edge and σ
3 is obtained by deleting the first two states of σ, |
σ
|
=
n
+
2
⇒
|
σ
3
|
=
n, and |
ρ
T
|
=
n
+
2
⇒
|
ρ
T
3
|
=
n. By the induction hypothesis we have the following conclusion:
(31)
σ
3
⊨
ant
ρ
T
3
⟹
σ
[
i
]
∈
φ
n
+
1
-
i
(
ρ
T
[
i
]
)
⊆
φ
n
+
2
-
i
(
ρ
T
[
i
]
)
,
(
i
=
3,4
,
…
,
n
,
n
+
1
)
.
According to (31),
(32)
σ
[
3
]
∈
φ
n
-
1
(
ρ
T
[
3
]
)
,
(33)
σ
[
2
]
∈
pre
(
σ
[
3
]
)
⟹
(
32
)
σ
[
2
]
∈
pre
(
φ
n
-
1
(
ρ
T
[
3
]
)
)
,
(34)
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
⟹
(
33
)
σ
[
2
]
∈
ant
(
ρ
T
[
2
]
)
∩
pre
(
φ
n
-
1
(
ρ
T
[
3
]
)
)
⊆
φ
n
-
1
(
ρ
T
[
2
]
)
∪
(
⋃
e
+
∈
out
(
ρ
T
[
2
]
)
(
pre
(
φ
n
-
1
(
e
+
)
)
∩
ant
(
ρ
T
[
2
]
)
)
)
=
φ
n
(
ρ
T
[
2
]
)
,
namely, σ
2
⊨
ant
ρ
T
2
⇒
σ
[
i
]
∈
φ
n
+
2
-
i
(
ρ
T
[
i
]
) (i
=
2,3
,
…
,
n
,
n
+
1).
(3) Consider(35)
σ
⊨
ant
ρ
T
⟹
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
,
(36)
σ
⊨
ant
ρ
T
⟹
σ
2
⊨
ant
ρ
T
2
⟹
(
34
)
σ
[
2
]
∈
φ
n
(
ρ
T
[
2
]
)
,
(37)
σ
[
1
]
∈
pre
(
σ
[
2
]
)
⟹
(
36
)
σ
[
1
]
∈
pre
(
φ
n
(
ρ
T
[
2
]
)
)
.
According to (35)–(37),
(38)
σ
[
1
]
∈
ant
(
ρ
T
[
1
]
)
∩
pre
(
φ
n
(
ρ
T
[
2
]
)
)
⊆
φ
n
(
ρ
T
[
1
]
)
∪
(
⋃
e
+
∈
out
(
ρ
T
[
1
]
)
(
pre
(
φ
n
(
e
+
)
)
∩
ant
(
ρ
T
[
1
]
)
)
)
=
φ
n
+
1
(
ρ
T
[
1
]
)
,
σ
⊨
ant
ρ
T
⟹
σ
[
n
+
2
]
∈
ant
(
ρ
T
[
n
+
2
]
)
=
φ
1
(
ρ
T
[
n
+
2
]
)
which exactly means that the lemma holds for k
=
n
+
1. Therefore, the lemma is true for all n starting with 2.The conclusions of Lemma19 have been used to prove Theorem 20. At the same time, Lemma 19 gives the conclusion that the backward simulation sequence φ
n is a convergent sequence. If the length of the path is n, then the simulation sequence of the ith edges will reach the fixed point through at least n
+
1
-
i iterations.Supposeφ
T
* is the fix-point of the backward simulation sequence based on the terminal set E
T; after replacing the label ant of each edge with the corresponding fix-point φ
T
*, the resulting assertion graph is denoted by G
′.Theorem 20.
Consider(
*
)
M
⊨
T
G
⟺
M
⊨
T
G
′
.Proof.
According to Section5.1 (the logic of algorithm), we know (
*
) holds equivalent to the following (
*
*
). For any n
≥
2, ρ
T represents all terminal paths of length n in assertion graph G (ρ
T is also the terminal path in assertion graph G
′) and σ represents all traces of the same length in model M. Consider
(
*
*
)
σ
⊨
ant
ρ
T
⟺
σ
⊨
φ
T
*
ρ
T
.
The direction ⇐ is obvious, since φ
T
*
(
e
)
⊆
ant
(
e
) for any e
∈
E.
The direction⇒: when σ
⊨
ant
ρ
T, according to Lemma 19,
(39)
σ
[
i
]
∈
φ
T
*
(
ρ
T
[
i
]
)
(
i
=
1,2
,
…
,
n
)
;
therefore, σ
⊨
ant
ρ
T
⇒
σ
⊨
φ
T
*
ρ
T.G
′ can be obtained through a series of transformations on G. Theorem 20 guarantees that these transformation operations will not change the model’s features on terminal satisfiability.Theorem 21.
For any terminal assertion graphG
=
(
V
,
v
0
,
E
,
a
n
t
,
c
o
n
s
,
E
T
) and any model M,
(40)
T
M
C
(
M
,
G
)
r
e
t
u
r
n
s
t
r
u
e
⟹
M
⊨
T
G
.Proof (G
′ is defined in Theorem 20).
Consider(41)
TMC
returns
true
⟺
SMC
(
M
,
G
′
)
returns
true
⟹
M
⊨
G
′
(
SMC
is
complete
[
3,8
]
)
⟹
M
⊨
T
G
′
(
Theorem
16
)
⟺
M
⊨
T
G
(
Theorem
20
)
.
Theorem21 proves that the TMC algorithm is sound.


## 5.3. The TMC Algorithm Is Complete

Now let us prove the completeness of the algorithm. First, we need the following lemma.Lemma 22 (see [3, 8]).
For anyn
≥
1, e
∈
E, and any s
∈
ψ
n
(
e
), there is a finite initial path ρ and a finite trace σ of some length l
≤
n such that
(42)
ρ
[
l
]
=
e
,
σ
[
l
]
=
s
,
σ
⊨
a
n
t
ρ
.Lemma22 provides a counterexample for the proof of Theorem 25. We can find a path ρ and a trace σ satisfying σ
⊨
ant
ρ but σ
⊭
cons
ρ when TMC returns false. [
ψ
1
,
ψ
2
,
…
,
ψ
n
,
…
] is the simulation sequence used in SMC algorithm; for more, please read [3, 8].Lemma 23 (see [3, 8]).
For alln
≥
1 and e
∈
E,
(43)
ψ
n
(
e
)
⊆
ψ
n
+
1
(
e
)
,
ψ
n
(
e
)
⊆
a
n
t
(
e
)
.According to the results of Lemma23, we can conclude that ψ
n
(
e
)
⊆
φ
T
*
(
e
) when ant
(
e
)
=
φ
T
*
(
e
).Lemma 24.
For a terminal assertion graphG
=
(
V
,
v
0
,
E
,
a
n
t
,
c
o
n
s
,
E
T
) and a model M
=
(
p
r
e
,
p
o
s
t
), let [
φ
1
,
φ
2
,
φ
3
,
…
] be the backward simulation sequence towards E
T
⊆
E. Then, for any n
≥
1, for any e
∈
E, and any state s
∈
φ
n
(
e
), there is a finite path ρ
e which starts from e and a finite trace σ
s which starts from s of some length l (1
≤
l
≤
n
+
1) such that
(44)
ρ
e
[
l
]
∈
E
T
,
σ
s
⊨
a
n
t
ρ
e
.Proof (mathematical induction).
k is a subscripted variable of the simulation sequence φ.
(1) (k
=
1): when e
∈
E
T, we have φ
1
(
e
)
=
ant
(
e
); for all s
∈
φ
1
(
e
), there is a path ρ
e
=
[
e
] of length 1 and a trace σ
s
=
[
s
] such that
(45)
ρ
e
[
1
]
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
When e
∈
E
-
E
T, we have two cases.
Case
1. out
(
e
)
∩
E
T
=
∅, φ
1
(
e
)
=
∅, the conclusion is obvious.
Case
2. out
(
e
)
∩
E
T
≠
∅ and φ
1
(
e
)
≠
∅; according to Definition 17:
(46)
∀
s
∈
φ
1
(
e
)
,
∃
e
+
∈
out
(
e
)
∩
E
T
,
s
.
t
.
s
∈
ant
(
e
)
∩
pre
(
ant
(
e
+
)
)
⟹
s
∈
ant
(
e
)
,
s
∈
pre
(
ant
(
e
+
)
)
;
(47)
⟹
(
46
)
∃
s
′
∈
ant
(
e
+
)
,
s
.
t
.
s
∈
pre
(
s
′
)
,
namely, there is a path ρ
e
=
[
e
e
+
] of length 2 and a trace σ
s
=
[
s
s
′
] such that
(48)
ρ
e
[
2
]
=
e
+
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
(2) Suppose the lemma is true fork
=
n (n is an arbitrary integer), we can get for all e
∈
E, for all s
∈
φ
n
(
e
), there is a finite path ρ
e starting from e and a trace σ
s starting from s of some length l (1
≤
l
≤
n
+
1) such that
(49)
ρ
e
[
l
]
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
(3) Supposek
=
n
+
1 for all e
∈
E and for all s
∈
φ
n
+
1
(
e
), according to Definition 17, we also have two cases.
Case
1.
s
∈
φ
n
(
e
); the lemma is obviously true according to induction hypothesis.
Case
2. Consider
(50)
∃
e
+
∈
out
(
e
)
,
s
.
t
.
s
∈
pre
(
φ
n
(
e
+
)
)
∩
ant
(
e
)
⟹
s
∈
ant
(
e
)
,
s
∈
pre
(
φ
n
(
e
+
)
)
;
(51)
⇒
(
50
)
∃
s
′
∈
φ
n
(
e
+
)
s
.
t
.
s
∈
pre
(
s
′
)
by the induction hypothesis, there exists a path ρ
e
+ of length l (1
≤
l
≤
n
+
1) which starts from e
+ and a trace σ
s
′ which starts from s
′ such that
(52)
ρ
e
+
[
l
]
∈
E
T
,
σ
s
′
⊨
ant
ρ
e
+
.
According to (51), there is a path ρ
e
=
(
e
:
ρ
e
+
) of length l
+
1 and a trace σ
s
=
(
s
:
σ
s
′
) of the same length such that
(53)
ρ
e
[
l
+
1
]
∈
E
T
,
σ
s
⊨
ant
ρ
e
.
(1), (2), and (3) show that the lemma is true.Lemma24 ensures that the counterexample path which we find is the terminal path.Theorem 25.
Consider(54)
T
M
C
(
M
,
G
)
r
e
t
u
r
n
s
f
a
l
s
e
⟹
M
⊯
T
G
.Proof.
Consider(55)
TMC
(
M
,
G
)
returns
false
⟹
SMC
(
M
,
G
′
)
returns
false
;
according to the SMC algorithm, there exists an edge e
1
∈
E such that ψ
*
(
e
1
)
⊈
cons
(
e
1
). Let s
1
∈
ψ
*
(
e
1
)
-
cons
(
e
), according to the Lemma 22, there exists a finite path ρ
1 of length l
1 and a trace σ
1 of the same length such that
(56)
ρ
1
[
l
1
]
=
e
1
,
σ
1
[
l
1
]
=
s
1
,
σ
1
⊨
ant
ρ
1
,
but
σ
1
⊯
cons
ρ
1
.
Whene
1
∈
E
T, ρ
1 is the terminal path. Namely, there exists an initial terminal path ρ
1 and a trace σ
1 of the same length such that σ
1
⊨
ant
ρ
1, σ
1
⊭
cons
ρ
1; according to Definition 14, we get M
⊯
T
G.
Whene
1
∈
E
-
E
T, ρ
1 is not the terminal path, we know s
1
∈
ψ
*
(
e
1
), s
1
∉
cons
(
e
1
). By analyzing Algorithm 1, we find that the terminal assertion graph G is already updated to G
′ when we call the SMC, and every edge in G
′ is labeled with φ
T
*
(
e
)
/
cons
(
e
). In G
′, for all e
∈
E, ant
(
e
)
=
φ
T
*
(
e
). According to Lemma 23, we get s
1
∈
ψ
*
(
e
1
)
⊆
φ
T
*
(
e
1
), s
1
∉
cons
(
e
1
). According to Lemma 24, there exists a finite path ρ
e
1 of length l
2 which starts from e
1 and a trace σ
s
1 of the same length which starts from s
1 such that
(57)
ρ
e
1
[
l
2
]
∈
E
T
,
σ
s
1
⊨
ant
ρ
e
1
.
Sinceρ
1
[
l
1
]
=
ρ
e
1
[
1
]
=
e
1, ρ
1 and ρ
e
1 can be spliced into one path ρ of length l
1
+
l
2
-
1. Since σ
1
[
l
1
]
=
σ
s
1
[
1
]
=
s
1 is true, σ
1 and σ
s
1 can be spliced into one trace σ whose length is l
1
+
l
2
-
1. ρ is a terminal path and such that
(58)
ρ
[
l
1
+
l
2
-
1
]
∈
E
T
,
σ
⊨
ant
ρ
,
σ
⊭
cons
ρ
.
According to Definition14, we get M
⊯
T
G.Algorithm 1:TMC(
M
,
G
).
Input: the model M and terminal assertion graph G.
Output: true: model terminally satisfies the terminal assertion graph.
false: model doesn't satisfy the terminal assertion graph.
(1) repeat
(2)G
old
:
=
G;
(3)φ
T
*:= the fix-point of the backward simulation sequence towards E
T;
(4)G:= replace the antecedent function in G with φ
T
*;
(5) untilG
=
G
old;
(6) SMC(
M
,
G
);
(7) end.Theorem25 proves that the TMC algorithm is complete.


## 6. Conclusions

This paper has presented a theoretical and experimental study of the TMC process and related concepts, such as terminal assertion graph, terminal path, and terminal satisfiability. Under the basis of the concept mentioned above, to improve the efficiency of the method SMC and solve its limitation, this paper presented an algorithm TMC. The approach TMC is explained and discussed thoroughly in the body of the paper. Then, we use the hardware circuit round-robin arbiter to specify that TMC can be used in industry successfully. In the end, this paper proves that our approach is sound and complete. The method outlined here can be used to deal with finite specifications. It remains to be determined whether our approach will be suitable for infinite specifications.



---

*Source: 725275-2014-05-15.xml*