Extending BALM to Synchronous Equations Over co-B¨uchi Specifications - The Unknown Component Problem: Theory and Applications - page 268

Chapter 18
Extending BALM to Synchronous Equations
Over co-B uchi Specifications

18.1 Introduction

Suppose that we consider sequential synthesis problems where the objective is to
find a strategy, implementable as a finite state machine (FSM), which guides a
system to a given subset of states where at least one state is accepting and keeps
it in that subset (e.g., the subset may include a winning state for a game, or a set
of states with some desirable property). Such situations need

-automata to capture
these specifications. For instance, a useful property like liveness is expressed with
Buchi automata.
When, as a special case, the problems we consider are concerned with steering a
system into an accepting set of states and then keeping it there, such requirements
are what can be expressed by co-Buchi automata. In this chapter we will describe a
synthesis flow for co-Buchi specifications. We comment at the end of this chapter
how the synthesis flow that we describe for co-Buchi can be adapted for Buchi
automata.
For co-B uchi specifications, the FSM synthesis problem is stated as usual: if

!

S

is a co-Buchi automaton, is a known FSM, and represents the synchronous

composition of two Buchi automata, find the most general FSM

F

X such that

F X S , i.e., the ! -language represented by the ! -automaton F X is contained

. 1 Fr om Ch ap. 2, we know that in the ! -language represented by the ! -automaton S

D S

the most general automaton solution is given by , where the outside

complementation must deal with the usual non-determinism. Therefore, in general,
ND Buchi and co-Buchi automata complementation are required, which are super-
exponential in complexity. We show how this can be avoided by aiming for a slightly
less general but more efficient solution. We propose a synthesis flow, very similar

X F

1 The consistency of the “types” of automata in the synchronous equation will become clear when
reading the chapter. It suffices to say here that an FSM can be interpreted as a special case of B uchi
or co-B uchi automaton.