Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices

  • Natsuki Urabe
  • Ichiro Hasuo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


We introduce notions of simulation between semiring-weighted automata as models of quantitative systems. Our simulations are instances of the categorical/coalgebraic notions previously studied by Hasuo—hence soundness wrt. language inclusion comes for free—but are concretely presented as matrices that are subject to linear inequality constraints. Pervasiveness of these formalisms allows us to exploit existing algorithms in: searching for a simulation, and hence verifying quantitative correctness that is formulated as language inclusion. Transformations of automata that aid search for simulations are introduced, too. This verification workflow is implemented for the plus-times and max-plus semirings.


Linear Inequality Simulation Matrice Linear Inequality Constraint Probabilistic Automaton Payoff Game 
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.
    The GNU linear programming kit,
  2. 2.
    Akian, M., Gaubert, S., Guterman, A.E.: Tropical polyhedra are equivalent to mean payoff games. International Journal of Algebra and Computation 22(1) (2012)Google Scholar
  3. 3.
    Baier, C., Hermanns, H., Katoen, J.P.: Probabilistic weak simulation is decidable in polynomial time. Inf. Process. Lett. 89(3), 123–130 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Bzem, M., Nieuwenhuis, R., Rodríguez-Carbonell, E.: Exponential behaviour of the butkovic-zimmermann algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Mathematics 156(18), 3506–3509 (2008)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theory Comput. Syst. 36(3), 231–245 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Butkovic, P., Zimmermann, K.: A strongly polynomial algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Math. 154(3), 437–446 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. Logical Methods in Computer Science 6(3) (2010)Google Scholar
  8. 8.
    Cîrstea, C.: Maximal traces and path-based coalgebraic temporal logics. Theor. Comput. Sci. 412(38), 5025–5042 (2011)CrossRefzbMATHGoogle Scholar
  9. 9.
    Doyen, L., Henzinger, T.A., Raskin, J.F.: Equivalence of labeled markov chains. Int. J. Found. Comput. Sci. 19(3), 549–563 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  10. 10.
    Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International Journal of Game Theory 8(2), 109–113 (1979)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Hasuo, I.: Generic forward and backward simulations. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 406–420. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Hasuo, I.: Generic forward and backward simulations II: Probabilistic simulation. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 447–461. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Hasuo, I., Jacobs, B.: Context-free languages via coalgebraic trace semantics. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 213–231. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Computer Science 3(4) (2007)Google Scholar
  15. 15.
    Hasuo, I., Kawabe, Y., Sakurada, H.: Probabilistic anonymity via coalgebraic simulations. Theor. Comput. Sci. 411(22-24), 2239–2259 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Hughes, J., Jacobs, B.: Simulations in coalgebra. Theor. Comput. Sci. 327(1-2), 71–108 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  17. 17.
    Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations, Draft of a book (ver. 2.0) (2012) (available online)Google Scholar
  18. 18.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE Computer Society (1991)Google Scholar
  19. 19.
    Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Language equivalence for probabilistic automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 526–540. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  20. 20.
    Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Algorithmic probabilistic game semantics—playing games with automata. Formal Methods in System Design 43(2), 285–312 (2013)CrossRefzbMATHGoogle Scholar
  21. 21.
    Konstantinos, C., Catuscia, P.: Probable innocence revisited. Theoretical Computer Science 367(1), 123–138 (2006)zbMATHMathSciNetGoogle Scholar
  22. 22.
    Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 101–112. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  23. 23.
    Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. Untimed systems. Inf. Comput. 121(2), 214–233 (1995)CrossRefzbMATHMathSciNetGoogle Scholar
  24. 24.
    Pin, J.E.: Tropical semirings. Idempotency (Bristol, 1994), 50–69 (1998)Google Scholar
  25. 25.
    Power, J., Turi, D.: A coalgebraic foundation for linear time semantics. Electr. Notes Theor. Comput. Sci. 29, 259–274 (1999)CrossRefMathSciNetGoogle Scholar
  26. 26.
    Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web transactions. ACM Trans. Inf. Syst. Secur. 1(1), 66–92 (1998)CrossRefGoogle Scholar
  27. 27.
    Tzeng, W.G.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J. Comput. 21(2), 216–227 (1992)CrossRefzbMATHMathSciNetGoogle Scholar
  28. 28.
    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1&2), 343–359 (1996)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Natsuki Urabe
    • 1
  • Ichiro Hasuo
    • 1
  1. 1.University of TokyoJapan

Personalised recommendations