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

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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