Information Technology Reference
In-Depth Information
1: definition LBA_bpr_C ::
2:
('q
nat) nres"
"('q, 'l, 'more) LBA_scheme
3: where
4:
A≡ do {
"LBA_bpr_C
QA ;
5:
let Q =
let C = ( ʻ q. 1);
6:
let C' = ( ʻ q. if
FA q then 1 else 2);
7:
8:
let i = 0;
9:
(_, C', _)
10:
WHILEIT
A Q)
11:
(LBA.LBA_bpr__whilei
( ʻ (C, C', i). i>0
−ₒ
= card (C ' Q))
12:
card (C' ' Q)
( ʻ (C, C', i). do {
13:
14:
let i = Suc i;
15:
let C = C';
let f = ( ʻ q. (C q,
LA q,
C ' successors A A q));
16:
17:
let R = f ' Q;
set_enum R;
18:
fi
19:
let C' = fi o f;
20:
RETURN (C, C', i)
21:
}) (C, C', i);
22:
RETURN C'
23:
}"
Fig. 3. BPR colouring
In the formalisation we present here, we use automata that follow [4] but
differ from the standard definition in one important aspect: we assume that
not the edges , but rather the states of automata are labelled. We call those
automata labelled Buchi automata ( LBA ), as opposed to BA . Moreover, in our
representation we have a set of initial states rather than a unique initial state.
Instead of a set of accepting states we use a predicate to express whether a state is
an accepting state or not. This kind of automata representation is suitable in our
context, since we formalise the algorithm in the context of the Buchi automaton
construction from an LTL formula according to [4], where the output automaton
corresponds to a state labelled rather than a transition labelled automaton.
Big parts of our library concern BAs, however, and technically, LBAs are
defined as an extension of the BA record type where labels for the states are
added and the labels for the edges are “disabled”.
4.1 The Bisimulation Reduction Algorithm
The Isabelle formalisation of the algorithm from Fig. 1 is shown in Figure 3.
The formalisation uses the Isabelle refinement framework [6] for writing what
resembles imperative code. We explain some of the syntactic constructs.
Lines 5 to 8 accomplish the initialisation. The let should be understood as
imperative assignment. We assign: Q is the state set of the input automaton
A
; C
 
Search WWH ::




Custom Search