D 2004

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN and Patricia BOUYER

Basic information

Original name

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Name in Czech

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

Authors

PELÁNEK, Radek (203 Czech Republic, guarantor), Kim G. LARSEN (208 Denmark), Gerd BEHRMANN (208 Denmark) and Patricia BOUYER (250 France)

Edition

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

Publisher

Springer-Verlag

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Spain

Confidentiality degree

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

RIV identification code

RIV/00216224:14330/04:00010716

Organization unit

Faculty of Informatics

ISBN

3-540-21299-X

UT WoS

000189496900025

Keywords in English

model checking; timed automata; abstraction

Tags

Tags

International impact, Reviewed
Změněno: 21/11/2006 14:02, doc. Mgr. Radek Pelánek, Ph.D.

Abstract

ORIG CZ

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.

In Czech

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

Links

GA201/03/0509, research and development project
Name: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
MSM 143300001, plan (intention)
Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing