Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Contracts and Games in Control...

Contracts and Games in Controller Synthesis for Discrete Systems

Ralph-Johan Back, Cristina Cerschi Seceleanu, Contracts and Games in Controller Synthesis for Discrete Systems. In: Miroslav Sveda Vaclav Dvorak (Ed.), 11th IEEE International Conference on the Engineering of Computer-Based Systems, Brno, Czech Republic, 307-314, IEEE Computer Society, 2004.

Abstract:

This study proposes a method for constructing reliable controllers for
arbitrarily large discrete systems. The controller is synthesized by
finding a winning strategy for specific games defined by contracts. The
discrete system model is an action system, and the requirement is a
temporal property. We use the extended action system notation that allows
both angelic and demonic nondeterminism, such that the game reduces to a
competition between the angel, that is, the controller, and the demon, that
is, the plant, which try to prevent each other from achieving their
respective goals. If the synthesis is possible, i.e., if the angel has a
way to enforce the required property, the process ends with the extraction
of the angelic winning strategy, by propagating certain assertions into the
contract that models the controllable actions. The technique guarantees the
correctness of the derived program. We illustrate our method on a
producer-consumer application.

Files:

Abstract in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpBaCe04a,
  title = {Contracts and Games in Controller Synthesis for Discrete Systems},
  booktitle = {11th IEEE International Conference on the Engineering of Computer-Based Systems, Brno, Czech Republic},
  author = {Back, Ralph-Johan and Cerschi Seceleanu, Cristina},
  editor = {Vaclav Dvorak, Miroslav Sveda},
  publisher = {IEEE Computer Society},
  pages = {307-314},
  year = {2004},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication