Synthesis from scenario-based specifications

We consider the problem of the automatic generation of reactive systems from specifications given in the scenario-based language of live sequence charts (LSCs). We start by extending the language so that it becomes more suitable for synthesis. We then translate a system specification given in the language into a two-player game between the system and the environment. By solving the game, we generate a winning strategy for the system, which corresponds to a correct implementation of the specification. We also define two notions of system correctness, and show how each can be synthesized.

► Automatic generation of reactive systems from Live Sequence Chart specifications. ► LSC language extended to be more suitable for synthesis. ► Synthesis computed by solving a game representation of the specification. ► Two notions of system correctness are defined.