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.