dtControl documentation

Introduction

dtControl is a tool for compressing memoryless controllers arising out of automatic controller synthesis of cyber-physical systems (CPS). dtControl takes as input controllers synthesised by various formal verification tools and represents them in the form of decision trees. In the process, the size of the controller is reduced greatly, and at the same time, it becomes more explainable. While in principle, memoryless strategies in any format can be handled by dtControl, currently it supports controllers output by two tools: SCOTS (TODO + ff.) and Uppaal Stratego. Additionally, there is rudimentary support for strategies produced by PRISM Model Checker and a pipeline with the model checker Storm is under works.

Moreover, it also supports a CSV-based format, which allows the user to quickly experiment with the techniques provided by dtControl.

We provide a User Manual, which gives information necessary to use dtControl and run the various decision tree learning algorithms implemented in it, as described in the paper “dtControl: Decision Tree Learning Algorithms for Controller Representation”, appearing at the 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2020). Updates introduced in dtControl 2.0 are explained in the paper “dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts”, presented at the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021).

An additional Developer Manual is made available for those who are interested in interfacing their own controller synthesis tools with dtControl or interested in implementing their own strategy representation algorithms.

If you find any mistakes in this documentation or if anything is unclear, we are happy to receive your message. You may contact Maxi, Christoph, Jan or Tabea.

Table of Contents

• User Manual
  • Capabilities
  • Getting Started
    • Installation
    • Input format
    • The command-line interface
    • Understanding the output
    • Timeout
    • Re-run
  • Quick Start with the Python Interface
    • Assigning priorities to splitting strategies
  • Web-Based Graphical User Interface
    • Running your first experiment
    • Inspecting your first result
    • Editing your first result
    • Simulating your first result
  • Semi-automatic Command-Line User Interface
  • Algebraic User-Defined Predicates
    • Standard predicate
    • Coefficient predicates
    • Feature constraints
• Developer Manual
  • Overview
  • Supporting New File Formats
    • The CSV format
    • Implementing a new dataset loader: The dataset management subsystem
  • Extending dtControl with new algorithms: The decision tree learning subsystem
    • Splitting strategies
    • Impurity measures
    • Determinization
  • Supporting New Output Formats
  • Predicate Parser
  • Richer Domain Split