On verification and constraint generation for families of similar hybrid automata

TL;DR

This paper reviews methods for analyzing parametric and similar hybrid automata, focusing on verifying safety properties using hierarchical reasoning and symbol elimination, with practical implementation and examples.

Contribution

It introduces approaches for describing and verifying systems with parametric and similar components, emphasizing hierarchical reasoning and parameter relationships.

Findings

Methods can determine parameter conditions ensuring safety

Implementation demonstrates practical applicability

Analysis supports systems with underspecified components

Abstract

In this paper we give an overview of results on the analysis of parametric linear hybrid automata, and of systems of similar linear hybrid automata: We present possibilities of describing systems with a parametric (i.e. not explicitly specified) number of similar components which can be connected to other systems, such that some parts in the description might be underspecified (i.e. parametric). We consider global safety properties for such systems, expressed by universally quantified formulae, using quantification over variables ranging over the component systems. We analyze possibilities of using methods for hierarchical reasoning and symbol elimination for determining relationships on (some of) the parameters used in the description of these systems under which the global safety properties are guaranteed to be inductive invariants. We discuss an implementation and illustrate its use on several examples.