Learning and Designing Stochastic Processes from Logical Constraints

  • Luca Bortolussi
  • Guido Sanguinetti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)


Continuous time Markov Chains (CTMCs) are a convenient mathematical model for a broad range of natural and computer systems. As a result, they have received considerable attention in the theoretical computer science community, with many important techniques such as model checking being now mainstream. However, most methodologies start with an assumption of complete specification of the CTMC, in terms of both initial conditions and parameters. While this may be plausible in some cases (e.g. small scale engineered systems) it is certainly not valid nor desirable in many cases (e.g. biological systems), and it does not lead to a constructive approach to rational design of systems based on specific requirements. Here we consider the problems of learning and designing CTMCs from observations/ requirements formulated in terms of satisfaction of temporal logic formulae. We recast the problem in terms of learning and maximising an unknown function (the likelihood of the parameters) which can be numerically estimated at any value of the parameter space (at a non-negligible computational cost). We adapt a recently proposed, provably convergent global optimisation algorithm developed in the machine learning community, and demonstrate its efficacy on a number of non-trivial test cases.


Model Check Logical Constraint Continuous Time Markov Chain Infected Node Statistical Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Andersson, H., Britton, T.: Stochastic Epidemic Models and Their Statistical Analysis. Springer (2000)Google Scholar
  3. 3.
    Andreychenko, A., Mikeev, L., Spieler, D., Wolf, V.: Approximate maximum likelihood estimation for stochastic chemical kinetics. EURASIP Journal on Bioinf. and Sys. Bio. 9 (2012)Google Scholar
  4. 4.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model checking continuous-time Markov chains by transient analysis. IEEE TSE 29(6), 524–541 (2003)Google Scholar
  5. 5.
    Barnes, C.P., Silk, D., Sheng, X., Stumpf, M.P.: Bayesian design of synthetic biological systems. PNAS USA 108(37), 15190–15195 (2011)CrossRefGoogle Scholar
  6. 6.
    Bishop, C.M.: Pattern Recognition and Machine Learning. Springer (2006)Google Scholar
  7. 7.
    Bradley, J.T., Gilmore, S.T., Hillston, J.: Analysing distributed internet worm attacks using continuous state-space approximation of process algebra models. J. Comput. Syst. Sci. 74(6), 1013–1032 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Chen, T., Diciolla, M., Kwiatkowska, M.Z., Mereacre, A.: Time-bounded verification of CTMCs against real-time specifications. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 26–42. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Cover, T., Thomas, J.: Elements of Information Theory, 2nd edn. Wiley (2006)Google Scholar
  10. 10.
    Durrett, R.: Essentials of stochastic processes. Springer (2012)Google Scholar
  11. 11.
    Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. of Physical Chemistry 81(25) (1977)Google Scholar
  12. 12.
    Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. 13.
    Jha, S.K., Langmead, C.J.: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement. Theor. Comp. Sc. 412(21), 2162–2187 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Kennedy, M., O’Hagan, A.: Bayesian calibration of computer models. Journal of the Royal Stat. Soc. Ser. B 63(3), 425–464 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  15. 15.
    Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. Int. Jour. on Softw. Tools for Tech. Transf. 6(2), 128–142 (2004)Google Scholar
  16. 16.
    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Opper, M., Sanguinetti, G.: Variational inference for Markov jump processes. In: Proc. of NIPS (2007)Google Scholar
  18. 18.
    Rasmussen, C.E., Williams, C.K.I.: Gaussian Processes for Machine Learning. MIT Press (2006)Google Scholar
  19. 19.
    Romero, P.A., Krause, A., Arnold, F.H.: Navigating the protein fitness landscape with Gaussian processes. PNAS USA 110(3), E193–E201 (2013)CrossRefGoogle Scholar
  20. 20.
    Srinivas, N., Krause, A., Kakade, S., Seeger, M.: Information-theoretic regret bounds for Gaussian process optimisation in the bandit setting. IEEE Trans. Inf. Th. 58(5), 3250–3265 (2012)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Vezhnevets, A., Ferrari, V., Buhmann, J.: Weakly supervised structured output learning for semantic segmentation. In: Comp. Vision and Pattern Recog. (2012)Google Scholar
  22. 22.
    Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368–1409 (2006)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Luca Bortolussi
    • 1
    • 2
  • Guido Sanguinetti
    • 3
    • 4
  1. 1.Department of Mathematics and GeosciencesUniversity of TriesteItaly
  2. 2.CNR/ISTIPisaItaly
  3. 3.School of InformaticsUniversity of EdinburghUK
  4. 4.SynthSys, Centre for Synthetic and Systems BiologyUniversity of EdinburghUK

Personalised recommendations