How to distribute LTL model-checking using decomposition of negative claim automaton

BARNAT, Jiří. How to distribute LTL model-checking using decomposition of negative claim automaton. In SOFSEM 2002 Student Research Forum Proceedings. Milovy,Czech Republic: Slovak University of Technology, 2002, s. 9-14.

Základní údaje

Originální název

How to distribute LTL model-checking using decomposition of negative claim automaton

Autoři

BARNAT, Jiří

Vydání

Milovy,Czech Republic, SOFSEM 2002 Student Research Forum Proceedings, s. 9-14, 2002

Nakladatel

Slovak University of Technology

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/02:00007074

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

Distribute LTL model-checking; Negative Claim Automaton

Štítky

Distribute LTL model-checking, Negative Claim Automaton

---

Anotace

V originále

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.

---

Návaznosti

GA201/00/1023, projekt VaV	Název: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
MSM 143300001, záměr	Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů