An assume-guarantee reasoning for hierarchical coordination of discrete event systems

The construction of a consistent abstraction plays a central role in the hierarchical control of discrete event systems. When constructing a consistent abstraction of a composed system it is first necessary to build the entire system, whose state space grows exponentially with the number of system components. Therefore it is desirable to build this consistent abstraction directly from the composition of consistent abstractions of the subsystems. But the composition of consistent abstractions of the subsystems is not necessarily a consistent abstraction of the composed system. This paper presents a method based on an assume-guarantee reasoning to build a consistent abstraction of the composed system by the composition of modified consistent abstractions of the subsystems. The method is then applied for a case of an Cooperative Adaptive Cruise Controller (CACC) system for an automobile.