Realizability of Scenario-Based Specifications

Thèse de l'étudiant: Master typesMaster en sciences informatiques

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éussite2003
langueAnglais
SuperviseurPierre-Yves Schobbens (Promoteur)

Citer ceci

Realizability of Scenario-Based Specifications
Bontemps, Y. (Auteur). 2003

Thèse de l'étudiant: Master typesMaster en sciences informatiques