How to distribute LTL model-checking using decomposition of negative claim automaton

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	BARNAT Jiří
Rok publikování	2002
Druh	Článek ve sborníku
Konference	SOFSEM 2002 Student Research Forum Proceedings
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	Distribute LTL model-checking; Negative Claim Automaton
Popis	We propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm.
Související projekty:	Algoritmy a nástroje pro praktickou verifikaci souběžných systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů