SAT-based Distributed Reactive Control Protocol Synthesis for Boolean Networks

Autor:	Sahin, Yunus Emre, Ozay, Necmiye
Rok vydání:	2016
Předmět:	Computer Science - Systems and Control
Druh dokumentu:	Working Paper
Popis:	This paper considers the synthesis of distributed reactive control protocols for a Boolean network in a distributed manner. We start with a directed acyclic graph representing a network of Boolean subsystems and a global contract, given as an assumption-guarantee pair. Assumption captures the environment behavior, and guarantee is the requirements to be satisfied by the system. Local assumption-guarantee contracts, together with local control protocols ensuring these local contracts, are computed recursively for each subsystem based on the partial order structure induced by the directed acyclic graph. By construction, implementing these local control protocols together guarantees the satisfaction of the global assumption-guarantee contract. Moreover, local control protocol synthesis reduces to quantified satisfiability (QSAT) problems in this setting. We also discuss structural properties of the network that affect the completeness of the proposed algorithm. As an application, we show how an aircraft electric power system can be represented as a Boolean network, and we synthesize distributed control protocols from a global assumption-guarantee contract. The assumptions capture possible failures of the system components, and the guarantees capture safety requirements related to power distribution. Comment: This is an extended version of the paper with the same title that will appear in IEEE MSC 2016
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1607.03479 Zobrazit plný text záznamu View this record from Arxiv