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 a controller 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 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).

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.

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