Abstract
Original language  Undefined 

Awarding Institution 

Supervisors/Advisors 

Thesis sponsors  
Award date  7 Dec 2012 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9789036534871 
DOIs  
Publication status  Published  7 Dec 2012 
Keywords
 imperfect information games
 antichains
 CRI.2.8
 EWI22816
 CRF.4
 safety
 Strategy
 IR82585
 compositional controller synthesis
 METIS290615
Cite this
}
Compositional Synthesis of Safety Controllers. / Kuijper, W.
Enschede : University of Twente, 2012. 184 p.Research output: Thesis › PhD Thesis  Research UT, graduation UT
TY  THES
T1  Compositional Synthesis of Safety Controllers
AU  Kuijper, W.
N1  IPA Ph.D.thesis series no. 201216
PY  2012/12/7
Y1  2012/12/7
N2  In my thesis I investigate compositional techniques for synthesis of safety controllers. A safety controller, in this context, is a state machine that gives the set of safe control outputs for every possible sequence of observations from the plant under control. Compositionality, in this context, refers to the ability to compose the plant model with a safety controller that is derived in a local context, meaning we only consider a selected subsets of the full set of plant model components. The main research question addressed in the thesis is how compositional techniques can have a beneficial effect on scalability. Here scalability applies to the way the running time and memory requirements of the synthesis algorithm increase with the number of plant model components. The working hypothesis was that compositionality should indeed have a beneficial impact on scalability. The intuition behind this is that using compositional techniques we should be able to avoid or at least partly alleviate the type of state explosion problem that is typically seen when synthesizing controllers for larger plant models that consist of the paralel composition of multiple plant model components. The experimental results presented in the thesis are positive in the sense that they indeed support the working hypothesis. We see on a natural example the compositional algorithm exhibits linear scaling behavior whereas the monolithic (non compositional) algorithm exhibits super–exponential scaling behavior. We see this even for an example that intrinsically requires a combination of local control constraints and a global control constraint, where the local constraints are each in turn dependent on a small number of adjacent plant components, whereas the global constraint is intrinsically dependent on all plant model components simultaneously. A first main contribution is a symbolic algorithm that works directly on a compact symbolic representation of the controller thereby avoiding explicit construction of the underlying state graph. The algorithm works by refining the representation of the control strategy in a counterexample driven manner. Upon termination the algorithm will yield a symbolic representation of the most permissive, safe control strategy for the given plant model. The algorithm is specifically designed for models that feature partial observability, meaning that certain internal state of the plant model is not directly observable by the controller. A second main contribution is a compositional technique that also explicitly takes partial observability into account. For this we develop a compositional algorithm that invokes the aforementioned strategy refinement algorithm repeatedly. In particular the compositional algorithm performs a two step synthesis process for each relevant subset of the plant model: (1) computation of the local context which effectively forms a local overapproximation of the allowable behavior, (2) computation of the local controller which effectively forms a local underapproximation of the deniable behavior. We prove that upon termination of the algorithm the context and the controller signatures coincide and we obtain precisely the desired most permissive safety controller, yet constructed in an incremental, compositional fashion. What sets these contributions apart from other contributions in the field is the fact that I consider compositionality in combination with partial observability, and also the fact that the resulting compositional algorithm does not rely on any type of explicit, congruence based state minimization procedure. Even though the two aforementioned main contributions can be considered separately, it may be more informative to view them in combination: it is the compositional algorithm that manages to exploit to the maximal extent the symbolic strategy refinement algorithm that underlies it, or, vice versa, it is the symbolic strategy refinement algorithm that enables the compositional algorithm that relies on it to scale well on larger problem instances.
AB  In my thesis I investigate compositional techniques for synthesis of safety controllers. A safety controller, in this context, is a state machine that gives the set of safe control outputs for every possible sequence of observations from the plant under control. Compositionality, in this context, refers to the ability to compose the plant model with a safety controller that is derived in a local context, meaning we only consider a selected subsets of the full set of plant model components. The main research question addressed in the thesis is how compositional techniques can have a beneficial effect on scalability. Here scalability applies to the way the running time and memory requirements of the synthesis algorithm increase with the number of plant model components. The working hypothesis was that compositionality should indeed have a beneficial impact on scalability. The intuition behind this is that using compositional techniques we should be able to avoid or at least partly alleviate the type of state explosion problem that is typically seen when synthesizing controllers for larger plant models that consist of the paralel composition of multiple plant model components. The experimental results presented in the thesis are positive in the sense that they indeed support the working hypothesis. We see on a natural example the compositional algorithm exhibits linear scaling behavior whereas the monolithic (non compositional) algorithm exhibits super–exponential scaling behavior. We see this even for an example that intrinsically requires a combination of local control constraints and a global control constraint, where the local constraints are each in turn dependent on a small number of adjacent plant components, whereas the global constraint is intrinsically dependent on all plant model components simultaneously. A first main contribution is a symbolic algorithm that works directly on a compact symbolic representation of the controller thereby avoiding explicit construction of the underlying state graph. The algorithm works by refining the representation of the control strategy in a counterexample driven manner. Upon termination the algorithm will yield a symbolic representation of the most permissive, safe control strategy for the given plant model. The algorithm is specifically designed for models that feature partial observability, meaning that certain internal state of the plant model is not directly observable by the controller. A second main contribution is a compositional technique that also explicitly takes partial observability into account. For this we develop a compositional algorithm that invokes the aforementioned strategy refinement algorithm repeatedly. In particular the compositional algorithm performs a two step synthesis process for each relevant subset of the plant model: (1) computation of the local context which effectively forms a local overapproximation of the allowable behavior, (2) computation of the local controller which effectively forms a local underapproximation of the deniable behavior. We prove that upon termination of the algorithm the context and the controller signatures coincide and we obtain precisely the desired most permissive safety controller, yet constructed in an incremental, compositional fashion. What sets these contributions apart from other contributions in the field is the fact that I consider compositionality in combination with partial observability, and also the fact that the resulting compositional algorithm does not rely on any type of explicit, congruence based state minimization procedure. Even though the two aforementioned main contributions can be considered separately, it may be more informative to view them in combination: it is the compositional algorithm that manages to exploit to the maximal extent the symbolic strategy refinement algorithm that underlies it, or, vice versa, it is the symbolic strategy refinement algorithm that enables the compositional algorithm that relies on it to scale well on larger problem instances.
KW  imperfect information games
KW  antichains
KW  CRI.2.8
KW  EWI22816
KW  CRF.4
KW  safety
KW  Strategy
KW  IR82585
KW  compositional controller synthesis
KW  METIS290615
U2  10.3990/1.9789036534871
DO  10.3990/1.9789036534871
M3  PhD Thesis  Research UT, graduation UT
SN  9789036534871
PB  University of Twente
CY  Enschede
ER 