Synthesis of Open Reactive Systems from Scenario-Based Specifications

Issue title: Application of Concurrency to System Design (ACSD'03)

Article type: Research Article

Authors: Bontemps, Yves^; | Schobbens, Pierre-Yves^; | Löding, Christof

Affiliations: Computer Science Department, University of Namur Namur, Belgium | FUNDP, Institut d'Informatique, 21, rue Grandgagnage, B5000 - Namur (Belgium) | Lehrstuhl für Informatik VII, RWTH Aachen, Aachen, Germany

Abstract: We propose here Live Sequence Charts with a new, game-based semantics to model interactions between the system and its environment. For constructing programs automatically, we give an algorithm to synthesize either a strategy for the system ensuring that the specification is respected, or, if the specification is unimplementable, a strategy for the environment forcing the system to fail. We introduce the concept of mercifulness, a desirable property of the synthesized program. We give a polynomial time algorithm for synthesizing merciful winning strategies.

Journal: Fundamenta Informaticae, vol. 62, no. 2, pp. 139-169, 2004