A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties

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	Časově optimální on-the-fly paralelní algoritmus pro ověřování modelu slabých LTL vlastností
Autoři	BARNAT Jiří BRIM Luboš ROČKAI Petr
Rok publikování	2009
Druh	Článek ve sborníku
Konference	Formal Methods and Software Engineering
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Doi	http://dx.doi.org/10.1007/978-3-642-10373-5_21
Obor	Informatika
Klíčová slova	on-the-fly; parallel; LTL Model Checking
Popis	Jeden z nejdůležitějších otevřených problému v paralelním ověřování modelu LTL je existence on-the-fly škálovatelného paralelního algoritmu s lineární časovou složitostí. V tomto článku dáváme částečnou odpověď na tento problém, jmenovitě řešíme tento problém pro poměrně bohatou podtřídu LTL vlastností, a to konkrétně slabých LTL vlastností.
Související projekty:	Techniky automatické verifikace a validace softwarových a hardwarových systémů Realistická aplikace formálních metod v komponentových systémech Vysoce paralelní a distribuované výpočetní systémy Verifikace a analýza velmi velkých počítačových systémů Automatizovaná formální verifikace s využitím soudobého hardware