A New Verification Procedure for Partially Clairvoyant Scheduling

  • K. Subramani
  • D. Desovski
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


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.


Execution Time Directed Cycle Constraint Network Dual Algorithm Standard Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [CGR96]
    Cherkassky, B.V., Goldberg, A.V., Radzik, T.: Shortest paths algorithms: Theory and experimental evaluation. Mathematical Programming 73, 129–174 (1996)MathSciNetzbMATHGoogle Scholar
  2. [GPS95]
    Gerber, R., Pugh, W., Saksena, M.: Parametric Dispatching of Hard Real-Time Tasks. IEEE Transactions on Computers (1995)Google Scholar
  3. [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
  4. [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
  5. [Sub03]
    Subramani, K.: An analysis of partially clairvoyant scheduling. Journal of Mathematical Modelling and Algorithms 2(2), 97–119 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  6. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • K. Subramani
    • 1
  • D. Desovski
    • 1
  1. 1.LDCSEEWest Virginia UniversityMorgantown

Personalised recommendations