D 2005

How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors

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

Základní údaje

Originální název

How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors

Název česky

Uspořádání vrcholů pro distribuované ověřování LTL vlastností modelu založené na akceptujících předchůdcích

Autoři

BRIM, Luboš (203 Česká republika, garant), Ivana ČERNÁ (203 Česká republika), Pavel MORAVEC (203 Česká republika) a Jiří ŠIMŠA (203 Česká republika)

Vydání

Lisboa, Portugal, Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005), s. 1-12, 2005

Nakladatel

TU Munchen

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Portugalsko

Utajení

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

Kód RIV

RIV/00216224:14330/05:00012461

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

accepting predecessors; LTL model checking

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 08:32, prof. RNDr. Luboš Brim, CSc.

Anotace

ORIG CZ

V originále

The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B\"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well.

Česky

Článek zkoumá problém optimálního uspořádání dříve prezentovaného algoritmu pro distribuované ověřování LTL vlastností modelu a prezentuje několik heuristik pro nalezení optimálního uspořádání v distribuovaném prostředí.

Návaznosti

GA201/03/0509, projekt VaV
Název: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
GD102/05/H050, projekt VaV
Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV
Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky