Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On verification and constraint generation for families of similar hybrid automata

Viorica Sofronie-Stokkermans, Philipp Marohn

TL;DR

The paper addresses verification and constraint generation for families of parametric linear hybrid automata (PLHA) and systems of similar hybrid automata, focusing on deriving parameter constraints that guarantee safety properties expressed as $\forall$-quantified formulas. It advances a hierarchical reasoning approach based on local theory extensions and a symbol-elimination method, implemented in SEH-PILoT (with H-PILoT as backend), and demonstrates its applicability through water-tank and autonomous-car examples, including dynamic topology updates. Key contributions include formalizing PLHA and spatial families (SFHA/SFLHA), establishing complexity results (PTIME for non-parametric LHA and exponential for PLHA), and providing practical constraint-generation workflows that scale to families of components via chain-like local extensions. Limitations are acknowledged for topology-update constraints involving pointers, due to the need for quantifier-alternation reasoning in pointer theories; future work aims at invariant strengthening and deeper connections to small-model properties for systems-of-systems, with potential impact on cyber-physical systems verification and automated driving systems synthesis.

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.

On verification and constraint generation for families of similar hybrid automata

TL;DR

The paper addresses verification and constraint generation for families of parametric linear hybrid automata (PLHA) and systems of similar hybrid automata, focusing on deriving parameter constraints that guarantee safety properties expressed as -quantified formulas. It advances a hierarchical reasoning approach based on local theory extensions and a symbol-elimination method, implemented in SEH-PILoT (with H-PILoT as backend), and demonstrates its applicability through water-tank and autonomous-car examples, including dynamic topology updates. Key contributions include formalizing PLHA and spatial families (SFHA/SFLHA), establishing complexity results (PTIME for non-parametric LHA and exponential for PLHA), and providing practical constraint-generation workflows that scale to families of components via chain-like local extensions. Limitations are acknowledged for topology-update constraints involving pointers, due to the need for quantifier-alternation reasoning in pointer theories; future work aims at invariant strengthening and deeper connections to small-model properties for systems-of-systems, with potential impact on cyber-physical systems verification and automated driving systems synthesis.

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.
Paper Structure (14 sections, 5 theorems, 6 equations, 1 figure, 1 algorithm)

This paper contains 14 sections, 5 theorems, 6 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Idea
  3. Preliminaries
  4. Local theory extensions
  5. Examples of local theory extensions
  6. Symbol elimination in local theory extensions
  7. Tools
  8. Parametric Linear Hybrid Automata
  9. Verification
  10. Example: Verification and constraint generation
  11. Families of Similar Hybrid Automata
  12. Verification
  13. Examples: Constraint generation
  14. Conclusions

Key Result

Theorem 1

If ${\cal T}_0 \subseteq {\cal T}_0 \cup {\cal K}$ is a (stably) local extension and $G$ is a set of ground clauses then we can reduce the problem of checking whether $G$ is satisfiable w.r.t. ${\cal T}_0 \cup {\cal K}$ to checking the satisfiability w.r.t. ${\cal T}_0$ of the formula ${\cal K}_0 \c

Figures (1)

  • Figure 1: Hybrid automaton modeling the behavior of a car on a two-lane highway

Theorems & Definitions (18)

  • Example 1: Sofronie-Fundamenta-Informaticae-2020
  • Example 2
  • Example 3: DammHS15
  • Definition 1: Local theory extension
  • Theorem 1: Sofronie-cade-05
  • Theorem 2: sofronie-lmcs-2018PeuterSofronie2019
  • Example 4
  • Definition 2: Hybrid automaton Henzinger
  • Definition 3
  • Definition 4: Linear hybrid automaton Henzinger
  • ...and 8 more