Informační systém MU
BARNAT, Jiří, Ivana ČERNÁ a Jana TŮMOVÁ. Quantitative Model Checking of Systems with Degradation. Online. 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. [citováno 2024-04-24]
Další formáty:   BibTeX LaTeX RIS
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
Originální 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)
WWW 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
Změnil Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 13. 10. 2020 09:38.
Anotace
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.
Anotace č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 VaVNá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 VaVNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
Zobrazeno: 24. 4. 2024 08:05