Advertisement

Better Quality in Synthesis through Quantitative Objectives

  • Roderick Bloem
  • Krishnendu Chatterjee
  • Thomas A. Henzinger
  • Barbara Jobstmann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another. For example, if a specification asks that every request is followed by a response, one may prefer an implementation that generates responses quickly but does not generate unnecessary responses. We use quantitative properties to measure the “goodness” of an implementation. Using games with corresponding quantitative objectives, we can synthesize “optimal” implementations, which are preferred among the set of possible implementations that satisfy a given specification.

In particular, we show how automata with lexicographic mean-payoff conditions can be used to express many interesting quantitative properties for reactive systems. In this framework, the synthesis of optimal implementations requires the solution of lexicographic mean-payoff games (for safety requirements), and the solution of games with both lexicographic mean-payoff and parity objectives (for liveness requirements). We present algorithms for solving both kinds of novel graph games.

References

  1. 1.
    Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters (1985)Google Scholar
  2. 2.
    Alur, R., Degorre, A., Maler, O., Weiss, G.: On omega-languages defined by mean-payoff conditions. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 333–347. Springer, Heidelberg (2009)Google Scholar
  3. 3.
    Björklund, H., Sandberg, S., Vorobyov, S.: Memoryless determinacy of parity and mean payoff games: a simple proof. Theor. Comput. Sci. (2004)Google Scholar
  4. 4.
    Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmannn, B.: Better quality in synthesis through quantitative objectives. CoRR, abs/0904.2638 (2009)Google Scholar
  5. 5.
    Chakrabarti, A., Chatterjee, K., Henzinger, T.A., Kupferman, O., Majumdar, R.: Verifying quantitative properties using bound functions. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 50–64. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117–133. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Chatterjee, K., de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Compositional quantitative reasoning. In: QEST, pp. 179–188. IEEE Computer Society Press, Los Alamitos (2006)Google Scholar
  8. 8.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 385–400. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: Annual Symposium on Logic in Computer Science (LICS) (2005)Google Scholar
  10. 10.
    Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Games with secure equilibria. In: LICS 2004, pp. 160–169. IEEE, Los Alamitos (2004)Google Scholar
  11. 11.
    de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: LICS 1998, pp. 454–465. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  12. 12.
    de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719. Springer, Heidelberg (2003)Google Scholar
  13. 13.
    de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game relations and metrics. In: LICS, pp. 99–108. IEEE Computer Society Press, Los Alamitos (2007)Google Scholar
  14. 14.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 258–273. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  15. 15.
    Droste, M., Gastin, P.: Weighted automata and weighted logics. Theoretical Computer Science 380, 69–86 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Droste, M., Kuich, W., Rahonis, G.: Multi-valued MSO logics over words and trees. Fundamenta Informaticae 84, 305–327 (2008)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International Journal of Game Theory (1979)Google Scholar
  18. 18.
    Karp, R.M.: A characterization of the minimum cycle mean of a digraph. Discrete Mathematics (1978)Google Scholar
  19. 19.
    King, V., Kupferman, O., Vardi, M.Y.: On the complexity of parity word automata. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, p. 276. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  20. 20.
    Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199–213. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  21. 21.
    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theoretical Computer Science (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Roderick Bloem
    • 1
  • Krishnendu Chatterjee
    • 2
  • Thomas A. Henzinger
    • 3
  • Barbara Jobstmann
    • 3
  1. 1.Graz University of TechnologyAustria
  2. 2.ISTAustria
  3. 3.EPFLSwitzerland

Personalised recommendations