Information Technology Reference
In-Depth Information
[1]). An example of this technique is shown in figure 4 using the Kripke structure of
figure 5.
f
1
g`
E
(
F
p
)
R
F
f
1
g`
E
(
p
)
fg `
E
(
p
)
f
1
g`
E
(
XF
p
)
f
1
;
2
g`
E
(
F
p
)
R
split
f
1
g`
E
(
F
p
)
f
2
g`
E
(
F
p
)
R
F
f
2
g`
E
(
p
)
fg `
E
(
p
)
f
2
g`
E
(
XF
p
)
f
2
;
3
g`
E
(
F
p
)
R
split
f
3
g`
E
(
F
p
)
f
2
g`
E
(
F
p
)
R
F
f
3
g`
E
(
p
)
fg `
E
(
p
)
f
3
g`
E
(
XF
p
)
f
1
;
2
g`
E
(
F
p
)
R
split
f
1
g`
E
(
F
p
)
f
2
g`
E
(
F
p
)
Fig. 4.
Example tableau for on-the-fly model checking of safety properties.
¬
p
1
2
3
¬
p
¬
p
Fig. 5.
Example Kripke structure for on-the-fly checking of safety properties.
Similar heuristics can be used for liveness properties. Consider the Kripke structure
in figure 6 and the property
EG
p
. If we split a sequent as soon it LHS contains a state
that already occurred in a sequent with the same RHS, then the following tableau finds
a witness for
EG
p
with just one image computation:
f
1
g`
E
(
G
p
)
R
G
f
1
g`
E
(
p
;
XG
p
)
R
A
+
f
1
g`
E
(
XG
p
)
R
X
f
1
;
2
g`
E
(
G
p
)
R
split
f
1
g`
E
(
G
p
)
f
2
g`
E
(
G
p
)
Search WWH ::
Custom Search