Parametric Systems: Verification and Synthesis

TL;DR

This paper explores hierarchical reasoning, symbol elimination, and model generation techniques to verify parametric systems, aiming to automatically generate parameter constraints that ensure safety and invariance.

Contribution

It introduces methods for automatic verification and synthesis of guarantees in parametric systems using hierarchical reasoning and model generation.

Findings

Effective methods for parameter constraint generation

Application to safety verification of parametric systems

Illustrative examples demonstrating the approach

Abstract

In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We analyze the possibility of automatically generating such guarantees in the form of constraints on parameters. We illustrate our methods on several examples