D 2004

Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC and Jiří ŠIMŠA

Basic information

Original name

Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.

Name in Czech

Akceptující předchůdci v distrubuovaném LTL ověřování modelů

Authors

BRIM, Luboš (203 Czech Republic, guarantor), Ivana ČERNÁ (203 Czech Republic), Pavel MORAVEC (203 Czech Republic) and Jiří ŠIMŠA (203 Czech Republic)

Edition

Neuveden, Formal Methods in Computer-Aided Design (FMCAD), p. 352-366, 24 pp. 2004

Publisher

Springer-Verlag, LNCS 3312

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/04:00010529

Organization unit

Faculty of Informatics

ISBN

3-540-23738-0

UT WoS

000226785300025

Keywords in English

distributed - memory LTL model checking; graph predecessors

Tags

Tags

International impact, Reviewed
Změněno: 8/6/2009 16:08, prof. RNDr. Ivana Černá, CSc.

Abstract

ORIG CZ

V originále

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. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.

In Czech

Článek prezentuje nový distribuovaný algoritmus pro ověřování LTL vlastností založený na akceptujících předchůdcích. Je prezentováné několik optimalizací a experimentální výsledky

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