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; 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
• 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ů