Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Logo poskytovatele

Varování

Publikace nespadá pod Fakultu sportovních studií, 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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info