A Causal Analysis Method for Concurrent Hybrid Automata

Abstract

Modern artifacts are typically composed of many sys-tem components and exhibit a complex pattern of con-tinuous/discrete behaviors. A concurrent hybrid au-tomaton is a powerful modeling concept to capture such a system’s behavior in terms a concurrent composition of hybrid automata for the individual system compo-nents. Because of the potentially large number of modes of the concurrent automaton model it is non-trivial to validate the composition such that every possible oper-ational mode leads to a causally valid dynamic model for the overall system. This paper presents a novel model analysis method that validates the automata com-position without the necessity to analyze a prohibitively large number of modes. We achieve this by formulating the exhaustive causal analysis of hybrid automata as a diagnosis problem. This provides causal specifications of the component automata and enables us to efficiently calculate the causal relationships for their concurrent composition and thus validate a concurrent automaton model.