Data-informed 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 [doi, pdf]
Przemyslaw Daca, Thomas A. Henzinger, Jan Kretinsky, Tatjana Petrov: Linear Distances between Markov Chains, In 27th International Conference on Concurrency Theory (CONCUR 2016) [doi, pdf slides]
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 [doi, pdf slides]
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]
Matej Hajnal, Morgane Nouvian, David Šafránek, Tatjana Petrov. Data-informed parameter synthesis for population markov chains. In International Workshop on Hybrid Systems Biology (HSB 2019) [doi pdf poster]