Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F04%3A00010716" target="_blank" >RIV/00216224:14330/04:00010716 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Original language description

Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions wrt. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds we can obtain significantly coarser abstractions. We show the soundness and completeness of the new abstractstions wrt. reachability and we experimentaly demonstrate their advantages. We demonstrate how information about lower and upper boudns can be usedto optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker UPPAAL.

Czech name

Horní a dolní meze při analýze časových automatů s použitím zónové abstrakce

Czech description

Časové automaty mají nekonečnou sémantiku. Pro účely verifikace se většinou používá abstrakce založená na zónách braných vzhledem k maximálním konstantám objevujícím se v časovém automatu. Ukazujeme, že rozlišením maximálních spodních a horním mezí lze dosáhnou významně hrubších abstrakcí. Dále předvádíme, jak může být informace o maximálních horních a dolních mezích využita pro kanonizaci matice rozdílů. Také experimentálně prokazujeme, že tato nová technika výrazně vylepší výkon nástroje UPPAAL.

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

<a href="/en/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automated Verification of Parallel and Distributed Systems</a><br>

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2004

Confidentiality

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

Article name in the collection

Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004)

ISBN

3-540-21299-X

ISSN

—

e-ISSN

—

Number of pages

15

Pages from-to

312-326

Publisher name

Springer-Verlag

Place of publication

Barcelona (Španělsko)

Event location

Barcelona

Event date

Jan 1, 2004

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—