Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Využití horních a dolních mezí při zónových abstrakcích časových automatů
Autoři	PELÁNEK Radek LARSEN Kim G. BEHRMANN Gerd BOUYER Patricia
Rok publikování	2006
Druh	Článek v odborném periodiku
Časopis / Zdroj	International Journal on Software Tools for Technology Transfer (STTT)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	model checking; timed automata; verification; abstraction; extrapolation
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ů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy