pith. sign in

arxiv: 1906.08178 · v2 · pith:DM5DHSD7new · submitted 2019-06-19 · 💻 cs.LO

Strategy Representation by Decision Trees with Linear Classifiers

Pranav Ashok , Tom\'a\v{s} Br\'azdil , Krishnendu Chatterjee , Jan K\v{r}et\'insk\'y , Christoph H. Lampert , Viktor Toman This is my paper

Pith reviewed 2026-05-25 19:55 UTC · model grok-4.3

classification 💻 cs.LO
keywords strategy representationdecision treeslinear classifiersgraph gamesMarkov decision processesreactive synthesisomega-regular conditionssuccinct representation
0
0 comments X

The pith

Decision trees with linear classifiers inside nodes represent winning strategies from graph games and MDPs more compactly than standard decision trees.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that decision trees whose internal nodes use linear classifiers instead of single-variable tests can encode complete, error-free strategies for graph games and Markov decision processes. This matters because strategies must be stored and executed exactly in verification and synthesis tasks, yet standard decision trees often grow large when the underlying state space has linear structure. The authors implement the approach and run it on benchmark problems, demonstrating consistent size reductions while preserving the exact strategy behavior required by omega-regular winning conditions. If correct, the method directly improves the practical handling of strategies in reactive systems.

Core claim

The authors propose replacing the usual threshold tests in decision-tree nodes with linear classifiers, implement the construction for strategies in graph games and MDPs, and show experimentally that the resulting trees are substantially smaller than those produced by ordinary decision-tree learners while still representing the full strategy without error.

What carries the argument

Decision tree whose internal nodes each contain a linear classifier (a hyperplane defined over state variables) that partitions the state space according to the strategy's action choice.

If this is right

  • Exact strategy representation remains possible even when the state space admits linear decision boundaries.
  • Fewer nodes are needed to store and evaluate the same strategy compared with ordinary decision trees.
  • The same data structure applies across safety, reachability, parity, and other omega-regular conditions.
  • The representation can be obtained automatically from an existing strategy via entropy minimization.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same node structure might reduce memory use when strategies are deployed in embedded controllers.
  • If the linear-classifier trees can be converted back to explicit controllers, they could serve as a compression step before code generation.
  • The method may extend naturally to strategies that are only approximately optimal, provided the error tolerance is made explicit.

Load-bearing premise

Linear classifiers exist that can be placed at tree nodes so the resulting tree matches any given winning strategy exactly, and an entropy-based learning procedure can find them.

What would settle it

A concrete game or MDP for which a winning strategy is known, yet the linear-classifier tree learner returns a tree whose decisions differ from the strategy on at least one reachable state.

Figures

Figures reproduced from arXiv: 1906.08178 by Christoph H. Lampert, Jan K\v{r}et\'insk\'y, Krishnendu Chatterjee, Pranav Ashok, Tom\'a\v{s} Br\'azdil, Viktor Toman.

Figure 1
Figure 1. Figure 1: A reactive system with two request channels. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A decision tree for {0, 1, 2, 3, 7} ⊆ N 1 . Decision tree (DT) over N d is a tuple T = (T, ρ, θ) where T is a finite rooted binary (ordered) tree, ρ assigns to every inner node an (in)equality predi￾cate comparing arithmetical expressions over vari￾ables {x1, . . . , xd}, and θ assigns to every leaf a value YES or NO. The language L(T ) ⊆ N d of the tree is defined as follows. For a vector x = (x1, . . . ,… view at source ↗
Figure 3
Figure 3. Figure 3: Good (triangles) and Bad (circles). No horizontal or vertical classifier can sep￾arate Train, but Train is lin￾early separable (by a slanted classifier). During the construction of a decision tree for a given dataset, each node corresponds to a certain subset of the dataset. This subset exactly captures the data points from the dataset that would reach the node starting from the root and progressing based … view at source ↗
Figure 4
Figure 4. Figure 4: A decision tree for the system’s controller. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Running Algorithm 3 on a sample dataset consisting of circle ( [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The Decision tree resulting from the above steps. [PITH_FULL_IMAGE:figures/full_fig_p011_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: True/False Positive/Negative. True/false positive/negative. Consider a fixed linear classifier c, and a sample x ∈ Train such that c(x) = YES. If x ∈ Good, then x is a true positive (TP) w.r.t. the clas￾sifier c, otherwise x ∈ Bad and thus x is a false positive (FP). Consider a different sam￾ple x¯ ∈ Train such that c(x¯) = NO. If x¯ ∈ Bad, then x¯ is a true negative (TN ), otherwise x¯ ∈ Good and x¯ is a … view at source ↗
Figure 8
Figure 8. Figure 8: Area under the curve for w = (1, 0) w.r.t. Good (triangles) and Bad (circles). Algorithm 4 Split procedure – area under the curve (auc) Input: data ⊆ N |Var| partitioned into subsets dataG and dataB. Output: A predicate pr maximizing area under the sat and unsat ROC curves. 1: areas ← ∅ 2: for pr ∈ Pred do 3: wsat ← LinearLeastSquares(data[pr ]) 4: wunsat ← LinearLeastSquares(data[¬pr ]) 5: areas(pr ) ← au… view at source ↗
Figure 9
Figure 9. Figure 9: Scheduling of Washing Cycles. LTL synthesis. In reactive synthesis, most properties considered in practice are ω-regular objectives, which can be specified as linear-time temporal logic (LTL) for￾mulae over input/output signals [44]. Given an LTL formula and input/output signal partitioning, the controller synthesis for this specification is reducible to solving a graph game with parity objective. In our e… view at source ↗
Figure 10
Figure 10. Figure 10: LTL synthesis [PITH_FULL_IMAGE:figures/full_fig_p015_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: LTL synthesis with randomized environment. [PITH_FULL_IMAGE:figures/full_fig_p016_11.png] view at source ↗
Figure 13
Figure 13. Figure 13: Scheduling of Washing Cycles – overall summary. [PITH_FULL_IMAGE:figures/full_fig_p023_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: LTL synthesis – overall summary. 23 [PITH_FULL_IMAGE:figures/full_fig_p023_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: LTL synthesis with randomized environment – overall summary. [PITH_FULL_IMAGE:figures/full_fig_p024_15.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes decision trees augmented with linear classifiers at internal nodes as a data structure for representing winning strategies in graph games and MDPs. It argues that this yields more succinct exact representations than standard decision trees, describes an entropy-minimization learning procedure adapted from machine learning, implements the approach, and reports experimental results on graph games and MDPs demonstrating improved efficiency.

Significance. If the method guarantees exact (zero-error) strategy representations and the reported efficiency gains hold under rigorous baselines, the work could improve the practicality of strategy storage and manipulation in reactive synthesis and probabilistic verification tools. The extension to linear classifiers addresses limitations of axis-aligned splits in standard decision trees for more complex state spaces.

major comments (2)
  1. [§4] §4 (Learning procedure): The entropy-minimization splitting rule is adapted from standard decision-tree induction, which is a heuristic that permits impure leaves. No argument, invariant, or termination condition is supplied showing that the procedure is guaranteed to produce a tree whose leaves assign exactly the prescribed strategy action to every state (zero error), which is required for the representation to be valid under ω-regular winning conditions.
  2. [§5] §5 (Experiments): The abstract and experimental section claim superior efficiency, yet the provided description supplies no quantitative metrics (tree size, construction time, memory), no baseline comparisons against standard decision trees or other succinct representations (e.g., BDDs), and no verification procedure confirming that the learned trees are exact on the full state space.
minor comments (2)
  1. [§3] Notation for linear classifiers inside nodes should be introduced with an explicit definition (e.g., the form of the hyperplane and how the split is evaluated on game states).
  2. [Abstract] The abstract states that 'no error is allowed' yet does not clarify whether the implementation includes a post-processing purity check or rejection of impure trees.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments. We address each major comment point by point below, indicating planned revisions where appropriate.

read point-by-point responses

  1. Referee: [§4] §4 (Learning procedure): The entropy-minimization splitting rule is adapted from standard decision-tree induction, which is a heuristic that permits impure leaves. No argument, invariant, or termination condition is supplied showing that the procedure is guaranteed to produce a tree whose leaves assign exactly the prescribed strategy action to every state (zero error), which is required for the representation to be valid under ω-regular winning conditions.

    Authors: The entropy-minimization rule is adapted such that splitting continues until every leaf is pure (all states in the leaf share the same strategy action). Because the state spaces of the considered games and MDPs are finite, the recursion terminates. Linear classifiers increase the chance of achieving purity compared with axis-aligned splits. We will add an explicit description of the purity invariant and termination argument to §4. revision: yes

  2. Referee: [§5] §5 (Experiments): The abstract and experimental section claim superior efficiency, yet the provided description supplies no quantitative metrics (tree size, construction time, memory), no baseline comparisons against standard decision trees or other succinct representations (e.g., BDDs), and no verification procedure confirming that the learned trees are exact on the full state space.

    Authors: Section 5 already reports quantitative metrics (node counts, construction times, memory) and direct comparisons against standard decision trees on the same benchmarks, confirming the claimed efficiency gains. Exactness is verified by evaluating each learned tree against the original strategy on every state of each benchmark instance. Comparisons to BDDs lie outside the paper's scope, which focuses on decision-tree representations. We will revise §5 to present the metrics and verification procedure more prominently. revision: partial

Circularity Check

0 steps flagged

No circularity; efficiency claim rests on experiments, not self-referential derivation

full rationale

The paper introduces decision trees augmented with linear classifiers as a data structure for strategy representation and supports the efficiency claim solely via implementation plus reported experiments on graph games and MDPs. No equations, predictions, or first-principles derivations appear that reduce the claimed succinctness or exact-match property to a fitted parameter, self-definition, or self-citation chain. The entropy-minimization procedure is presented as a standard ML technique adapted to the zero-error requirement; its success is treated as an empirical outcome rather than a definitional guarantee. The central claim therefore remains independent of its own inputs and receives the default non-circularity finding.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that linear classifiers can be integrated into decision trees while preserving exact representation of arbitrary strategies; no free parameters or invented entities are mentioned in the abstract.

axioms (1)
  • domain assumption Linear classifiers placed at decision-tree nodes can be selected so that the tree exactly encodes any winning strategy without error.
    Required for the representation to remain complete and exact, as stated in the abstract's contrast with traditional ML where errors are tolerated.

pith-pipeline@v0.9.0 · 5753 in / 1231 out tokens · 41667 ms · 2026-05-25T19:55:20.898107+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

51 extracted references · 51 canonical work pages · 1 internal anchor

  1. [1]

    Abadi, L

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

    work page 1989

  2. [2]

    S. B. Akers. Binary decision diagrams. IEEE Transactions on Computers, C-27(6):509–516, 1978

    work page 1978

  3. [3]

    R. Alur, R. Bod ´ık, E. Dallal, D. Fisman, P. Garg, G. Juniwal, H. Kress-Gazit, P. Madhusu- dan, M. M. K. Martin, M. Raghothaman, S. Saha, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided synthesis. In Dependable Software Systems Engi- neering, pages 1–25. 2015

    work page 2015

  4. [4]

    R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49:672–713, 2002

    work page 2002

  5. [5]

    Baier and J

    C. Baier and J. Katoen. Principles of Model Checking. 2008

    work page 2008

  6. [6]

    Blass, Y

    A. Blass, Y . Gurevich, L. Nachmanson, and M. Veanes. Play to test. InFATES, pages 32–46, 2005

    work page 2005

  7. [7]

    Boutilier and R

    C. Boutilier and R. Dearden. Approximate value trees in structured dynamic programming. In ICML, pages 54–62, 1996

    work page 1996

  8. [8]

    Boutilier, R

    C. Boutilier, R. Dearden, and M. Goldszmidt. Exploiting structure in policy construction. In IJCAI, pages 1104–1113, 1995

    work page 1995

  9. [9]

    Br ´azdil, K

    T. Br ´azdil, K. Chatterjee, M. Chmel´ık, A. Fellner, and J. Kˇret´ınsk´y. Counterexample expla- nation by learning small strategies in Markov decision processes. In CAV, pages 158–177, 2015

    work page 2015

  10. [10]

    Br ´azdil, K

    T. Br ´azdil, K. Chatterjee, M. Chmel ´ık, A. Gupta, and P. Novotn ´y. Stochastic shortest path with energy constraints in POMDPs: (extended abstract). In AAMAS, pages 1465–1466, 2016

    work page 2016

  11. [11]

    Br ´azdil, K

    T. Br ´azdil, K. Chatterjee, J. K ˇret´ınsk´y, and V . Toman. Strategy representation by decision trees in reactive synthesis. In TACAS, pages 385–407, 2018

    work page 2018

  12. [12]

    Breiman, J

    L. Breiman, J. H. Friedman, R. A. Olshen, and C. J. Stone. Classification and Regression Trees. 1984

    work page 1984

  13. [13]

    R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986

    work page 1986

  14. [14]

    J. B ¨uchi. On a decision method in restricted second-order arithmetic. In International Congress on Logic, Methodology, and Philosophy of Science, pages 1–11, 1962

    work page 1962

  15. [15]

    B ¨uchi and L

    J. B ¨uchi and L. Landweber. Solving sequential conditions by finite-state strategies. Trans- actions of the AMS, 138:295–311, 1969

    work page 1969

  16. [16]

    Chatterjee

    K. Chatterjee. Stochastic Omega-Regular Games. PhD thesis, University of California at Berkeley, USA, 2007

    work page 2007

  17. [17]

    Chatterjee, T

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

    work page 2015

  18. [18]

    A. Church. Logic, arithmetic, and automata. In International Congress of Mathematicians, pages 23–35, 1962

    work page 1962

  19. [19]

    E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors. Handbook of Model Check- ing, chapter: Games and Synthesis. 2018

    work page 2018

  20. [20]

    de Alfaro and T

    L. de Alfaro and T. Henzinger. Interface automata. In FSE, pages 109–120, 2001

    work page 2001

  21. [21]

    de Alfaro, T

    L. de Alfaro, T. Henzinger, and F. Mang. Detecting errors before reaching them. In CAV, pages 186–201, 2000

    work page 2000

  22. [22]

    Dehnert, S

    C. Dehnert, S. Junges, J. Katoen, and M. V olk. A storm is coming: A modern probabilistic model checker. In CAV, pages 592–600, 2017

    work page 2017

  23. [23]

    D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. 1989

    work page 1989

  24. [24]

    D. P. Dobkin. A nonlinear lower bound on linear search tree programs for solving knapsack problems. Journal of Computer and System Sciences, 13(1):69–73, 1976

    work page 1976

  25. [25]

    Duret-Lutz, A

    A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0 - A framework for LTL andω-automata manipulation. In ATVA, pages 122–129, 2016

    work page 2016

  26. [26]

    Frank, Y

    E. Frank, Y . Wang, S. Inglis, G. Holmes, and I. H. Witten. Using model trees for classifica- tion. Machine learning, 32(1):63–76, 1998

    work page 1998

  27. [27]

    P. Garg, D. Neider, P. Madhusudan, and D. Roth. Learning invariants using decision trees and implication counterexamples. In POPL, pages 499–512, 2016

    work page 2016

  28. [28]

    Gurevich and L

    Y . Gurevich and L. Harrington. Trees, automata, and games. In STOC, pages 60–65, 1982

    work page 1982

  29. [29]

    Henzinger, O

    T. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. I&C, 173:64–81, 2002

    work page 2002

  30. [30]

    S. Jacobs. Extended AIGER format for synthesis. CoRR, abs/1405.5793, 2014

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  31. [31]

    Jacobs, R

    S. Jacobs, R. Bloem, R. Brenguier, R. K ¨onighofer, G. A. P ´erez, J. Raskin, L. Ryzhyk, O. Sankur, M. Seidl, L. Tentrup, and A. Walker. The second reactive synthesis competi- tion (SYNTCOMP 2015). In SYNT, pages 27–57, 2015

    work page 2015

  32. [32]

    Kom ´arkov´a and J

    Z. Kom ´arkov´a and J. Kˇret´ınsk´y. Rabinizer 3: Safraless translation of LTL to small determin- istic automata. In ATVA, pages 235–241, 2014

    work page 2014

  33. [33]

    Kontschieder, M

    P. Kontschieder, M. Fiterau, A. Criminisi, and S. R. Bul `o. Deep neural decision forests. In IJCAI, pages 4190–4194, 2016

    work page 2016

  34. [34]

    M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: probabilistic symbolic model checker. In TOOLS, pages 200–204, 2002

    work page 2002

  35. [35]

    M. Z. Kwiatkowska, G. Norman, and D. Parker. The PRISM benchmark suite. In QEST, pages 203–204, 2012

    work page 2012

  36. [36]

    Landwehr, M

    N. Landwehr, M. Hall, and E. Frank. Logistic model trees. In ECML, pages 241–252, 2003

    work page 2003

  37. [37]

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

    work page 2010

  38. [38]

    Manna and A

    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specifi- cation. 1992

    work page 1992

  39. [39]

    McNaughton

    R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65:149–184, 1993

    work page 1993

  40. [40]

    T. M. Mitchell. Machine Learning. 1997

    work page 1997

  41. [41]

    D. Neider. Small strategies for safety games. In ATVA, pages 306–320, 2011

    work page 2011

  42. [42]

    Neider, S

    D. Neider, S. Saha, and P. Madhusudan. Synthesizing piece-wise functions by learning clas- sifiers. In TACAS, pages 186–203, 2016

    work page 2016

  43. [43]

    Neider and U

    D. Neider and U. Topcu. An automaton learning approach to solving safety games over infinite graphs. In TACAS, pages 204–221, 2016

    work page 2016

  44. [44]

    A. Pnueli. The temporal logic of programs. In FOCS, pages 46–57, 1977

    work page 1977

  45. [45]

    Pnueli and R

    A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, pages 179–190, 1989

    work page 1989

  46. [46]

    J. R. Quinlan. Induction of decision trees. Machine Learning, 1(1):81–106, 1986

    work page 1986

  47. [47]

    J. R. Quinlan. Learning with Continuous Classes. In Australian Joint Conference on Artificial Intelligence, pages 343–348, 1992. 20

    work page 1992

  48. [48]

    M. Rabin. Automata on Infinite Objects and Church’s Problem. Conference Series in Math- ematics. 1969

    work page 1969

  49. [49]

    Ramadge and W

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

    work page 1987

  50. [50]

    W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages , pages 389–455. 1997

    work page 1997

  51. [51]

    Wimmer, B

    R. Wimmer, B. Braitling, B. Becker, E. M. Hahn, P. Crouzen, H. Hermanns, A. Dhama, and O. Theel. Symblicit calculation of long-run averages for concurrent probabilistic systems. In QEST, pages 27–36, 2010. 21 Appendix A Linear least squares problem In this work, we consider dataset Train to be a set of tuples (samples) over natural numbers x∈ Nd. Consider...

    work page 2010