Randomization Helps in LTL Model Checking

BRIM, Luboš, Ivana ČERNÁ a Martin NEČESAL. Randomization Helps in LTL Model Checking. In Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001. Berlin Heidelberg New York: Springer, 2001, s. 105-119. LNCS 2165. ISBN 3-540-42556-X.

Základní údaje

Originální název

Randomization Helps in LTL Model Checking

Autoři

BRIM, Luboš, Ivana ČERNÁ a Martin NEČESAL

Vydání

Berlin Heidelberg New York, Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001, s. 105-119, LNCS 2165, 2001

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10000 1. Natural Sciences

Stát vydavatele

Německo

Utajení

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

Kód RIV

RIV/00216224:14330/01:00004526

Organizační jednotka

Fakulta informatiky

ISBN

3-540-42556-X

Klíčová slova anglicky

Model checking; randomized algorithm; depth-first search

Štítky

depth-first search, Model checking, randomized algorithm

---

Anotace

V originále

We present and analyze a new probabilistic method for automata based LTL model checking of non-proba\-bi\-listic systems with intention to reduce memory requirements. The main idea of our approach is to use randomness to decide which of the needed information (visited states) should be stored during a computation and which could be omitted. We propose two strategies of probabilistic storing of states. The algorithm never errs, i.e. it always delivers correct results. On the other hand the computation time can increase. The method has been embedded into the SPIN model checker and a series of experiments has been performed. The results confirm that randomization can help to increase the applicability of model checkers in practice.

---

Návaznosti

GA201/00/0400, projekt VaV	Název: Nekonečně stavové souběžné systémy - modely a verifikace Investor: Grantová agentura ČR, Nekonečně stavové souběžné systémy - modely a verifikace
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ů