Priority Scheduling of Distributed Systems Based on Model Checking

  • Ananda Basu
  • Saddek Bensalem
  • Doron Peled
  • Joseph Sifakis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


Priorities are used to control the execution of systems to meet given requirements for optimal use of resources, e.g., by using scheduling policies. For distributed systems, it is hard to find efficient implementations for priorities; because they express constraints on global states, their implementation may incur considerable overhead.

Our method is based on performing model checking for knowledge properties. It allows identifying where the local information of a process is sufficient to schedule the execution of a high priority transition. As a result of the model checking, the program is transformed to react upon the knowledge it has at each point. The transformed version has no priorities, and uses the gathered information and its knowledge to limit the enabledness of transitions so that it matches or approximates the original specification of priorities.


  1. 1.
    Basu, A., Bidinger, P., Bozga, M., Sifakis, J.: Distributed Semantics and Implementation for Systems with Interaction and Priority. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 116–133. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    Buckley, G.N., Silberschatz, A.: An Effective Implementation for the Generalized Input-Output Construct of CSP. ACM Transactions on Programming Language and Systems 5, 223–235 (1983)CrossRefzbMATHGoogle Scholar
  3. 3.
    Emerson, E.A., Clarke, E.M.: Characterizing Correctness Properties of Parallel Programs using Fixpoints. In: ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)Google Scholar
  4. 4.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  5. 5.
    Francez, N., Rodeh, M.: A Distributed Abstract Data Type Implemented by a Probabilistic Communication Scheme. In: 21st Annual Symposium on Foundations of Computer Science (FOCS), Syracuse, New York, pp. 373–379 (1980)Google Scholar
  6. 6.
    Halpern, J.Y., Zuck, L.D.: A little knowledge goes a long way: knowledge based derivation and correctness proof for a family of protocols. Journal of the ACM 39(3), 449–478 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Hoare, C.A.R.: Communicating Sequential Processes. Communication of the ACM 21, 666–677 (1978)CrossRefzbMATHGoogle Scholar
  8. 8.
    Gößler, G., Sifakis, J.: Priority Systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 443–466. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Manna, Z., Pnueli, A.: How to Cook a Temporal Proof System for Your Pet Language. In: POPL 1983, Austin, TX, pp. 141–154 (1983)Google Scholar
  10. 10.
    van der Meyden, R.: Common Knowledge and Update in Finite Environment. Information and Computation 140, 115–157 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Quielle, J.P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: 5th International Symposium on Programming, pp. 337–350 (1981)Google Scholar
  12. 12.
    Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM Journal on Control and Optimization 25(1), 206–230 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Yoo, T.S., Lafortune, S.: A general architecture for decentralized supervisory control of discrete-event systems. Discrete event dynamic systems, theory & applications 12(3), 335–377 (2002)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ananda Basu
    • 1
  • Saddek Bensalem
    • 1
  • Doron Peled
    • 2
  • Joseph Sifakis
    • 1
  1. 1.Centre Equation - VERIMAGGieresFrance
  2. 2.Department of Computer ScienceBar Ilan UniversityRamat GanIsrael

Personalised recommendations