Language Based Abstraction Refinement for Hybrid System Verification

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F07%3A00339925" target="_blank" >RIV/67985807:_____/07:00339925 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Language Based Abstraction Refinement for Hybrid System Verification

Popis výsledku v původním jazyce

The standard counterexample-guided abstraction-refinement (CEGAR) approach uses finite transition systems as abstractions of concrete systems. We present an approach to represent and refine abstractions of infinite-state systems. Instead of using finitetransition systems we use regular languages. The advantage of languages over transition systems is that we can store more fine-grained information in the abstraction and thus reduce the number of abstract states. Based on this language-based approach forCEGAR, we present new abstraction-refinement algorithms for hybrid system verification. Moreover, we evaluate our approach by verifying various non-linear hybrid systems.

Název v anglickém jazyce

Language Based Abstraction Refinement for Hybrid System Verification

Popis výsledku anglicky

The standard counterexample-guided abstraction-refinement (CEGAR) approach uses finite transition systems as abstractions of concrete systems. We present an approach to represent and refine abstractions of infinite-state systems. Instead of using finitetransition systems we use regular languages. The advantage of languages over transition systems is that we can store more fine-grained information in the abstraction and thus reduce the number of abstract states. Based on this language-based approach forCEGAR, we present new abstraction-refinement algorithms for hybrid system verification. Moreover, we evaluate our approach by verifying various non-linear hybrid systems.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2007

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Verification, Model Checking, and Abstract Interpretation

ISBN

978-3-540-69735-0

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

—

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Nice

Datum konání akce

14. 1. 2007

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000244555600011