Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN a Patricia BOUYER. Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. In Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004). Barcelona (Španělsko): Springer-Verlag, 2004, s. 312-326. ISBN 3-540-21299-X.

Základní údaje

Originální název

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Název česky

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

Autoři

PELÁNEK, Radek (203 Česká republika, garant), Kim G. LARSEN (208 Dánsko), Gerd BEHRMANN (208 Dánsko) a Patricia BOUYER (250 Francie)

Vydání

Barcelona (Španělsko), Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004), od s. 312-326, 15 s. 2004

Nakladatel

Springer-Verlag

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Španělsko

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/04:00010716

Organizační jednotka

Fakulta informatiky

ISBN

3-540-21299-X

UT WoS

000189496900025

Klíčová slova anglicky

model checking; timed automata; abstraction

Štítky

Abstraction, Model checking, timed automata

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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 used to 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.

Česky

Č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.

---

Návaznosti

GA201/03/0509, projekt VaV	Název: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 143300001, záměr	Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů