RésuméWe propose the language of Live Sequence Charts (LSCs) to specify behavioral properties of reactive systems, with a new, game-based, semantics. This semantics is given in a transparent way and allows analysts to model reactive systems with an assume/guarantee-like paradigm. We present a game-theoretic algorithm for solving the realizability problem for LSC specifications. This algorithm synthesizes finite-state strategies as a by-product, which can be used to help analysts understand better their specification. We define the notion of mercifulness and present an algorithm for synthesizing merciful strategies.
|Date de réussite||2003|
|Superviseur||Pierre-Yves Schobbens (Promoteur)|
Realizability of Scenario-Based Specifications
Bontemps, Y. (Auteur). 2003
Thèse de l'étudiant: Master types › Master en sciences informatiques