Using verified property to partition the state space in LTL model-checking

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 F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model-checking; distributed model-checking; verification
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.