Small Decision Trees for MDPs with Deductive Synthesis
Roman Andriushchenko, Milan \v{C}e\v{s}ka, Sebastian Junges, Filip Mac\'ak

TL;DR
This paper introduces SMT-based methods and an abstraction-refinement loop to generate concise decision tree representations of optimal policies in MDPs, significantly reducing size while maintaining near-optimality.
Contribution
It presents a novel SMT encoding technique and an abstraction-refinement approach for synthesizing small decision trees for MDP policies, improving interpretability and efficiency.
Findings
Up to 20x smaller decision trees for policies
Effective handling of models with up to 10,000 states
Outperforms existing methods on benchmark problems
Abstract
Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can efficiently compute policies that are optimal with respect to, e.g., reachability probabilities. However, these policies are then given in a tabular format. A longstanding challenge is to represent optimal or almost-optimal policies concisely, e.g., as decision trees. This paper makes two contributions towards this challenge: first, an SMT-based approach to encode a given (optimal) policy as a small decision tree, and second, an abstraction-refinement loop that searches for policies that are optimal within the set of policies that can be represented with a small tree. Technically, the latter combines the SMT encoding with verification approaches for families of Markov chains. The empirical evaluation demonstrates…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFuzzy Logic and Control Systems · Logic, Reasoning, and Knowledge · Network Security and Intrusion Detection
