Specification Theories for Probabilistic and Real-Time Systems

  • Uli Fahrenberg
  • Axel Legay
  • Louis-Marie Traonouez
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8415)


We survey extensions of modal transition systems to specification theories for probabilistic and timed systems.


Structural Composition Winning Strategy Atomic Proposition Interval Constraint Clock Constraint 
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.


  1. 1.
    Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601 (1993)Google Scholar
  2. 2.
    Bauer, S.S., Fahrenberg, U., Legay, A., Thrane, C.: General quantitative specification theories with modalities. In: Hirsch, E.A., Karhumäki, J., Lepistö, A., Prilutskii, M. (eds.) CSR 2012. LNCS, vol. 7353, pp. 18–30. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  3. 3.
    Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: Compositional design methodology with constraint Markov chains. In: QEST, pp. 123–132. IEEE Computer Society (2010)Google Scholar
  4. 4.
    Canetti, R., Cheung, L., Kaynar, D.K., Liskov, M., Lynch, N.A., Pereira, O., Segala, R.: Analyzing security protocols using time-bounded task-PIOAs. Discrete Event Dynamic Systems 18(1), 111–159 (2008)CrossRefGoogle Scholar
  5. 5.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Cheung, L., Lynch, N.A., Segala, R., Vaandrager, F.W.: Switched PIOA: Parallel composition via distributed scheduling. Theor. Comput. Sci. 365(1-2), 83–108 (2006)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Cheung, L., Stoelinga, M., Vaandrager, F.W.: A testing scenario for probabilistic processes. J. ACM 54(6) (2007)MathSciNetCrossRefGoogle Scholar
  9. 9.
    David, A., Larsen, K.G., Legay, A., Nyman, U., Traonouez, L.-M., Wąsowski, A.: Real-time specifications. Int. J. Softw. Tools Techn. Transfer (2013),
  10. 10.
    David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: HSCC, pp. 91–100. ACM (2010)Google Scholar
  11. 11.
    de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 108–122. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  13. 13.
    Delahaye, B., Fahrenberg, U., Larsen, K.G., Legay, A.: Refinement and difference for probabilistic automata. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 22–38. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  15. 15.
    Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: APAC: A tool for reasoning about abstract probabilistic automata. In: QEST, pp. 151–152. IEEE Computer Society (2011)Google Scholar
  16. 16.
    Fahrenberg, U., Larsen, K.G., Legay, A., Traonouez, L.-M.: Parametric and quantitative extensions of modal transition systems. In: Bensalem, S., Lakhnech, Y., Legay, A. (eds.) FPS 2014 (Sifakis Festschrift). LNCS, vol. 8415, pp. 84–97. Springer, Heidelberg (2014)Google Scholar
  17. 17.
    Fahrenberg, U., Legay, A., Thrane, C.: The quantitative linear-time–branching-time spectrum. In: FSTTCS. LIPIcs, vol. 13, pp. 103–114. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)Google Scholar
  18. 18.
    Fahrenberg, U., Thrane, C.R., Larsen, K.G.: Distances for weighted transition systems: Games and properties. In: QAPL. Electr. Proc. Theor. Comput. Sci., vol. 57, pp. 134–147 (2011)Google Scholar
  19. 19.
    Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Jansen, D.N., Hermanns, H., Katoen, J.-P.: A probabilistic extension of UML statecharts. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 355–374. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE (1991)Google Scholar
  22. 22.
    Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: Timed I/O automata: A mathematical framework for modeling and analyzing real-time systems. In: RTSS, pp. 166–177. Society Press (2003)Google Scholar
  24. 24.
    Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  25. 25.
    Larsen, K.G., Legay, A., Traonouez, L.-M., Wąsowski, A.: Robust synthesis for real-time systems. Theor. Comput. Sci. 515, 96–122 (2014)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society (1988)Google Scholar
  27. 27.
    Legay, A., Traonouez, L.-M.: PyEcdar: Towards open source implementation for timed systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 460–463. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  28. 28.
    Parma, A., Segala, R.: Axiomatization of trace semantics for stochastic nondeterministic processes. In: QEST, pp. 294–303. IEEE (2004)Google Scholar
  29. 29.
    Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64–78. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  30. 30.
    Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. NJC 2(2), 250–273 (1995)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Uli Fahrenberg
    • 1
  • Axel Legay
    • 1
  • Louis-Marie Traonouez
    • 1
  1. 1.Inria/IRISARennesFrance

Personalised recommendations