Timed Automata Approach to Verification of Systems with Degradation

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BARNAT Jiří ČERNÁ Ivana TŮMOVÁ Jana

Rok publikování 2012
Druh Článek ve sborníku
Konference MEMICS 2011
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-25929-6_8
Obor Informatika
Klíčová slova model checking; linear temporal properties with degradation
Přiložené soubory
Popis We focus on systems that naturally incorporate a degrad- ing quality, such as electronic devices with degrading electric charge or broadcasting networks with decreasing power or quality of a transmitted signal. For such systems, we introduce an extension of linear temporal logic with quantitative constraints (Linear Temporal Logic with Degra- dation Constraints) that provides a user-friendly for- malism for specifying properties involving quantitative requirements on the level of degradation. The syntax of DLTL resembles syntax of Metric Interval Temporal Logic (MITL) designed for reasoning about timed systems. Thus, we investigate their relation and a possibility of translating DLTL verication problem for systems with degradation into previously solved MITL verication problem for timed automata. We show, that through the mentioned translation, the DLTL model checking problem can be solved with limited, yet arbitrary, precision.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.