A Survey of Relevant Literature - The Unknown Component Problem: Theory and Applications - page 95

weak bisimulation relation (as opposed to language containment in our approach).
The authors derive an automaton representing all traces of the parallel composition
of A and each sequence over the alphabet U [ O. The final state of each trace of the
composition whose I [ O-restriction is not a trace of C is marked as a bad state. To
compute the largest solution, the automaton is augmented with a designated don't
care state that accepts all infeasible sequences, i.e., those that do not occur in the
composition. Finally the .U [ O/-restriction of the automaton is derived and the
result is determinized by subset construction, where each subset including a bad
state is marked as bad. The largest solution is the subset of all sequences of the
.U [ O/-restriction whose runs do not end up in bad states. In [155] the authors
study supervisory control for nodeterministic specifications to design a controller
such that the closed-loop system is bisimilar to the specification. Nondeterministic
plant and specification are studied also in [59], using the trajectory model.

5.2.4 Delay-Insensitive Processes

In the context of modeling delay-insensitive processes and their environments, a
number of concurrency models use various labelings of states of processes to repre-
sent certain properties of states, such as quiescence and error or violation [90, 100].
The existence of state labels requires a stronger semantics than language semantics
and leads to a reflection operator further refining the language complementation
operator. See [90, 100] for discussions on parallel composition operators for delay-
insensitive processes. The largest solution of the equation P k X R is the
process Q .P kQ R/,where k is a composition operator and Q is a reflection
operator, replacing the complementation operator used with language semantics.
As with language semantics, such a solution might not be compositionally .U [
O/-convergent; it is also of interest to look for solutions exhibiting a property
called healthness , capturing correctness properties according to the chosen parallel
composition operator [90].

5.3 ! -Automata, Games, Realizability and Synthesis

Given a game 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 and player-1 does the
same from the finite alphabet ˙ 1 . A play of the game is a finite or infinite sequence
of steps. Player-0 wins the game if the play is in the game language, .˙ 0
˙ 1 / ! ; otherwise, player-1 wins, i.e., when the play is in .
A strategy for a player is a rule that tells the player what symbol to choose at
each instant; a winning strategy is one that insures a win for the player no matter
how the other player behaves. Each player sees the move of the other player at each