A New Verification Procedure for Partially Clairvoyant Scheduling
In this paper, we describe a new algorithm for the problem of checking whether a real-time system has a Partially Clairvoyant schedule (PCS). Existing algorithms for the PCS problem are predicated on sequential quantifier elimination, i.e., the innermost quantifier is eliminated first, followed by the next one and so on. Our technique is radically different in that the quantifiers in the schedulability specification are eliminated in arbitrary fashion. We demonstrate the usefulness of this technique by achieving significant performance improvement over a wide range of inputs. Additionally, the analysis developed for the new procedure may find applications in domains such as finite model theory and classical logic.
KeywordsExecution Time Directed Cycle Constraint Network Dual Algorithm Standard Constraint
Unable to display preview. Download preview PDF.
- [GPS95]Gerber, R., Pugh, W., Saksena, M.: Parametric Dispatching of Hard Real-Time Tasks. IEEE Transactions on Computers (1995)Google Scholar
- [LSW03]Larsen, K.G., Steffen, B., Weise, C.: Continuous modelling of real time and hybrid systems. Technical report, Aalborg Universitet, BRICS Technical Report (2003)Google Scholar
- [MSC+97]Muscettola, N., Smith, B., Chien, S., Fry, C., Rabideau, G., Rajan, K., Yan, D.: In-board planning for autonomous spacecraft. In: The Fourth International Symposium on Artificial Intelligence, Robotics, and Automation for Space (i-SAIRAS) (July 1997)Google Scholar
- [Wei97]Weispfenning, V.: Simulation and optimization by quantifier elimination. Journal of Symbolic Computation 24(2), 189–208 (1997); Applications of quantifier elimination (Albuquerque, NM) (1995)Google Scholar