dtControl logo

dtControl

Represent controllers as decision trees. Improve memory footprint, boost explainability while preserving guarantees.

dtControl is a tool for compressing memoryless controllers, e.g. arising out of automatic controller synthesis of cyber-physical systems (CPS) or probabilistic model checking. dtControl takes as input a controller synthesised by various formal verification tools and represents them in the form of decision trees. An example is shown below:

Controller of an automatic climate control system for a building with 10 rooms obtained from SCOTS.

Small and explainable decision tree of the same controller (determinized) as output by dtControl

Currently dtControl supports controller output generated by the tools SCOTS, Uppaal Stratego, PRISM, and Storm.

To learn more about dtControl and representing controllers using decision trees, you may want to watch our demo or talk at HSCC 2020, take a look at our tool manual or read our HSCC 2020 paper. The latest features including support of algebraic predicates, categorical predicates, a semi-automatic interface, GUI with several interactive modes, new determinization procedure and an interface for model checkers PRISM and Storm, can be found in our latest TACAS 2021 paper.

Quick Start

You can quickly install dtControl by running the following command

pip install dtcontrol

Check whether dtControl has installed by running

dtcontrol --version

As a quick example, you may download the controller generated by SCOTS for the climate control example shown above by running

wget https://gitlab.lrz.de/i7/dtcontrol/raw/6dd07a5991a0e0a7992c9f7c94e1b9c75c7d94e3/examples/10rooms.scs.zip \
&& unzip 10rooms.scs.zip

following which you may use dtControl to generate a decision tree.

dtcontrol --input 10rooms.scs --use-preset maxfreq

The above command, if executed successfully, will generate a files benchmark.html, benchmark.json and a folder decision_trees which contain the output of the run. You may open the benchmark.html file in any browser to access the generated trees.

Manuals / Documentation

Our complete documentation including user and developer manuals are available at dtcontrol.readthedocs.io. Please ensure that you are referring to the correct version of the documentation. Additionally, we provide video tutorials, covering the most aspects of dtControl.

Artifact evaluation

dtControl has undergone several artifact evaluation processes. All the resources for that are available here.

Contact

For questions, suggestions and comments, you may contact Mathias, Pranav, Maxi, Christoph or Jan. We would also be glad to help you incorporate dtControl into your controller synthesis/usage workflow. Other feature requests are also welcome.

Citing

Cite dtControl in academic publications as:

dtControl was first introduced in:

Other closely related publications include: