| Identifikační kód | RIV/00216224:14330/12:00057864 |
|---|
| Název v anglickém jazyce | Verification of Systems with Degradation |
|---|
| Druh | J - Článek v odborném periodiku |
|---|
| 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 degrading 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 (Linear Temporal Logic with Degradation Constraints, or DLTL for short) that provides a user-friendly formalism for specifying properties involving quantitative requirements on the level of degradation. We investigate possibilityof translating DLTL verification problem for systems with degradation into previously solved MITL verification problem for timed automata, and we show that through the translation, DLTL model checking problem can be solved with limited, yet arbitrary, precision. For a specific subclass of DLTL formulas, we present a full precision verification technique based on translation of DLTL formulas into a specification formalism called Buchi Automata with Degradation Constraints (BADCs) develope |
|---|
| Klíčová slova oddělená středníkem | Systems with degradation; Linear Temporal Logic; Quantitative model checking; Automata-based approach to verification; Timed automata |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|