Hierarchic Superposition with Weak Abstraction

Baumgartner, Peter; Waldmann, Uwe

doi:10.1007/978-3-642-38574-2_3

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

会議論文

Hierarchic Superposition with Weak Abstraction

MPS-Authors

/persons/resource/persons45689

Waldmann, Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

公開されているフルテキストはありません

付随資料 (公開)

There is no public supplementary material available

引用

Baumgartner, P., & Waldmann, U. (2013). Hierarchic Superposition with Weak Abstraction. In M. P., Bonacina (Ed.), Automated Deduction - CADE-24 (pp. 39-57). Berlin: Springer. doi:10.1007/978-3-642-38574-2_3.

引用: https://hdl.handle.net/11858/00-001M-0000-0024-6C42-F

要旨

In this paper we study possibilities of using methods for hierarchical reasoning in local theory extensions for the analysis and verification of parametric hybrid systems, where the parameters can be either constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We first analyze the possibility of automatically generating such guarantees in the form of constraints on parameters, then show that we can also synthesise so-called criticality functions, typically used for proving stability and/or safety of hybrid systems. We illustrate our methods on several examples.