Realizability of Scenario-Based Specifications

  • Yves Bontemps

Student thesis: Master typesMaster en sciences informatiques


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.
la date de réponse2003
langue originaleAnglais
SuperviseurPIERRE-YVES SCHOBBENS (Promoteur)

Contient cette citation