Small Decision Trees for MDPs with Deductive Synthesis

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0198879" target="_blank" >RIV/00216305:26230/26:0198879 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1007/978-3-031-98679-6_8" target="_blank" >https://doi.org/10.1007/978-3-031-98679-6_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-98679-6_8" target="_blank" >10.1007/978-3-031-98679-6_8</a>

Result language

angličtina

Original language name

Small Decision Trees for MDPs with Deductive Synthesis

Original language description

Markov decision processes (MDPs) describe decision making subject to probabilistic uncertainty. A classical problem on MDPs is to compute a policy, selecting actions in every state, that maximizes the probability of reaching a dedicated set of target states. Computing such policies in tabular form is efficiently possible via standard algorithms. However, for further processing by either humans or machines, policies should be represented concisely, e.g., as a decision tree. This paper considers finding (almost) optimal decision trees of minimal depth and contributes a deductive synthesis approach. Technically, we combine pruning the space of concise policies with an abstraction-refinement loop with an SMT-encoding that maps candidate policies into decision trees. Our experiments show that this approach beats the state-of-the-art solver using an MILP encoding by orders of magnitude. The approach also pairs well with heuristic approaches that map a fixed policy into a decision tree: for an MDP with 1.5M states, our approach reduces the size of the given tree by 90%, while sacrificing only 1% of the optimal performance.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA23-06963S" target="_blank" >GA23-06963S: VESCAA: Verifiable and Efficient Synthesis of Controllers for Autonomous Agents</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2025

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Computer Aided Verification

ISBN

978-3-031-98678-9

ISSN

—

e-ISSN

—

Number of pages

24

Pages from-to

169-192

Publisher name

Springer Cham

Place of publication

—

Event location

Zahreb

Event date

Jul 23, 2025

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001562506600008