Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Generalising the Dining Philosophers Problem: Competitive Dynamic Resource Allocation in Multi-agent Systems
Stockholm University, Faculty of Humanities, Department of Philosophy.ORCID iD: 0000-0003-2540-7395
Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
2019 (English)In: Multi-Agent Systems: 16th European Conference, EUMAS 2018, Bergen, Norway, December 6–7, 2018, Revised Selected Papers / [ed] Marija Slavkovik, Springer, 2019, p. 30-47Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2019. p. 30-47
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11450
Keywords [en]
Dining philosophers games, Dynamic resource allocation, Alternating time temporal logic ATL, Symbolic model checking
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:su:diva-164090DOI: 10.1007/978-3-030-14174-5_3ISBN: 978-3-030-14173-8 (print)ISBN: 978-3-030-14174-5 (electronic)OAI: oai:DiVA.org:su-164090DiVA, id: diva2:1280515
Conference
16th European Conference, EUMAS 2018, Bergen, Norway, December 6–7, 2018
Funder
Swedish Research Council, 2015-04388Available from: 2019-01-19 Created: 2019-01-19 Last updated: 2019-04-10Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
De Masellis, RiccardoGoranko, Valentin
By organisation
Department of Philosophy
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 56 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf