Using Accepting Predecessors in Distributed LTL Model-Checking

MORAVEC, Pavel. Using Accepting Predecessors in Distributed LTL Model-Checking. In MOVEP'04: 6th school on MOdeling and VErifying parallel Processes. Bruxelles, Belgium: Universite Libre de Bruxelles, 2004, p. 122-129, 7 pp.

Basic information

• Original name: Using Accepting Predecessors in Distributed LTL Model-Checking
• Name in Czech: Použití akceptujících předchůdců u distribuovaného ověřování LTL vlastností modelu
• Authors: MORAVEC, Pavel (203 Czech Republic, guarantor).
• Edition: Bruxelles, Belgium, MOVEP'04: 6th school on MOdeling and VErifying parallel Processes, p. 122-129, 7 pp. 2004.
• Publisher: Universite Libre de Bruxelles

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Belgium
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/04:00011071
• Organization unit: Faculty of Informatics
• Keywords in English: LTL model checking; distributed algorithm
• Tags: distributed algorithm, LTL model checking

Abstract

We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. The influence of the ordering on the algorithm performance is open as future work.

Abstract (in Czech)

Prezentujeme nový algoritmus s distribuovanou pamětí pro ověřování LTL vlastností modelu, který je navržen pro síť počítačů komunikujících pomocí MPI. Detekce akceptujících cyklů je založena na počítání největších akceptujících předchůdců a na následném rozkladu grafu na nezávislé předchůdcovské podgrafy indukované největšími akceptujícími předchůdci. Vliv uspořádání vrcholů na chování algoritmu je otevřena jako budoucí práce.

Links

• GA201/03/0509, research and development project: Name: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed 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