| Identifikační kód | RIV/00216224:14330/12:00057212 |
|---|
| Název v anglickém jazyce | Timed Automata Approach to Verification of Systems with Degradation |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2012 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792)
Ivana Černá (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2361132)
Jana Tůmová (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 4293738) |
|---|
| Popis výsledku v anglickém jazyce | 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 extensionof 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 syntaxof 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. |
|---|
| Klíčová slova oddělená středníkem | model checking; linear temporal properties with degradation |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-25929-6_8 |
|---|