Application of Model-Checking Technology to Controller Synthesis

Alexandre David, Jacob Deleuran Grunnet, Jan Jacob Jessen, Kim Guldstrand Larsen, Jacob Illum Rasmussen

Research output: Contribution to journalConference article in JournalResearchpeer-review

8 Citations (Scopus)

Abstract

In this paper we present two frameworks that have been
implemented to link traditional model-checking techniques to the domain
of control. The techniques are based on solving a timed game and using
the resulting solution (a strategy) as a controller. The obtained discrete
controller must fit within its continuous environment, which is modelled
and taken care of in our frameworks. Our first technique does it by using
Matlab to discretise the problem and then Uppaal-tiga to solve the
obtained timed game. This is implemented as a toolbox. The second
technique relies on the user defining a timed game model in Uppaal-
tiga. Then the strategy is automatically imported in Simulink as an
S-function for simulation and validation purposes. We demonstrate the
effectiveness of these frameworks in different case-studies.
Original languageEnglish
Book seriesLecture Notes in Computer Science
Volume6957
Pages (from-to)336-351
Number of pages16
ISSN0302-9743
DOIs
Publication statusPublished - 2011
Event9th International Symposium on Formal Methods for Components and Objects - Graz, Austria
Duration: 29 Nov 20101 Dec 2010
Conference number: 9

Conference

Conference9th International Symposium on Formal Methods for Components and Objects
Number9
CountryAustria
CityGraz
Period29/11/201001/12/2010

Fingerprint

Model checking
Model Checking
Synthesis
Game
Controller
Controllers
Simulink
Demonstrate
Framework
Simulation
Strategy
Model

Cite this

David, Alexandre ; Grunnet, Jacob Deleuran ; Jessen, Jan Jacob ; Larsen, Kim Guldstrand ; Rasmussen, Jacob Illum. / Application of Model-Checking Technology to Controller Synthesis. In: Lecture Notes in Computer Science. 2011 ; Vol. 6957. pp. 336-351.
@inproceedings{a6299d6085634cd5a7a29e2a6cdba475,
title = "Application of Model-Checking Technology to Controller Synthesis",
abstract = "In this paper we present two frameworks that have beenimplemented to link traditional model-checking techniques to the domainof control. The techniques are based on solving a timed game and usingthe resulting solution (a strategy) as a controller. The obtained discretecontroller must fit within its continuous environment, which is modelledand taken care of in our frameworks. Our first technique does it by usingMatlab to discretise the problem and then Uppaal-tiga to solve theobtained timed game. This is implemented as a toolbox. The secondtechnique relies on the user defining a timed game model in Uppaal-tiga. Then the strategy is automatically imported in Simulink as anS-function for simulation and validation purposes. We demonstrate theeffectiveness of these frameworks in different case-studies.",
author = "Alexandre David and Grunnet, {Jacob Deleuran} and Jessen, {Jan Jacob} and Larsen, {Kim Guldstrand} and Rasmussen, {Jacob Illum}",
year = "2011",
doi = "10.1007/978-3-642-25271-6_18",
language = "English",
volume = "6957",
pages = "336--351",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Physica-Verlag",

}

Application of Model-Checking Technology to Controller Synthesis. / David, Alexandre; Grunnet, Jacob Deleuran; Jessen, Jan Jacob; Larsen, Kim Guldstrand; Rasmussen, Jacob Illum.

In: Lecture Notes in Computer Science, Vol. 6957, 2011, p. 336-351.

Research output: Contribution to journalConference article in JournalResearchpeer-review

TY - GEN

T1 - Application of Model-Checking Technology to Controller Synthesis

AU - David, Alexandre

AU - Grunnet, Jacob Deleuran

AU - Jessen, Jan Jacob

AU - Larsen, Kim Guldstrand

AU - Rasmussen, Jacob Illum

PY - 2011

Y1 - 2011

N2 - In this paper we present two frameworks that have beenimplemented to link traditional model-checking techniques to the domainof control. The techniques are based on solving a timed game and usingthe resulting solution (a strategy) as a controller. The obtained discretecontroller must fit within its continuous environment, which is modelledand taken care of in our frameworks. Our first technique does it by usingMatlab to discretise the problem and then Uppaal-tiga to solve theobtained timed game. This is implemented as a toolbox. The secondtechnique relies on the user defining a timed game model in Uppaal-tiga. Then the strategy is automatically imported in Simulink as anS-function for simulation and validation purposes. We demonstrate theeffectiveness of these frameworks in different case-studies.

AB - In this paper we present two frameworks that have beenimplemented to link traditional model-checking techniques to the domainof control. The techniques are based on solving a timed game and usingthe resulting solution (a strategy) as a controller. The obtained discretecontroller must fit within its continuous environment, which is modelledand taken care of in our frameworks. Our first technique does it by usingMatlab to discretise the problem and then Uppaal-tiga to solve theobtained timed game. This is implemented as a toolbox. The secondtechnique relies on the user defining a timed game model in Uppaal-tiga. Then the strategy is automatically imported in Simulink as anS-function for simulation and validation purposes. We demonstrate theeffectiveness of these frameworks in different case-studies.

U2 - 10.1007/978-3-642-25271-6_18

DO - 10.1007/978-3-642-25271-6_18

M3 - Conference article in Journal

VL - 6957

SP - 336

EP - 351

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -