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

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