ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 15:30 - 16:00 at SUN I - Hybrid and Stochastic Systems Chair(s): Kim Larsen

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 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change