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.
Realizability of Scenario-Based Specifications
Bontemps, Y. (Auteur). 2003
Student thesis: Master types › Master en sciences informatiques