Author name cluster

Pranav Ashok

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

ICRA Conference 2022 Conference Paper

Planning via model checking with decision-tree controllers

Jonis Kiesbye
Kush Grover
Pranav Ashok
Jan Kretínský

Planning problems can be solved not only by planners, but also by model checkers. While the former yield a plan that requires replanning as soon as any fault occurs, the latter provide a “universal” plan (a. k. a. strategy, policy, or controller) able to make decisions under all circumstances. One of the prohibitive aspects of the latter approach is stemming from this very advantage: since it is defined for all possible states of the system, it is typically so large that it does not fit into small memories of embedded devices. As another consequence of the size, its execution may be slow. In this paper, we provide a solution to this issue by linking the model checkers with decision-tree learners, resulting in decision-tree representations of the synthesized strategies. Not only are they dramatically smaller, but also more explainable and orders-of-magnitude faster to execute than plans with replanning. In addition, we describe a method for model validation and debugging via the model checker and the decision-tree learner in the loop. We illustrate the approach on our case study of a robotic arm for picking items in a real industrial setting.

Details

Highlights Conference 2020 Conference Abstract

Compact and explainable strategy representations using dtControl

Pranav Ashok

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.

Details

Highlights Conference 2018 Conference Abstract

Continuous-Time Markov Decisions based on Partial Exploration

Pranav Ashok

ABSTRACT. We provide a framework for speeding up algorithms for time-bounded reachability analysis of continuous-time Markov decision processes. The principle is to find a small, but almost equivalent subsystem of the original system and only analyse the subsystem. Candidates for the subsystem are identified through simulations and iteratively enlarged until runs are represented in the subsystem with high enough probability. The framework is thus dual to that of abstraction refinement. We instantiate the framework in several ways with several traditional algorithms and experimentally confirm orders-of-magnitude speed ups in many cases. A paper based on this work is currently under submission.

Details