J 2012

On Expressing and Monitoring Oscillatory Dynamics

DLUHOŠ, Petr, Luboš BRIM a David ŠAFRÁNEK

Základní údaje

Originální název

On Expressing and Monitoring Oscillatory Dynamics

Autoři

DLUHOŠ, Petr (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí) a David ŠAFRÁNEK (203 Česká republika, garant, domácí)

Vydání

Electronic Proceedings in Theoretical Computer Science, Newcastle Upon Tyne, EPTCS, 2012, 2075-2180

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Kód RIV

RIV/00216224:14330/12:00057626

Organizační jednotka

Fakulta informatiky

DOI

Klíčová slova anglicky

dynamical systems; oscillation; monitoring; Signal Temporal Logic

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 11. 4. 2013 17:36, doc. RNDr. David Šafránek, Ph.D.

Anotace

V originále

To express temporal properties of dense-time real-valued signals, the Signal Temporal Logic (STL) has been defined by Maler et al. The work presented a monitoring algorithm deciding the satisfiability of STL formulae on finite discrete samples of continuous signals. The logic has been used to express and analyse biological systems, but it is not expressive enough to sufficiently distinguish oscillatory properties important in biology. In this paper we define the extended logic STL* in which STL is augmented with a signal-value freezing operator allowing us to express (and distinguish) detailed properties of biological oscillations. The logic is supported by a monitoring algorithm prototyped in Matlab. The monitoring procedure of STL* is evaluated on a biologically-relevant case study.

Návaznosti

CZ.1.07/2.3.00/20.0256, interní kód MU
(Kód CEP: EE2.3.20.0256)
Název: Vytvoření výzkumného týmu a mezinárodního konzorcia pro počítačový model buňky sinice (Akronym: CyanoTeam)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vytvoření výzkumného týmu a mezinárodního konzorcia pro počítačový model buňky sinice, 2.3 Lidské zdroje ve výzkumu a vývoji
GAP202/11/0312, projekt VaV
Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
GP201/09/P497, projekt VaV
Název: Automatizovaná formální verifikace s využitím soudobého hardware
Investor: Grantová agentura ČR, Automatizovaná formální verifikace s využitím soudobého hardware
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty