Abstract
We propose here Live Sequence Charts with a new, game-based semantics to model interactions between the system and its environment. For constructing programs automatically, we give an algorithm to synthesize either a strategy for the system ensuring that the specification is respected, or, if the specification is unimplementable, a strategy for the environment forcing the system to fail. We introduce the concept of mercifulness, a desirable property of the synthesized program. We give a polynomial time algorithm for synthesizing merciful winning strategies.
Original language | English |
---|---|
Pages (from-to) | 139-169 |
Number of pages | 31 |
Journal | Fundamenta Informaticae |
Volume | 62 |
Issue number | 2 |
Publication status | Published - 1 Sept 2004 |