Download PROSYD: - Verimag

nonempty language. If the initial state is in the winning region, the language of
ANBTk is not empty and we extract a witness.
Since ANBTk is a subset of ANBTk+1 , we can reuse all results obtained when computing language emptiness on ANBTk to compute language emptiness on ANBTk+1 .
Moreover, it follows from Miyano and Hayashi’s construction that if L(A(S,O) ) 6= 0/
′ ′
/ We may use this fact to further speed up the
and S ⊆ S′ , then L(A(S ,O ) ) 6= 0.
computation of language emptiness, and especially to reuse information obtained
computing language emptiness on ANBTk for larger k.
A witness for nonemptiness corresponds to a winning attractor strategy [Tho95].
The winning strategy follows the µ-iterations of the final ν-computation of WB (α):
From a state q 6∈ α we go to a state q′ from which the protagonist can force a shorter
path to an accepting state. In an accepting state we move back to an arbitrary state
in the winning region.
If a strategy exists, it corresponds to a complete Σ-labeled D-tree and thus to a
Moore machine M. The states of M are the states of ANBTk that are reachable when
the strategy is followed, and the edges are given by the strategy.
To minimize the strategy, we compute the simulation relation and apply Theorem 4, which is equivalent to using the classical FSM minimization algorithm
[HU79]. Thus, the optimized strategy is guaranteed to be minimal with respect
to its given I/O language. The output of our tool is a state machine described in
V ERILOG that implements this strategy.
30 • Underlying Theory
Property-Based Synthesis Tool