Skip to main content
SpringerLink
Log in
Book cover

International Conference on Quantitative Evaluation of Systems

QEST 2019: Quantitative Evaluation of Systems pp 109–128Cite as

Strategy Representation by Decision Trees with Linear Classifiers

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11785))

Abstract

Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of \(\omega \)-regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    The set of considered predicates \( Pred \) is typically domain-specific, and finitely restricted in a natural way. In this work, we consider (in)equality predicates that compare values of variables to constants. A natural finite restriction is to consider only constants that appear in the dataset.

References

  1. Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: ICALP, pp. 1–17 (1989)

    Google Scholar 

  2. Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C–27(6), 509–516 (1978)

    Article  Google Scholar 

  3. Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, pp. 1–25 (2015)

    Google Scholar 

  4. Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  5. Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C.H., Toman, V.: Strategy representation by decision trees with linear classifiers. arXiv.org.1906.08178 (2019)

  6. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, New York (2008)

    MATH  Google Scholar 

  7. Blass, A., Gurevich, Y., Nachmanson, L., Veanes, M.: Play to test. In: FATES, pp. 32–46 (2005)

    Google Scholar 

  8. Boutilier, C., Dearden, R.: Approximate value trees in structured dynamic programming. In: ICML, pp. 54–62 (1996)

    Google Scholar 

  9. Boutilier, C., Dearden, R., Goldszmidt, M.: Exploiting structure in policy construction. In: IJCAI, pp. 1104–1113 (1995)

    Google Scholar 

  10. Brázdil, T., Chatterjee, K., Chmelík, M., Fellner, A., Křetínský, J.: Counterexample explanation by learning small strategies in Markov decision processes. In: CAV, pp. 158–177 (2015)

    Chapter  Google Scholar 

  11. Brázdil, T., Chatterjee, K., Chmelík, M., Gupta, A., Novotný, P.: Stochastic shortest path with energy constraints in POMDPs: (extended abstract). In: AAMAS, pp. 1465–1466 (2016)

    Google Scholar 

  12. Brázdil, T., Chatterjee, K., Křetínský, J., Toman, V.: Strategy representation by decision trees in reactive synthesis. In: TACAS, pp. 385–407 (2018)

    Google Scholar 

  13. Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and Regression Trees. Chapman and Hall/CRC, Boca Raton (1984)

    MATH  Google Scholar 

  14. Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C–35(8), 677–691 (1986)

    Article  Google Scholar 

  15. Büchi, J.: On a decision method in restricted second-order arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11 (1962)

    Google Scholar 

  16. Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311 (1969)

    Article  MathSciNet  Google Scholar 

  17. Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. J. ACM 62(1), 9:1–9:34 (2015)

    Article  MathSciNet  Google Scholar 

  18. Church, A.: Logic, arithmetic, and automata. In: International Congress of Mathematicians, pp. 23–35 (1962)

    Google Scholar 

  19. de Alfaro, L., Henzinger, T.: Interface automata. In: FSE, pp. 109–120 (2001)

    Google Scholar 

  20. de Alfaro, L., Henzinger, T., Mang, F.: Detecting errors before reaching them. In: CAV, pp. 186–201 (2000)

    Google Scholar 

  21. Dehnert, C., Junges, S., Katoen, J., Volk, M.: A storm is coming: a modern probabilistic model checker. In: CAV, pp. 592–600 (2017)

    Google Scholar 

  22. Dill, D.: Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, Cambridge (1989)

    Book  Google Scholar 

  23. Dobkin, D.P.: A nonlinear lower bound on linear search tree programs for solving knapsack problems. J. Comput. Syst. Sci. 13(1), 69–73 (1976)

    Article  MathSciNet  Google Scholar 

  24. Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - a framework for LTL and \(\omega \)-automata manipulation. In: ATVA, pp. 122–129 (2016)

    Google Scholar 

  25. Frank, E., Wang, Y., Inglis, S., Holmes, G., Witten, I.H.: Using model trees for classification. Mach. Learn. 32(1), 63–76 (1998)

    Article  Google Scholar 

  26. Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: POPL, pp. 499–512 (2016)

    Google Scholar 

  27. Gurevich, Y., Harrington, L.: Trees, automata, and games. In: STOC, pp. 60–65 (1982)

    Google Scholar 

  28. Henzinger, T., Kupferman, O., Rajamani, S.: Fair simulation. Inf. Comput. 173, 64–81 (2002)

    Article  MathSciNet  Google Scholar 

  29. Jacobs, S.: Extended AIGER format for synthesis. CoRR, abs/1405.5793 (2014)

    Google Scholar 

  30. S. Jacobs, et al.: The second reactive synthesis competition (SYNTCOMP 2015). In: SYNT, pp. 27–57 (2015)

    Google Scholar 

  31. Komárková, Z., Křetínský, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: ATVA, pp. 235–241 (2014)

    Google Scholar 

  32. Kontschieder, P., Fiterau, M., Criminisi, A., Bulò, S.R.: Deep neural decision forests. In: IJCAI, pp. 4190–4194 (2016)

    Google Scholar 

  33. Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: TOOLS, pp. 200–204 (2002)

    Google Scholar 

  34. Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203–204 (2012)

    Google Scholar 

  35. Landwehr, N., Hall, M., Frank, E.: Logistic model trees. In: ECML, pp. 241–252 (2003)

    Chapter  Google Scholar 

  36. Liu, S., Panangadan, A., Raghavendra, C.S., Talukder, A.: Compact representation of coordinated sampling policies for body sensor networks. In: Advances in Communication and Networks, pp. 6–10 (2010)

    Google Scholar 

  37. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Kluwer Academic, Norwell (1992)

    Book  Google Scholar 

  38. McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65, 149–184 (1993)

    Article  MathSciNet  Google Scholar 

  39. Mitchell, T.M.: Machine Learning. McGraw Hill, Maidenhead (1997)

    MATH  Google Scholar 

  40. Neider, D.: Small strategies for safety games. In: ATVA, pp. 306–320 (2011)

    Chapter  Google Scholar 

  41. Neider, D., Saha, S., Madhusudan, P.: Synthesizing piece-wise functions by learning classifiers. In: TACAS, pp. 186–203 (2016)

    Google Scholar 

  42. Neider, D., Topcu, U.: An automaton learning approach to solving safety games over infinite graphs. In: TACAS, pp. 204–221 (2016)

    Google Scholar 

  43. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)

    Google Scholar 

  44. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)

    Google Scholar 

  45. Quinlan, J.R.: Induction of decision trees. Mach. Learn. 1(1), 81–106 (1986)

    Google Scholar 

  46. Quinlan, J.R.: Learning with continuous classes. In: Australian Joint Conference on Artificial Intelligence, pp. 343–348 (1992)

    Google Scholar 

  47. Rabin, M.: Automata on infinite objects and Church’s problem. In: Conference Series in Mathematics (1969)

    Google Scholar 

  48. Ramadge, P., Wonham, W.: Supervisory control of a class of discrete-event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)

    Article  MathSciNet  Google Scholar 

  49. Thomas, Wolfgang: Languages, automata, and logic. In: Rozenberg, Grzegorz, Salomaa, Arto (eds.) Handbook of Formal Languages, pp. 389–455. Springer, Heidelberg (1997). https://doi.org/10.1007/978-3-642-59126-6_7

    Chapter  Google Scholar 

  50. R. Wimmer, et al.: Symblicit calculation of long-run averages for concurrent probabilistic systems. In: QEST, pp. 27–36 (2010)

    Google Scholar 

Download references

Acknowledgments

This work has been partially supported by DFG Grant No KR 4890/2-1 (SUV: Statistical Unbounded Verification), TUM IGSSE Grant 10.06 (PARSEC), Czech Science Foundation grant No. 18-11193S, Vienna Science and Technology Fund (WWTF) Project ICT15-003, the Austrian Science Fund (FWF) NFN Grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE).

Author information

Authors and Affiliations

  1. Technical University of Munich, Munich, Germany

    Pranav Ashok & Jan Křetínský

  2. Masaryk University, Brno, Czech Republic

    Tomáš Brázdil

  3. IST Austria, Klosterneuburg, Austria

    Krishnendu Chatterjee, Christoph H. Lampert & Viktor Toman

Authors
  1. Pranav Ashok
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tomáš Brázdil
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Krishnendu Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jan Křetínský
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Christoph H. Lampert
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Viktor Toman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Viktor Toman .

Editor information

Editors and Affiliations

  1. University of Birmingham, Birmingham, UK

    David Parker

  2. Saarland University, Saarbrücken, Germany

    Verena Wolf

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C.H., Toman, V. (2019). Strategy Representation by Decision Trees with Linear Classifiers. In: Parker, D., Wolf, V. (eds) Quantitative Evaluation of Systems. QEST 2019. Lecture Notes in Computer Science(), vol 11785. Springer, Cham. https://doi.org/10.1007/978-3-030-30281-8_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30281-8_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30280-1

  • Online ISBN: 978-3-030-30281-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation