Realizability of Scenario-Based Specifications

  • Yves Bontemps

Student thesis: Master types › Master in Computer science

Abstract

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 of Award2003
Original languageEnglish
SupervisorPierre Yves Schobbens (Supervisor)

Keywords

  • Live Sequence Charts
  • Scenarios
  • Reactive Systems
  • Synthesis
  • Realizability
  • Game Theory
  • Automata Theory

Cite this

Documents

  • File: application/pdf, 225 bytes

    Type: Text

Links

'