Generalising the Dining Philosophers Problem: Competitive Dynamic Resource Allocation in Multi-agent Systems

  • Riccardo De MasellisEmail author
  • Valentin Goranko
  • Stefan Gruner
  • Nils Timm
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11450)


We consider a new generalisation of the Dining Philosophers problem with a set of agents and a set of resource units which can be accessed by them according to a fixed graph of accessibility between agents and resources. Each agent needs to accumulate a certain (fixed for the agent) number of accessible resource units to accomplish its task, and once it is accomplished the agent releases all resources and starts accumulating them again. All this happens in succession of discrete ‘rounds’ and yields a concurrent game model of ‘dynamic resource allocation’. We use the Alternating time Temporal Logic (ATL) to specify important properties, such as goal achievability, fairness, deadlock, starvation, etc. These can be formally verified using the efficient model checking algorithm for ATL. However, the sizes of the resulting explicit concurrent game models are generally exponential both in the number of resources and the number of agents, which makes the ATL model checking procedure generally intractable on such models, especially when the number of resources is large. That is why we also develop an abstract representation of the dynamic resource allocation models and develop a symbolic version of the model checking procedure for ATL. That symbolic procedure reduces the time complexity of model checking to polynomial in the number of resources, though it can take a worst-case double exponential time in the number of agents.


Dining philosophers games Dynamic resource allocation Alternating time temporal logic ATL Symbolic model checking 



The work of Valentin Goranko and Riccardo De Masellis was supported by a research grant 2015-04388 of the Swedish Research Council, which also partly funded a working visit of Nils Timm to Stockholm. Valentin Goranko was also partly supported by a visiting professorship grant by the University of Pretoria.


  1. 1.
    Alechina, N., Logan, B., Hoang Nga, N., Rakib, A.: Resource-bounded alternating-time temporal logic. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems: Volume 1, AAMAS 2010, vol. 1, pp. 481–488. International Foundation for Autonomous Agents and Multiagent Systems, Richland (2010)Google Scholar
  2. 2.
    Alechina, N., Logan, B., Hoang Nga, N., Raimondi, F.: Symbolic model checking for one-resource RB\(\pm \)ATL. In: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI 2015, pp. 1069–1075. AAAI Press (2015)Google Scholar
  3. 3.
    Alechina, N., Logan, B., Hoang Nga, N., Raimondi, F., Mostarda, L.: Symbolic model-checking for resource-bounded ATL. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, pp. 1809–1810. International Foundation for Autonomous Agents and Multiagent Systems, Richland (2015)Google Scholar
  4. 4.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Bhargava, D., Vyas, S.: Agent based solution for dining philosophers problem. In: 2017 International Conference on Infocom Technologies and Unmanned Systems (Trends and Future Directions), ICTUS, pp. 563–567, December 2017Google Scholar
  6. 6.
    Chandy, K.M., Misra, J.: The drinking philosophers problem. ACM Trans. Program. Lang. Syst. 6(4), 632–646 (1984)CrossRefGoogle Scholar
  7. 7.
    Chevaleyre, Y., et al.: Issues in multiagent resource allocation. Informatica 30, 3–31 (2006)zbMATHGoogle Scholar
  8. 8.
    Choppella, V., Kasturi, V., Sanjeev, A.: Generalised dining philosophers as feedback control. CoRR abs/1805.02010 (2018)Google Scholar
  9. 9.
    Datta, A.K., Gradinariu, M., Raynal, M.: Stabilizing mobile philosophers. Inf. Process. Lett. 95(1), 299–306 (2005)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2016).
  11. 11.
    Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1(2), 115–138 (1971)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Herescu, O.M., Palamidessi, C.: On the generalized dining philosophers problem. In: Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed Computing, PODC 2001, pp. 81–89. ACM, New York (2001)Google Scholar
  13. 13.
    Hopcroft, J.E., Karp, R.M.: An n\({}^{\text{5/2 }}\) algorithm for maximum matchings in bipartite graphs. SIAM J. Comput. 2(4), 225–231 (1973)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Papatriantafilou, M.: On distributed resource handling: dining, drinking and mobile philosophers. In: Proceedings of the First International Conference on Principles of Distributed Systems, OPODIS, pp. 293–308 (1997)Google Scholar
  15. 15.
    Sidhu, D.P., Pollack, R.H.: A robust distributed solution to the generalized Dining Philosophers problem. In: 1984 IEEE First International Conference on Data Engineering, pp. 483–489, April 1984Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Riccardo De Masellis
    • 1
    Email author
  • Valentin Goranko
    • 1
    • 2
  • Stefan Gruner
    • 3
  • Nils Timm
    • 3
  1. 1.Stockholm UniversityStockholmSweden
  2. 2.University of JohannesburgJohannesburgSouth Africa
  3. 3.University of PretoriaPretoriaSouth Africa

Personalised recommendations