We are excited to announce that the repository will soon undergo an upgrade, featuring a new look and feel along with several enhanced features to improve your experience. Please be on the lookout for further updates and announcements regarding the launch date. We appreciate your support and look forward to unveiling the improved platform soon.
dc.contributor.author | Timm, Nils![]() |
|
dc.contributor.author | Botha, Josua![]() |
|
dc.contributor.author | Jordaan, Steve![]() |
|
dc.date.accessioned | 2024-02-29T09:29:37Z | |
dc.date.available | 2024-02-29T09:29:37Z | |
dc.date.issued | 2023-06 | |
dc.description.abstract | We present techniques for verifying strategic abilities of multi-agent systems via SAT-based and Max-SAT-based bounded model checking. In our approach we focus on systems of agents that pursue goals with regard to the allocation of shared resources. One of the problems to be solved is to determine whether a coalition of agents has a joint strategy that guarantees the achievement of all resource goals, irrespective of how the opposing agents in the system act. Our approach does not only decide whether such a winning strategy exists, but also synthesises the strategy. Winning strategies are particularly useful in the presence of an opposition because they guarantee that each agent of the coalition will achieve its individual goal, no matter how the opposition behaves. However, for the grand coalition consisting of all agents in the system, following a winning strategy may involve an inefficient use of resources. A winning strategy will only ensure that each agent will reach its goal at some time. But in practical resource allocation problems it may be of additional importance that once-off resource goals will be achieved as early as possible or that repetitive goals will be achieved as frequent as possible. We present an extended technique that synthesises strategies that are collectively optimal with regard to such quantitative performance criteria. A collectively optimal strategy allows to optimise the overall system performance but it may favour certain agents over others. In competitive scenarios a Nash equilibrium strategy may be a more adequate solution. It guarantees that no agent can improve its individual performance by unilaterally deviating from the strategy. We developed an algorithm that initially generates a collectively optimal strategy and then iteratively alternates this strategy until the strategy becomes a Nash equilibrium or a cycle of non-equilibrium strategies is detected. Our approach is based on a propositional logic encoding of strategy synthesis problems. We reduce the synthesis of winning strategies to the Boolean satisfiability problem and the synthesis of optimal and Nash equilibrium strategies to the maximum satisfiability problem. Hence, efficient SAT- and Max-SAT solvers can be employed to solve the encoded strategy synthesis problems | en_US |
dc.description.department | Computer Science | en_US |
dc.description.librarian | am2024 | en_US |
dc.description.sdg | SDG-09: Industry, innovation and infrastructure | en_US |
dc.description.uri | http://www.elsevier.com/locate/scico | en_US |
dc.identifier.citation | Timm, N., Botha, J., Jordaan, S. 2023, 'Max-SAT-based synthesis of optimal and Nash equilibrium strategies for multi-agent systems', Science of Computer Programming, vol. 228, art. 102946, pp. 1-28. https://DOI.org/10.1016/j.scico.2023.102946. | en_US |
dc.identifier.issn | 0167-6423 | |
dc.identifier.other | 10.1016/j.scico.2023.102946 | |
dc.identifier.uri | http://hdl.handle.net/2263/95004 | |
dc.language.iso | en | en_US |
dc.publisher | Elsevier | en_US |
dc.rights | © 2023 The Author(s). This is an open access article under the CC BY license. | en_US |
dc.subject | Bounded model checking | en_US |
dc.subject | Multi-agent systems | en_US |
dc.subject | Strategy synthesis | en_US |
dc.subject | Max-SAT-based optimisation | en_US |
dc.subject | Nash equilibrium | en_US |
dc.subject | SDG-09: Industry, innovation and infrastructure | en_US |
dc.title | Max-SAT-based synthesis of optimal and Nash equilibrium strategies for multi-agent systems | en_US |
dc.type | Article | en_US |