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

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří

Year of publication 2002
Type Article in Proceedings
Conference SOFSEM 2002 Student Research Forum Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords Distribute LTL model-checking; Negative Claim Automaton
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.