Data-aware Multilayer Networks

Networks are routinely used for modelling and analysis of grouping and spreading phenomena such as epidemics, gene regulation, animal communication, all the way to the cyber-physical  systems  such  as  the  internet-of-things  or  a network of robots. Standard network approaches often overlook the different types of interactions and interdependencies. Multilayer Networks (MLNs) simultaneously incorporate multiple layers of relationships between group members, as well as inter-layer correlations, in a natural and compact way. However, more detailed description poses challenges for the respective computational analysis, inference, and learning, and novel techniques are needed for the context of MLNs.

Related works

Tatjana Petrov, Stefano Tognazzi: Centrality-Preserving Exact Reductions of Multi-Layer Networks
Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles (ISoLA 2020) [doi, pdf]

Tatjana Petrov, Stefano Tognazzi: Exact and Approximate Role Assignment for Multi-Layer Networks Journal of Complex Networks 2021 [doi, pdf]

Automated reductions for stochastic Chemical Reaction Networks

Chemical reaction networks (CRNs) are used for modelling population dynamics in a wide range of sciences including organic chemistry, epidemiology, systems/synthetic biology, ecology. CRN models give rise to a continuous-time Markov chain (CTMC) which is often computationally demanding and even prohibitive to analyse in practice. The challenge is especially prominent in systems and synthetic biology research, where one deals with a large number of species, stochasticity, and events happening at multiple time-scales. It is hence desirable to develop automated model reduction techniques that allow for efficient simulation yet faithfully abstract the context-relevant features emerging from the hypothesised mechanism.

Related works
Repin D, Petrov T (2021) Automated Deep Abstractions for Stochastic Chemical Reaction Networks. Information and Computation pdf

Repin Denis, Phung N Huy, Petrov Tatjana: StochNetV2: A Tool for Automated Deep Abstractions for Stochastic Reaction Networks, Quantitative Evaluation of Systems (QEST 2020) [doi, pdf]

Grey-box verification for Markov (population) models

Markov population models are an intuitive formalism representing how a group of agents (genes in systems biology, animals in collective behaviour, or robots in cyber-physical systems) evolves stochastically over time. However, in many modelling and verification scenarios, the parameters of the chain are not directly measurable, are subject to uncertainty, and the available experimental data measurements are limited. Such situations make it challenging to reason about the behaviours of the chain, where uncertainties may quickly propagate into significant errors through a cascading effect.

Related works

  • Przemyslaw Daca, Thomas A. Henzinger, Jan Kretinsky, Tatjana Petrov: Faster Statistical Model Checking for Unbounded Temporal Properties, ACM Transactions on Computational Logic, 2017 [doipdf]
  • Przemyslaw Daca, Thomas A. Henzinger, Jan Kretinsky, Tatjana Petrov: Linear Distances between Markov Chains, In 27th International Conference on Concurrency Theory (CONCUR 2016) [doipdf]
  • Przemyslaw Daca, Thomas A. Henzinger, Jan Kretinsky, Tatjana Petrov: Faster Statistical Model Checking for Unbounded Temporal Properties, In 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), nomination for best paper award [doipdf]
  • Matej Hajnal, Tatjana Petrov, David Safranek: DiPS: A Tool for Data-informed Parameter Synthesis for Discrete-Time Stochastic Processes from Multiple-Property Specifications 2021 [doi, pdf]

Old research description page

My research lies at the interface of theoretical computer science and mathematical modelling. My favourite models are probabilistic, and favourite application are biological systems. A common thread in my research is the combined use of formal methods (such as model-checking, SAT solvers, automated reasoning in general) and mathematical modelling (such as Markov chains, model reduction, statistical inference, machine learning), as well as the domain-specific modelling languages and theories (such as rule-based modelling, stochastic chemical kinetics). My recent interests include data-informed and learning methods, targeting explanatory models of collective behaviour.