Assume-Guarantee Reasoning for Additive Hybrid Behaviour

Pieter J.L. Cuijpers, Jonas Hansen, Kim G. Larsen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademicpeer review


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.

Originele taal-2Engels
TitelTheories of Programming and Formal Methods
SubtitelEssays Dedicated to Jifeng He on the Occasion of His 80th Birthday
RedacteurenJonathan P. Bowen, Qin Li, Qiwen Xu
Aantal pagina's26
ISBN van elektronische versie978-3-031-40436-8
ISBN van geprinte versie978-3-031-40435-1
StatusGepubliceerd - 2023

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14080 LNCS
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349

Bibliografische nota

Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.


Duik in de onderzoeksthema's van 'Assume-Guarantee Reasoning for Additive Hybrid Behaviour'. Samen vormen ze een unieke vingerafdruk.

Citeer dit