Optimal Time-Bounded Reachability Analysis for Concurrent Systems
Efficient optimal scheduling for concurrent systems over finite horizon is a challenging task up to date. There are two dimensions to this problem. On one hand side optimal behaviour depends on time which has continuous domain. On the other hand for each time point there are exponentially many possible decisions to choose from. In this paper we present the solution to optimal time-bounded reachability problem for Markov automata, one of the most general formalisms to model concurrent systems. Our algorithm is based on the discretisation of the time horizon. In contrast to most existing approaches for similar problems, the step of the discretisation is not fixed. We attempt to discretise only in those time points when the optimal scheduler in fact changes its decision, thus making it very coarse. The empirical evaluation proves the algorithm to improve on existing solutions up to several orders of magnitude.
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher Moments TACAS Link to publication | ||
14:30 30mTalk | Computing the Expected Execution Time of Probabilistic Workflow Nets TACAS Link to publication | ||
15:00 30mTalk | Shepherding Hordes of Markov Chains TACAS Milan Ceska Brno University of Technology , Nils Jansen RWTH Aachen University, Sebastian Junges RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University Link to publication | ||
15:30 30mTalk | Optimal Time-Bounded Reachability Analysis for Concurrent Systems TACAS Link to publication |