Advertisement

Near-Optimal Scheduling for LTL with Future Discounting

  • Shota Nakagawa
  • Ichiro HasuoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9533)

Abstract

We study the search problem for optimal schedulers for the linear temporal logic (LTL) with future discounting. The logic, introduced by Almagor, Boker and Kupferman, is a quantitative variant of LTL in which an event in the far future has only discounted contribution to a truth value (that is a real number in the unit interval [0, 1]). The precise problem we study—it naturally arises e.g. in search for a scheduler that recovers from an internal error state as soon as possible—is the following: given a Kripke frame, a formula and a number in [0, 1] called a margin, find a path of the Kripke frame that is optimal with respect to the formula up to the prescribed margin (a truly optimal path may not exist). We present an algorithm for the problem; it works even in the extended setting with propositional quality operators, a setting where (threshold) model-checking is known to be undecidable.

Keywords

Event Horizon Linear Temporal Logic Atomic Proposition Kripke Structure Tree Automaton 
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.

Notes

Acknowledgments

Thanks are due to Shaull Almagor, Shuichi Hirahara, and the anonymous referees, for useful discussions and comments. The authors are supported by Grants-in-Aid No. 24680001, 15KT0012 and 15K11984, JSPS.

References

  1. 1.
    Abdeddaïm, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272–300 (2006)CrossRefMathSciNetzbMATHGoogle Scholar
  2. 2.
    Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 15–27. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 424–439. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  4. 4.
    Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. Extended version of [2], preprint (private communication) (2014)Google Scholar
  5. 5.
    Baier, C., Dubslaff, C., Klüppelholz, S.: Trade-off analysis meets probabilistic model checking. In: Henzinger, T.A., Miller, D. (eds.), CSL-LICS 2014, p. 1. ACM (2014)Google Scholar
  6. 6.
    Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  7. 7.
    Bouyer, P., Markey, N., Matteplackel, R.M.: Averaging in LTL. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 266–280. Springer, Heidelberg (2014)Google Scholar
  8. 8.
    Černý, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243–259. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. Logical Methods Comput. Sci. 6(3), 1–23 (2010)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS 2005, pp. 178–187. IEEE Computer Society (2005)Google Scholar
  11. 11.
    Cheung, L., Stoelinga, M., Vaandrager, F.W.: A testing scenario for probabilistic processes. J. ACM 54(6) (2007). Article No. 29Google 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, volume 2719 of LNCS, pp. 1022–1037. Springer (2003)Google Scholar
  13. 13.
    Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. Theor. Comput. Sci. 410(37), 3481–3494 (2009)CrossRefMathSciNetzbMATHGoogle Scholar
  14. 14.
    Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electr. Notes Theor. Comput. Sci. 220(3), 61–77 (2008)CrossRefzbMATHGoogle Scholar
  15. 15.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  16. 16.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)CrossRefMathSciNetzbMATHGoogle Scholar
  18. 18.
    Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984)CrossRefMathSciNetzbMATHGoogle Scholar
  19. 19.
    Nakagawa, S., Hasuo, I.: Near-optimal scheduling for LTL with future discounting (2015). CoRR, abs/1410.4950
  20. 20.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11–13, 1989, pp. 179–190. ACM Press (1989)Google Scholar
  21. 21.
    Rahonis, G.: Infinite fuzzy computations. Fuzzy Sets Syst. 153(2), 275–288 (2005)CrossRefMathSciNetzbMATHGoogle Scholar
  22. 22.
    van Glabbeek, R.J.: The linear time-branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.), Handbook of Process Algebra, chapter 1, pp. 3–99. Elsevier (2001)Google Scholar
  23. 23.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency: Structure Versus Automata, vol. 1043 of LNCS, pp. 238–266. Springer-Verlag (1996)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.University of TokyoTokyoJapan

Personalised recommendations