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

• 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
• 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

• Algorithms and tools for practical verification of concurrent systems.
• Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing