Compact and explainable strategy representations using dtControl

Strategies or controllers are entities arising out of controller synthesis of cyber-physical systems or model checking of non-deterministic systems. A strategy specifies for every state an action that may be taken to satisfy some specification (e. g. , safety). For implementation and debugging purposes, it is beneficial to have concise and human-interpretable representations of strategies. Recent work has shown that decision trees can be used to represent provably-correct strategies concisely. Moreover, they make the strategy explainable and help boost understanding and trust. Compared to representations using lookup tables or binary decision diagrams, decision tree representations are smaller and more explainable. In this talk, I will present the recent advances we have made in decision tree representations of memoryless strategies produced by model checking tools such as PRISM and Storm, as well as controller synthesis tools such as SCOTS and Uppaal Stratego. I will also present a comprehensive evaluation of various decision tree learning algorithms applied to multiple case studies, obtained using our new tool dtControl. The talk is based on our paper published at HSCC 2020, co-authored with Mathias Jackermeier, Pushpak Jagtap, Jan Křetínský, Maximilian Weininger and Majid Zamani.

Authors

• Pranav Ashok

Keywords

No keywords are indexed for this paper.