Digging for Decision Trees: A Case Study in Strategy Sampling and Learning

TL;DR

This paper presents a formal model for optimizing open-pit mine operations using Markov automata, proposing statistical model checking and decision trees to address state space challenges and improve strategy interpretability.

Contribution

It introduces a novel approach combining statistical model checking, feature-based strategies, and decision trees for mine operation optimization, addressing scalability and explainability.

Findings

Model checking is infeasible for small mine instances due to state space explosion.

Q-learning has limitations in this context, influenced by feature selection.

Decision trees provide an explainable strategy representation.

Abstract

We introduce a formal model of transportation in an open-pit mine for the purpose of optimising the mine's operations. The model is a network of Markov automata (MA); the optimisation goal corresponds to maximising a time-bounded expected reward property. Today's model checking algorithms exacerbate the state space explosion problem by applying a discretisation approach to such properties on MA. We show that model checking is infeasible even for small mine instances. Instead, we propose statistical model checking with lightweight strategy sampling or table-based Q-learning over untimed strategies as an alternative to approach the optimisation task, using the Modest Toolset's modes tool. We add support for partial observability to modes so that strategies can be based on carefully selected model features, and we implement a connection from modes to the dtControl tool to convert sampled or learned strategies into decision trees. We experimentally evaluate the adequacy of our new tooling on the open-pit mine case study. Our experiments demonstrate the limitations of Q-learning, the impact of feature selection, and the usefulness of decision trees as an explainable representation.