SAT-based Distributed Reactive Control Protocol Synthesis for Boolean Networks

TL;DR

This paper presents a SAT-based method for synthesizing distributed reactive control protocols for Boolean networks, ensuring global specifications are met through local contracts and control protocols derived from a DAG structure.

Contribution

It introduces a novel SAT-based approach for distributed control synthesis using assumption-guarantee contracts in Boolean networks, with recursive local protocol computation.

Findings

Successfully applied to an aircraft electric power system example.

Reduces control synthesis to QSAT problems for efficiency.

Provides structural insights affecting algorithm completeness.

Abstract

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.