Skip to main content
SpringerLink
Log in

Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation

  • Conference paper
  • First Online:
Formal Methods: Foundations and Applications (SBMF 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13130))

Included in the following conference series:

Abstract

We present a technique for verifying strategic abilities of multi-agent systems via 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. The problem 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 strategy exists, but also synthesises the strategy. The technique is based on a propositional logic encoding of the model checking problem. The encoding is satisfiable if and only if some specified coalition of agents has a strategy to reach a resource allocation goal. Each satisfying truth assignment of the encoding characterises a successful strategy.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM (JACM) 49(5), 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  2. Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028774

    Chapter  Google Scholar 

  3. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  4. Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. 4(2–4), 75–97 (2008)

    MATH  Google Scholar 

  5. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Handbook of Satisfiability, vol. 185, no. 99, pp. 457–481 (2009)

    Google Scholar 

  6. Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. STTT 2(4), 410–425 (2000). https://doi.org/10.1007/s100090050046

    Article  MATH  Google Scholar 

  7. Cohen, M., Dam, M., Lomuscio, A., Qu, H.: A symmetry reduction technique for model checking temporal-epistemic logic. In: IJCAI (2009)

    Google Scholar 

  8. De Masellis, R., Goranko, V., Gruner, S., Timm, N.: Generalising the dining philosophers problem: competitive dynamic resource allocation in multi-agent systems. In: Slavkovik, M. (ed.) EUMAS 2018. LNCS (LNAI), vol. 11450, pp. 30–47. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-14174-5_3

    Chapter  Google Scholar 

  9. Jamroga, W., Penczek, W., Sidoruk, T., Dembiński, P., Mazurkiewicz, A.: Towards partial order reductions for strategic ability. JAIR 68, 817–850 (2020)

    Article  MathSciNet  Google Scholar 

  10. Kacprzak, M., Penczek, W.: Unbounded model checking for alternating-time temporal logic. In: CAV, pp. 646–653. IEEE (2004)

    Google Scholar 

  11. Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 557–572. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_44

    Chapter  Google Scholar 

  12. Lomuscio, A., Penczek, W., Woźna, B.: Bounded model checking for knowledge and real time. Artif. Intell. 171(16–17), 1011–1038 (2007)

    Article  MathSciNet  Google Scholar 

  13. Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. STTT 19(1), 9–30 (2017). https://doi.org/10.1007/s10009-015-0378-x

    Article  Google Scholar 

  14. Luo, X., Su, K., Sattar, A., Reynolds, M.: Verification of multi-agent systems via bounded model checking. In: Sattar, A., Kang, B. (eds.) AI 2006. LNCS (LNAI), vol. 4304, pp. 69–78. Springer, Heidelberg (2006). https://doi.org/10.1007/11941439_11

    Chapter  Google Scholar 

  15. Pilecki, J., Bednarczyk, M.A., Jamroga, W.: SMC: synthesis of uniform strategies and verification of strategic ability for multi-agent systems. J. Log. Comput. 27(7), 1871–1895 (2017)

    MathSciNet  MATH  Google Scholar 

  16. Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. J. Appl. Log. 5(2), 235–251 (2007)

    Article  MathSciNet  Google Scholar 

  17. Schewe, S.: ATL* satisfiability is 2EXPTIME-complete. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 373–385. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_31

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Pretoria, Pretoria, South Africa

    Nils Timm & Josua Botha

Authors
  1. Nils Timm
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Josua Botha
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nils Timm .

Editor information

Editors and Affiliations

  1. Departamento de Ciência da Computação, Universidade Federal de Minas Gerais, Belo Horizonte, Minas Gerais, Brazil

    Sérgio Campos

  2. College of Information and Computer Sciences, University of Massachusetts, Amherst, MA, USA

    Marius Minea

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Timm, N., Botha, J. (2021). Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation. In: Campos, S., Minea, M. (eds) Formal Methods: Foundations and Applications. SBMF 2021. Lecture Notes in Computer Science(), vol 13130. Springer, Cham. https://doi.org/10.1007/978-3-030-92137-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-92137-8_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-92136-1

  • Online ISBN: 978-3-030-92137-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation