BARNAT, Jiří, Ivana ČERNÁ and 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, p. 21-30. ISBN 978-0-7695-3808-2.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Quantitative Model Checking of Systems with Degradation
Name in Czech Kvantitativní ověřování modelu systémů s degradací
Authors BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution) and Jana TŮMOVÁ (203 Czech Republic, belonging to the institution).
Edition Los Alamitos (California), 2009 Sixth International Conference on the Quantitative Evaluation of Systems, p. 21-30, 10 pp. 2009.
Publisher IEEE Computer Society
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Hungary
Confidentiality degree is not subject to a state or trade secret
Publication form storage medium (CD, DVD, flash disk)
WWW URL URL
RIV identification code RIV/00216224:14330/09:00029636
Organization unit Faculty of Informatics
ISBN 978-0-7695-3808-2
UT WoS 000275039200002
Keywords (in Czech) Systémy s degradací; LTL; ověřování modelu
Keywords in English Systems with degradation; LTL model checking
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 13/10/2020 09:38.
Abstract
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.
Abstract (in Czech)
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*.
Links
GA201/09/1389, research and development projectName: Verifikace a analýza velmi velkých počítačových systémů
Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
GP201/09/P497, research and development projectName: Automatizovaná formální verifikace s využitím soudobého hardware
Investor: Czech Science Foundation, Automated formal verification using modern hardware
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science
PrintDisplayed: 19/9/2024 06:36