Safe Schedulability of Bounded-Rate Multi-Mode Systems.
Rajeev Alur, Vojtec Forejt, Salar Moarref, and Ashutosh Trivedi
Bounded-rate multi-mode systems (BMS) are hybrid sys-
tems that can switch freely among a finite set of modes, and
whose dynamics is specified by a finite number of real-valued
variables with mode-dependent rates that can vary within
given bounded sets. The schedulability problem for BMS
is defined as an infinite-round game between two players|
the scheduler and the environment|where in each round the
scheduler proposes a time and a mode while the environment
chooses an allowable rate for that mode, and the state of the
system changes linearly in the direction of the rate vector.
The goal of the scheduler is to keep the state of the system
within a pre-specified safe set using a non-Zeno schedule,
while the goal of the environment is the opposite. Green
scheduling under uncertainty is a paradigmatic example of
BMS where a winning strategy of the scheduler corresponds
to a robust energy-optimal policy. We present an algorithm
to decide whether the scheduler has a winning strategy from
an arbitrary starting state, and give an algorithm to com-
pute such a winning strategy, if it exists. We show that the
schedulability problem for BMS is co-NP complete in general,
but for two variables it is in PTIME. We also study
the discrete schedulability problem where the environment
has only finitely many choices of rate vectors in each mode
and the scheduler can make decisions only at multiples of a
given clock period, and show it to be EXPTIME-complete.
Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC 2013, pages 243-252, ACM.
PDF © 2013 ACM.