Distributed LTL Model-Checking Based on Negative Cycle Detection

BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL and Radek PELÁNEK. Distributed LTL Model-Checking Based on Negative Cycle Detection. In FST-TCS 2001. Bangalore, India: Springer, 2001, p. 96-110. LNCS 2245. ISBN 3-540-43002-4.

Basic information

• Original name: Distributed LTL Model-Checking Based on Negative Cycle Detection
• Name (in English): Distributed LTL Model-Checking Based on Negative Cycle Detection
• Authors: BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL and Radek PELÁNEK.
• Edition: Bangalore, India, FST-TCS 2001, p. 96-110, LNCS 2245, 2001.
• Publisher: Springer

Other information

• Type of outcome: Proceedings paper
• Field of Study: 20206 Computer hardware and architecture
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/01:00004500
• Organization unit: Faculty of Informatics
• ISBN: 3-540-43002-4

Abstract

This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are based on depth first traversal of the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking.

Abstract (in English)

This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are based on depth first traversal of the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking.

Links

• GA201/00/0400, research and development project: Name: Nekonečně stavové souběžné systémy - modely a verifikace

Investor: Czech Science Foundation, Infinite state concurrent systems - models and verification

• GA201/00/1023, research and development project: Name: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů

Investor: Czech Science Foundation, Algorithms and tools for practical verification of concurrent systems.

• MSM 143300001, plan (intention): Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů

Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing