Application of Model-Checking Technology to Controller Synthesis

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

doi:10.1007/978-3-642-25271-6_18

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 journal › Conference article in Journal › Research › peer-review

9 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 language	English
Book series	Lecture Notes in Computer Science
Volume	6957
Pages (from-to)	336-351
Number of pages	16
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-642-25271-6_18
Publication status	Published - 2011
Event	9th International Symposium on Formal Methods for Components and Objects - Graz, Austria Duration: 29 Nov 2010 → 1 Dec 2010 Conference number: 9

Conference

Conference	9th International Symposium on Formal Methods for Components and Objects
Number	9
Country/Territory	Austria
City	Graz
Period	29/11/2010 → 01/12/2010

Access to Document

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

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@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",

note = "9th International Symposium on Formal Methods for Components and Objects ; Conference date: 29-11-2010 Through 01-12-2010",

}

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

N1 - Conference code: 9

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

SN - 0302-9743

VL - 6957

SP - 336

EP - 351

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 9th International Symposium on Formal Methods for Components and Objects

Y2 - 29 November 2010 through 1 December 2010

ER -

Application of Model-Checking Technology to Controller Synthesis

Abstract

Conference

Access to Document

AUB Link

Fingerprint

Cite this