Title
Application of model-checking technology to controller synthesis
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.
Year
DOI
Venue
2010
10.1007/978-3-642-25271-6_18
Lecture Notes in Computer Science
Keywords
Field
DocType
traditional model-checking technique,controller synthesis,resulting solution,validation purpose,discrete controller,model-checking technology,continuous environment,game model,different case-studies
Control theory,Model checking,MATLAB,Computer science,Toolbox,Real-time computing,Hybrid system,Linear matrix inequality,Distributed computing
Conference
Citations 
PageRank 
References 
7
0.48
11
Authors
5
Name
Order
Citations
PageRank
Alexandre David1166776.52
Jacob Deleuran Grunnet2122.47
Jan Jessen3294.50
Kim Guldstrand Larsen44434346.88
Jacob Illum Rasmussen51518.00