Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

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 LARSEN Kim G. BEHRMANN Gerd BOUYER Patricia
Rok publikování	2004
Druh	Článek ve sborníku
Konference	Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	model checking; timed automata; abstraction
Popis	Č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.
Související projekty:	Automatizovaná verifikace paralelních a distribuovaných systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů