Local Quantitative LTL Model Checking

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

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
Citace
www	http://dx.doi.org/10.1007/978-3-642-03240-0_8
Doi	https://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