Assume-Guarantee Reasoning for Additive Hybrid Behaviour

Hybrid Automata describe dynamical systems where continuous behaviour interacts with discrete events. Resource Timed Automata (RTA), a subset of Hybrid Automata, adopt an additive composition scheme, in which discrete behaviour of components is executed concurrently, time is synchronized, and the evolution of continuous variables is arithmetically added up. Additive composition facilitates modelling and analysis of cumulative properties of continuous variables, such as conservation laws, typically manifested as the balancing of real-valued variables. In this paper, we present and exemplify an assume-guarantee framework aimed at additive compositional reasoning in the setting of hybrid systems. Crucially, we introduce a notion of refinement on so-called Resource Hybrid Automata (RHA), and show that it is a pre-congruence for additive composition. Furthermore - crucial for our assume-guarantee framework – we show that RHAs are closed under conjunction and admit a so-called quotient constructions (a dual operator to parallel composition). Finally, we demonstrate how the Statistical Model Checking (SMC) engine of the tool UPPAAL may be used to efficiently falsify refinements.