David Šafránek

Petr Dluhoš, Luboš Brim, David Šafránek

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.

Ondřej Huvar, Nikola Beneš, Martin Jonáš et al.

Qualitative models provide crucial instruments for modelling complex biological systems. While advances in automated reasoning and symbolic encodings have enabled rigorous inference of these models from data, the process remains highly fragile. First, biological measurement errors inevitably propagate into formal model specifications. Second, when a specification becomes unsatisfiable, distinguishing between fundamental design flaws and minor technical errors is notoriously difficult. This uncertainty often leads to under-specification, as it is unclear which observations are still ``safe'' to incorporate. To overcome these challenges, we introduce a robust inference method based on weighted MaxSMT. By encoding uncertain biological observations as weighted soft constraints, our approach enables the solver to identify a model best reflecting the observations, even with some conflicting constraints. Our method allows for Boolean and multi-valued variable domains, alongside observations derived from discretisation (level constraints) and differential expression (ordering constraints). We show our approach can be used to successfully infer neural cell differentiation models from prior-knowledge networks with 200--1300 genes using ordering constraints on all included genes.

Matej Troják, David Šafránek, Luboš Brim

This technical report relates Biochemical Space Language (BCSL) to Multiset rewriting systems (MRS). For a BCSL model, the semantics are defined in terms of transition systems, while for an MRS, they are defined in terms of a set of runs. In this report, we relate BCSL to MRS by first showing how the transition system is related to a set of runs and consequently showing how for every BCSL model, an MRS can be constructed such that both represent the same set of runs. The motivation of this step is to establish BCSL in the context of a more general rewriting system and benefit from properties shown for them. Finally, we show that regulations defined for MRS can be consequently used in the BCSL model.