Compositional Synthesis of Safety Controllers

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

70 Downloads (Pure)

Abstract

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.
Original languageUndefined
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • van de Pol, Jaco , Supervisor
Thesis sponsors
Award date7 Dec 2012
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-3487-1
DOIs
Publication statusPublished - 7 Dec 2012

Keywords

  • imperfect information games
  • anti-chains
  • CR-I.2.8
  • EWI-22816
  • CR-F.4
  • safety
  • Strategy
  • IR-82585
  • compositional controller synthesis
  • METIS-290615

Cite this

Kuijper, W.. / Compositional Synthesis of Safety Controllers. Enschede : University of Twente, 2012. 184 p.
@phdthesis{0298630f64024c87bc22951952f8979f,
title = "Compositional Synthesis of Safety Controllers",
abstract = "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.",
keywords = "imperfect information games, anti-chains, CR-I.2.8, EWI-22816, CR-F.4, safety, Strategy, IR-82585, compositional controller synthesis, METIS-290615",
author = "W. Kuijper",
note = "IPA Ph.D.-thesis series no. 2012-16",
year = "2012",
month = "12",
day = "7",
doi = "10.3990/1.9789036534871",
language = "Undefined",
isbn = "978-90-365-3487-1",
publisher = "University of Twente",
address = "Netherlands",
school = "University of Twente",

}

Compositional Synthesis of Safety Controllers. / Kuijper, W.

Enschede : University of Twente, 2012. 184 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

TY - THES

T1 - Compositional Synthesis of Safety Controllers

AU - Kuijper, W.

N1 - IPA Ph.D.-thesis series no. 2012-16

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 - anti-chains

KW - CR-I.2.8

KW - EWI-22816

KW - CR-F.4

KW - safety

KW - Strategy

KW - IR-82585

KW - compositional controller synthesis

KW - METIS-290615

U2 - 10.3990/1.9789036534871

DO - 10.3990/1.9789036534871

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-3487-1

PB - University of Twente

CY - Enschede

ER -