Supervisor Synthesis to Satisfy Safety and Reachability Requirements in Chemical Process Control

A specification expressed in computation tree logic (CTL) that enforces safety and reachability requirements in discrete event systems is proposed. It is shown that the specification has a unique minimal control strategy that maximizes the set of states that satisfy the specification, and an algorithm is provided to calculate the control strategy. The specification captures the idea that the chemical process should always be able to shut down in a safe manner. The algorithm uses established CTL model checking procedures to perform the intermediate calculations, and can incorporate symbolic model checking. The maximum problem size for which a control strategy can be calculated is similar to that of the corresponding verification problem. A small example demonstrates the application of the algorithm to a problem that includes safety and reachability constraints. Current work aims to use the techniques to solve a real process control problem supplied by industry.