Quantitative Model Checking of Systems with Degradation

BARNAT, Jiří, Ivana ČERNÁ a Jana TŮMOVÁ. Quantitative Model Checking of Systems with Degradation. In 2009 Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos (California): IEEE Computer Society, 2009, s. 21-30. ISBN 978-0-7695-3808-2.

Základní údaje

Originální název

Quantitative Model Checking of Systems with Degradation

Název česky

Kvantitativní ověřování modelu systémů s degradací

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Jana TŮMOVÁ (203 Česká republika, domácí)

Vydání

Los Alamitos (California), 2009 Sixth International Conference on the Quantitative Evaluation of Systems, od s. 21-30, 10 s. 2009

Nakladatel

IEEE Computer Society

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Maďarsko

Utajení

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

Forma vydání

paměťový nosič (CD, DVD, flash disk)

Odkazy

URL URL

Kód RIV

RIV/00216224:14330/09:00029636

Organizační jednotka

Fakulta informatiky

ISBN

978-0-7695-3808-2

UT WoS

000275039200002

Klíčová slova česky

Systémy s degradací; LTL; ověřování modelu

Klíčová slova anglicky

Systems with degradation; LTL model checking

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

In this paper we describe a rather specialized quality of a system -- the degradation. We demonstrate systems that naturally incorporate degradation phenomenon and we show how these systems can be verified by adapting the standard automata-based approach to LTL model checking. We introduce B\"uchi Automata with Degradation Constraints (BADCs) to specify the desired properties of systems with degradation and we describe how these can be used for verification. A major obstacle in the verification process is that the synchronous product of the system and the B\"uchi automaton may be infinite, which we deal with by introducing a normal form of the B\"uchi automata and normalizing procedure. We also show that the newly introduced formalism can be used to distinguish MDPs indistinguishable by any LTL, PCTL or even PCTL* formula.

Česky

V tomto článku je popsána speciální vlastnost systémů - degradace, a je rozpracován metoda verifikace tohoto aspektu, která staví na technice ověřování modelu. Dále je v článku definován nový formalismus pro zachycení vlastností systémů s degradací, a je demonstrováno, že tento formalismus je schopen vyjádřit vlastnosti pravděpodobnostních systémů, které nejsou vyjádřitelné ve stadnardních logikách jako jsou PLTL, nebo PCTL*.

---

Návaznosti

GA201/09/1389, projekt VaV	Název: Verifikace a analýza velmi velkých počítačových systémů Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
GP201/09/P497, projekt VaV	Název: Automatizovaná formální verifikace s využitím soudobého hardware Investor: Grantová agentura ČR, Automatizovaná formální verifikace s využitím soudobého hardware
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky