@article{8788,
  abstract     = {We consider a real-time setting where an environment releases sequences of firm-deadline tasks, and an online scheduler chooses on-the-fly the ones to execute on a single processor so as to maximize cumulated utility. The competitive ratio is a well-known performance measure for the scheduler: it gives the worst-case ratio, among all possible choices for the environment, of the cumulated utility of the online scheduler versus an offline scheduler that knows these choices in advance. Traditionally, competitive analysis is performed by hand, while automated techniques are rare and only handle static environments with independent tasks. We present a quantitative-verification framework for precedence-aware competitive analysis, where task releases may depend on preceding scheduling choices, i.e., the environment can respond to scheduling decisions dynamically . We consider two general classes of precedences: 1) follower precedences force the release of a dependent task upon the completion of a set of precursor tasks, while and 2) pairing precedences modify the characteristics of a dependent task provided the completion of a set of precursor tasks. Precedences make competitive analysis challenging, as the online and offline schedulers operate on diverging sequences. We make a formal presentation of our framework, and use a GPU-based implementation to analyze ten well-known schedulers on precedence-based application examples taken from the existing literature: 1) a handshake protocol (HP); 2) network packet-switching; 3) query scheduling (QS); and 4) a sporadic-interrupt setting. Our experimental results show that precedences and task parameters can vary drastically the best scheduler. Our framework thus supports application designers in choosing the best scheduler among a given set automatically.},
  author       = {Pavlogiannis, Andreas and Schaumberger, Nico and Schmid, Ulrich and Chatterjee, Krishnendu},
  issn         = {19374151},
  journal      = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
  number       = {11},
  pages        = {3981--3992},
  publisher    = {IEEE},
  title        = {{Precedence-aware automated competitive analysis of real-time scheduling}},
  doi          = {10.1109/TCAD.2020.3012803},
  volume       = {39},
  year         = {2020},
}

@article{8790,
  abstract     = {Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.},
  author       = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
  issn         = {19374151},
  journal      = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
  number       = {11},
  pages        = {4018--4029},
  publisher    = {IEEE},
  title        = {{Reachability analysis of linear hybrid systems via block decomposition}},
  doi          = {10.1109/TCAD.2020.3012859},
  volume       = {39},
  year         = {2020},
}