Quantitative model checking for a controller design

Abstract

A controller design method based on a quantitative model checking technique is proposed. Controllers have been designed to shape the closed-loop system’s responses to meet certain requirements. We use Linear Temporal Logic for Control (LTLC) [16] to formally describe complex requirements and design a controller to meet the requirements with guidance from model checking results. The technique can help design a controller robust against errors systematically hampering the controller’s efforts. To demonstrate the usefulness of the proposed technique, we exercised several controller design examples with different types of errors.