Local Quantitative LTL Model Checking

• Název česky: Lokální kvantitativní ověřování modelu pro LTL
• Autoři: BARNAT Jiří; BRIM Luboš; ČERNÁ Ivana; ČEŠKA Milan; TŮMOVÁ Jana
• Rok publikování: 2009
• Druh: Článek ve sborníku
• Konference: Formal Methods for Industrial Critical Systems
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://dx.doi.org/10.1007/978-3-642-03240-0_8
• Doi: http://dx.doi.org/10.1007/978-3-642-03240-0_8
• Obor: Informatika
• Klíčová slova: Quantitative Model Checking; Linear Temporal Logic; Probabilistic systems
• Popis: Kvantitativní analýza pravděpodonostsních systémů byla studována především z pohledu metody globálního ověřování modelu (určení pravděpodobnosti pro každý stav systému). V článku ukazujeme jak lze výpočetní náročnost problému redukovat, pokud se zajímáme pouze o pravděpodobnost splnění formule v počátečním stavu (lokální ověřování modelu). V článku je popsáno několik technik, které redukují čas potřebný pro výpočet pravděpodobnosti z řádu dnů na řády minut.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Automatizovaná verifikace softwaru