Hardware Reference
In-Depth Information
step, and the strategy may be a function of the entire history of the game, a game
of perfect information. The game is determined if one of the players has a winning
strategy.
This type of infinite games of perfect information were first considered by Gale
and Stewart [45] (GSP games). If is presented as an !-automaton. we have a Gale-
Stewart game of perfect information on an !-automaton. In this case the winner has
a finite-state strategy implemented by an FSM. Buchi and Landweber [20] gave a
constructive procedure to solve games on !-automata, i.e., to decide the winner
and synthesize the FSM representing the winner's strategy. Solving a game on an
!-automaton is also known as Church's problem [31]. If is a property to be
satisfied by a synchronous digital circuit to be synthesized, what we need to know is
whether the circuit to be synthesized has a winning strategy against its adversarial
environment (problem of
realizability
), and if it exists, we need to find an FSM
realizing a winning strategy subject to the implementation constraints (problem of
synthesis
).
Notice that while for combinational logic synthesis, given a Boolean relation
R
f
0;1
g
n
m
, there is always a Boolean function f
Wf
0;1
g
n
m
f
0;1
g
!f
0;1
g
n
, if there exists
satisfying the relation R, i.e., such that for every i
2f
0;1
g
m
for which .i;o/
2
R,then.i;f.i//
2
R [17], for sequential
logic synthesis this is not always the case. Indeed, the objective of sequential
synthesis is to come up with a sequential circuit that satisfies a property relation
R
2
I
!
o
2f
0;1
g
O
!
specifying for each input sequence the expected output sequences.
Such a circuit can be seen as an FSM whose behavior corresponds to a function
f
W
I
?
!
O such that, for all i
0
i
1
i
2
2
I
!
and f.i
0
/f.i
0
i
1
/f.i
0
i
1
i
2
/
2
O
!
, it holds that .i
0
i
1
i
2
:::;f.i
0
//f.i
0
i
1
/f.i
0
i
1
i
2
/
2
R. Not every property is
realizable, i.e., there is not always an FSM that implements it; e.g., the relation
R
f
0;1
g
!
;b
!
/
2
R is
not realizable [74], because after the first input 0 to decide whether to output a or
b it would need to look into the future to know whether the second input is 1 (and
then output a now) or 0 (and then output b now).
However property synthesis problems arising in practice, such as the synthesis
of the unknown component problem, do no always fall in the paradigm of Gale-
Stewart games of perfect information. To model these synthesis problems, Krishnan
and Brayton [74] proposed and studied the paradigm of two-person Gale-Stewart
games of incomplete information on deterministic !-automata (GSI games). For
these games each player observes only the observable part of the opponent's actions,
on which he has to base his moves. The winner of GSI games can be decided and a
winning strategy synthesized by reducing them to pairs of appropriate GSP games,
at a higher computational cost. Some GSI games are not determined, i.e., there is no
winner with a deterministic winning strategy.
More precisely, GSI games are two person games played between two players:
player-0 and player-1. In a single step of the game player-0 chooses a symbol from
the finite alphabet ˙
0
D
˙
obs
0
!
!
defined by .01
f
0;1
g
!
;a
!
/
2
R and .01
f
0;1
g
f
a;b
g
˙
hid
0
, followed by player-1 choosing a letter from
1
˙
hi
1
. Same as for GSP games, a play of the
game is a finite or infinite sequence of steps. The distinguishing feature of GSI
games (Gale-Stewart games of incomplete information or partial observation) with
D
˙
obs
the finite alphabet ˙
1
Search WWH ::
Custom Search