Safe schedulability of bounded-rate multi-mode systems
Safe schedulability of bounded-rate multi-mode systems
复制标题
有界速率多模系统的安全可调度性
DOI：
10.1145/2461328.2461366
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Ashutosh Trivedi
中科院分区：
文献类型：
--
作者：
R. Alur;Vojtěch Forejt;Salar Moarref;Ashutosh Trivedi
有界速率多模式系统（Bounded-rate multi-mode systems，BMS）是一种能够在有限个模式之间自由切换的混合系统，其动态特性由有限个具有模式相关速率的实值变量来描述，这些速率可以在给定的有界集合内变化。BMS的可调度性问题被定义为两个玩家之间的无限回合游戏-调度程序和环境-在每一轮中，调度程序提出一个时间和一个模式，而环境选择一个允许的速率为该模式，系统的状态沿速率向量的方向线性变化。调度器的目标是使用非Zeno调度将系统的状态保持在预先指定的安全集内，而环境的目标则相反。不确定性下的绿色调度是BMS的一个典型例子，其中调度器的获胜策略对应于鲁棒的能量最优策略。我们提出了一种算法来决定调度器是否具有来自任意开始状态的获胜策略，并且给出了一种算法来计算这样的获胜策略（如果存在的话）。我们表明，BMS的可验证性问题是co-NP完全的一般情况下，但对于两个变量，它是在PTIME。我们还研究了离散的可扩展性问题，其中的环境中只有100多种选择的速率向量在每种模式和调度程序只能在一个给定的时钟周期的倍数作出决定，并显示它是EXPTIME完成。
Bounded-rate multi-mode systems (BMS) are hybrid systems 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 compute 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.
恒定速率多模系统的优化调度
DOI：
10.1145/2185632.2185647
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Alur R
通讯作者：
Alur R