On Expressing and Monitoring Oscillatory Dynamics

DLUHOŠ, Petr, Luboš BRIM and David ŠAFRÁNEK. On Expressing and Monitoring Oscillatory Dynamics. Online. Electronic Proceedings in Theoretical Computer Science. Newcastle Upon Tyne: EPTCS, 2012, vol. 2012, No 92, p. 73-87. ISSN 2075-2180. Available from: https://dx.doi.org/10.4204/EPTCS.92. [citováno 2024-04-24]

Basic information

• Original name: On Expressing and Monitoring Oscillatory Dynamics
• Authors: DLUHOŠ, Petr (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution)
• Edition: Electronic Proceedings in Theoretical Computer Science, Newcastle Upon Tyne, EPTCS, 2012, 2075-2180.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/12:00057626
• Organization unit: Faculty of Informatics
• Doi: http://dx.doi.org/10.4204/EPTCS.92
• Keywords in English: dynamical systems; oscillation; monitoring; Signal Temporal Logic
• Tags: International impact, Reviewed

Abstract

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.

Links

• CZ.1.07/2.3.00/20.0256, interní kód MU(CEP code: EE2.3.20.0256): Name: Vytvoření výzkumného týmu a mezinárodního konzorcia pro počítačový model buňky sinice (Acronym: CyanoTeam)

Investor: Ministry of Education, Youth and Sports of the CR, 2.3 Human resources in research and development

• GAP202/11/0312, research and development project: Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)

Investor: Czech Science Foundation

• GP201/09/P497, research and development project: Name: Automatizovaná formální verifikace s využitím soudobého hardware

Investor: Czech Science Foundation, Automated formal verification using modern hardware

• MUNI/A/0914/2009, interní kód MU: Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)

Investor: Masaryk University, Category A