Conflict-Tolerant Specifications for Hybrid Systems

Deepak D'Souza, Madhu Gopinathan, S.Ramesh, Prahladavaradan Sampath

We propose a framework for developing hybrid systems that are comprised of a plant with multiple controllers, each of which controls the plant intermittently. The framework is based on the notion of a "conflict-tolerant" specification for a controller, and provides a mod- ular way of developing and reasoning about such systems. We first motivate the need for conflict-tolerant specifications by illustrating conflict between two controllers in a real world system. We then pro- pose a way of defining conflict-tolerant specifications for general hy- brid systems. We also give a decision procedure for verifying whether a controller satisfies its conflict-tolerant specification, in the special case when the components are modeled using initialized rectangular hybrid automata. With tolerant specifications and verified controllers, it is easy to construct a simple priority based supervisory controller for re- solving conflict among controllers. We also show that in the restricted setting of switched control, it is possible to construct a supervisory controller which guarantees the "maximal" use of every controller by ensuring that the advice of each controller is always followed except at time instants when each of the controller's advice conflicts with that of a higher priority controller.

pdf