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