Timed Automata Approach to Verification of Systems with Degradation

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057212" target="_blank" >RIV/00216224:14330/12:00057212 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-25929-6_8" target="_blank" >http://dx.doi.org/10.1007/978-3-642-25929-6_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-25929-6_8" target="_blank" >10.1007/978-3-642-25929-6_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Timed Automata Approach to Verification of Systems with Degradation

Popis výsledku v původní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.

Název v anglickém jazyce

Timed Automata Approach to Verification of Systems with Degradation

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2012

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

MEMICS 2011

ISBN

9783642259289

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

10

Strana od-do

84-93

Název nakladatele

Springer

Místo vydání

Heidelberg

Místo konání akce

Lednice

Datum konání akce

1. 1. 2011

Typ akce podle státní příslušnosti

CST - Celostátní akce

Kód UT WoS článku

—