430
S. Wimmer and J. von Mutius
l 2 , 0 < c 1 ≤ 1 ∧ c 2 = 0
l 2 , c 1 = 0 ∧ c 2 < 1
l 2 , c 1 = 0 ∧ c 2 < 2
· · ·
l 2 , c 1 = 0 ∧ c 2 ≤ 100
l 1 , c 1 = c 2 = 0
Fig. 2: The zone graph of the automaton depicted in Figure 1.
while the dashed edge indicates that the zone at its tail has a successor in the
zone graph ((l 2 , {u | u |= c 1 = 0 ∧ c 2 < 1})) that is subsumed by the tip of
the edge. The set of these three states can act as a certificate of unreachability.
They essentially form an inductive invariant of the zone graph: for each state in
the certificate, all its successors in the zone graph are either contained in the
certificate themselves or subsumed by another state in the certificate. Thus we
know that any symbolic state that is reachable from the initial state is subsumed
by some state in the certificate, and as the final state is not contained in the
certificate, we can conclude that it is unreachable.
Figure 3b shows a certificate with only two states that replaces the two states
for l 2 by the state with a dashed border. Note that this state is not part of the
original zone graph. The certificate fulfills the same invariant property and thus
also proves unreachability. We will use this technique of adding larger states to
the certificate that are not part of the zone graph for our compression techniques
in section 4.
l 2 , 0 < c 1 ≤ 1 ∧ c 2 = 0
l 1 , c 1 = c 2 = 0
l 2 , c 1 = 0 ∧ c 2 ≤ 100
(a) Stored states
l 1 , c 1 = c 2 = 0
l 2 , c 2 ≤ 100
(b) Smaller certificate
Fig. 3: Two certificates of unreachability for the automaton from Figure 1.
S. Wimmer and J. von Mutius
l 2 , 0 < c 1 ≤ 1 ∧ c 2 = 0
l 2 , c 1 = 0 ∧ c 2 < 1
l 2 , c 1 = 0 ∧ c 2 < 2
· · ·
l 2 , c 1 = 0 ∧ c 2 ≤ 100
l 1 , c 1 = c 2 = 0
Fig. 2: The zone graph of the automaton depicted in Figure 1.
while the dashed edge indicates that the zone at its tail has a successor in the
zone graph ((l 2 , {u | u |= c 1 = 0 ∧ c 2 < 1})) that is subsumed by the tip of
the edge. The set of these three states can act as a certificate of unreachability.
They essentially form an inductive invariant of the zone graph: for each state in
the certificate, all its successors in the zone graph are either contained in the
certificate themselves or subsumed by another state in the certificate. Thus we
know that any symbolic state that is reachable from the initial state is subsumed
by some state in the certificate, and as the final state is not contained in the
certificate, we can conclude that it is unreachable.
Figure 3b shows a certificate with only two states that replaces the two states
for l 2 by the state with a dashed border. Note that this state is not part of the
original zone graph. The certificate fulfills the same invariant property and thus
also proves unreachability. We will use this technique of adding larger states to
the certificate that are not part of the zone graph for our compression techniques
in section 4.
l 2 , 0 < c 1 ≤ 1 ∧ c 2 = 0
l 1 , c 1 = c 2 = 0
l 2 , c 1 = 0 ∧ c 2 ≤ 100
(a) Stored states
l 1 , c 1 = c 2 = 0
l 2 , c 2 ≤ 100
(b) Smaller certificate
Fig. 3: Two certificates of unreachability for the automaton from Figure 1.