Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data

Area of Science:

• Computational Biology
• Systems Biology
• Formal Methods

Background:

• Stochastic population models are crucial across diverse fields like cyber-physical systems and collective animal behavior.
• Quantitative analysis is hindered by the vast number of population states and difficulty in measuring transition parameters.
• Parameter inference is challenging with limited population-level data, especially regarding terminal state distributions.

Purpose of the Study:

• Investigate the application of formal verification methods for parameter inference in population discrete-time Markov chains.
• Address parameter identifiability and uncertainty quantification with limited sample data.
• Develop and evaluate novel methods for enhanced parameter inference.

Main Methods:

• Discuss parameter identifiability and uncertainty quantification in the context of limited data.
• Apply existing techniques of formal parameter synthesis and Bayesian inference.
• Propose and implement four new inference methods, three utilizing formal parameter synthesis as a pre-computation step.

Main Results:

• Proposed methods incorporating formal parameter synthesis significantly improve inference accuracy, precision, and scalability.
• Successfully captured the subspace of data-compliant parameters at a desired confidence level, even for unidentifiable parameters.
• Empirical evaluation across four case studies validated the performance enhancements.

Conclusions:

• Formal verification methods offer a powerful approach to parameter inference for stochastic population models.
• The integration of formal parameter synthesis as a pre-computation step is key to achieving enhanced inference capabilities.
• These methods provide robust solutions for scenarios with limited data and parameter identifiability challenges.