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:
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.
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.
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.
dtControl has undergone several artifact evaluation processes. All the resources for that are available here.
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.
Cite dtControl in academic publications as:
dtControl was first introduced in:
Other closely related publications include:
Pranav Ashok, Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Christoph H. Lampert, Viktor Toman.
Strategy Representation by Decision Trees with Linear Classifiers.
QEST 2019.
view / bibtex / pre-print
Pranav Ashok, Jan Kretínský, Kim Guldstrand Larsen, Adrien Le Coënt, Jakob Haahr Taankvist, Maximilian Weininger.
SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes.
QEST 2019.
view / bibtex / pre-print
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretínský.
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.
CAV 2015
view / bibtex / pre-print