Skip to main content
SpringerLink
Log in
Book cover

International Conference on Principles and Practice of Multi-Agent Systems

PRIMA 2020: PRIMA 2020: Principles and Practice of Multi-Agent Systems pp 259–280Cite as

A SMT-based Implementation for Safety Checking of Parameterized Multi-Agent Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 12568))

Abstract

We address the problem of verifying whether unwanted states, characterized as a given state formula, are reachable in a given parameterized multi-agent system (PMAS), i.e., whether the PMAS is unsafe. As the multi-agent system is parameterized, it only describes the finite set of possible agent templates, while the actual number of concrete agent instances for each template is unbounded and cannot be foreseen. However, as safety depends in general on the number of agent instances, the verification result must be correct irrespective of such a number. After having defined two distinct execution semantics of PMASs, in this paper we focus on an implemented approach for checking safety, which is composed of two steps. First, we have implemented a modeling tool, called SAFE, that allows to specify the agent templates in the PMAS and their possible interactions, and to automatically translate this model into a textual encoding of an array-based system (ABS). Second, we check safety via infinite-state model checking based on satisfiability modulo theories (SMT), by using the general purpose SMT-based model checker MCMT, which accepts ABS specifications as input. We show the correctness guarantees of this approach by relying on the theory of ABSs. Finally we discuss how this approach lends itself to richer parameterized and data-aware MAS settings beyond the state-of-the-art solutions in the literature, using SMT-based results now available thanks to this work.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Notes

  1. 1.

    These examples are available at: http://safeswarms.club/page/mcmt/exZb with Z=1..4.

  2. 2.

    These examples are available at: http://safeswarms.club/page/mcmt/exZ with Z=1..3.

  3. 3.

    To replicate these experiments, it is sufficient to disable the template alternation through the GUI.

  4. 4.

    The example, modeled via SAFE, is publicly available at: http://safeswarms.club/page/mcmt/rooms.

References

  1. MCMT: Model Checker Modulo Theories. http://users.mat.unimi.it/users/ghilardi/mcmt. Accessed 1 Sep 2020

  2. SAFE: the swarm safety detector. http://www.safeswarms.club. Accessed 1 Sep 2020

  3. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS, pp. 313–321. IEEE (1996)

    Google Scholar 

  4. Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014). https://doi.org/10.1007/s10703-014-0209-9

    Article  MATH  Google Scholar 

  5. Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinite-state systems. Fund. Inform. 150(1), 1–24 (2017)

    MathSciNet  Google Scholar 

  6. Alechina, N., Brázdil, T., De Giacomo, G., Felli, P., Logan, B., Vardi, M.Y.: Unbounded orchestrations of transducers for manufacturing. In: Proceedings of AAAI, pp. 2646–2653 (2019)

    Google Scholar 

  7. Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305–343 (2018)

    Google Scholar 

  8. Bloem, R., Jacobs, S., Khalimov, A.: Decidability of Parameterized Verification. Morgan & Claypool Publishers, San Rafael (2015)

    Google Scholar 

  9. Bulling, N., Goranko, V., Jamroga, W.: Logics for reasoning about strategic abilities in multi-player games. In: Models of Strategic Reasoning - Logics, Games, and Communities, pp. 93–136 (2015)

    Google Scholar 

  10. Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal modeling and SMT-based parameterized verification of data-aware BPMN. In: Hildebrandt, T., van Dongen, B.F., Röglinger, M., Mendling, J. (eds.) BPM 2019. LNCS, vol. 11675, pp. 157–175. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-26619-6_12

    Chapter  Google Scholar 

  11. Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: From model completeness to verification of data aware processes. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.-Y., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 212–239. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22102-7_10

    Chapter  MATH  Google Scholar 

  12. Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 142–160. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_9

    Chapter  Google Scholar 

  13. Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: SMT-based verification of data-aware processes: a model-theoretic approach. Math. Struct. Comp. Sci. 30(3), 271–313 (2020)

    Article  MathSciNet  Google Scholar 

  14. Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. Handbook of Model Checking, pp. 921–962. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_27

    Chapter  Google Scholar 

  15. Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: Proceedings of FMCAD, pp. 61–68. IEEE (2013)

    Google Scholar 

  16. Condurache, R., De Masellis, R., Goranko, V.: Dynamic multi-agent systems: conceptual framework, automata-based modelling and verification. In: Baldoni, M., Dastani, M., Liao, B., Sakurai, Y., Zalila Wenkstern, R. (eds.) PRIMA 2019. LNCS (LNAI), vol. 11873, pp. 106–122. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33792-6_7

    Chapter  Google Scholar 

  17. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236–254. Springer, Heidelberg (2000). https://doi.org/10.1007/10721959_19

    Chapter  Google Scholar 

  18. Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: Proceedings of LICS, pp. 361–370. IEEE (2003)

    Google Scholar 

  19. Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)

    Article  MathSciNet  Google Scholar 

  20. Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Inf. 54(2), 191–215 (2017)

    Article  MathSciNet  Google Scholar 

  21. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theoret. Comput. Sci. 256(1), 63–92 (2001)

    Article  MathSciNet  Google Scholar 

  22. Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri nets with parameterised data. In: Fahland, D., Ghidini, C., Becker, J., Dumas, M. (eds.) BPM 2020. LNCS, vol. 12168, pp. 55–74. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58666-9_4

    Chapter  Google Scholar 

  23. Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Proceedings of IJCAR, pp. 67–82 (2008)

    Google Scholar 

  24. Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4), 1–48 (2010)

    Google Scholar 

  25. Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_3

    Chapter  Google Scholar 

  26. Ghilardi, S., Ranise, S., Valsecchi, T.: Light-weight SMT-based model checking. Electron. Notes Theor. Comput. Sci. 250(2), 85–102 (2009)

    Article  Google Scholar 

  27. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Proceedings of FMCAD, pp. 201–209. IEEE (2013)

    Google Scholar 

  28. Kouvaros, P., Lomuscio, A.: Parameterised verification for multi-agent systems. Artif. Intell. 234, 152–189 (2016)

    Article  MathSciNet  Google Scholar 

  29. Kouvaros, P., Lomuscio, A.: Parameterised verification of infinite state multi-agent systems via predicate abstraction. In: Proceedings of AAAI, pp. 3013–3020 (2017)

    Google Scholar 

  30. Kouvaros, P., Lomuscio, A., Pirovano, E., Punchihewa, H.: Formal verification of open multi-agent systems. In: Proceedings of AAMAS, pp. 179–187 (2019)

    Google Scholar 

  31. Li, Y., Deutsch, A., Vianu, V.: VERIFAS: a practical verifier for artifact systems. In: Proceedings of VLDB, pp. 283–296 (2017)

    Google Scholar 

  32. Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1, infty)- counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_9

    Chapter  Google Scholar 

Download references

Acknowledgements

This work was partially supported by the Unibz RTD project SMARTEST.

Author information

Authors and Affiliations

  1. Free University of Bozen-Bolzano, Bolzano, Italy

    Paolo Felli, Alessandro Gianola & Marco Montali

Authors
  1. Paolo Felli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alessandro Gianola
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marco Montali
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alessandro Gianola .

Editor information

Editors and Affiliations

  1. Nagoya Institute of Technology, Nagoya, Japan

    Takahiro Uchiya

  2. University of Tasmania, Tasmania, TAS, Australia

    Quan Bai

  3. University of Alcalá, Alcala de Henares, Spain

    Iván Marsá Maestre

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

Felli, P., Gianola, A., Montali, M. (2021). A SMT-based Implementation for Safety Checking of Parameterized Multi-Agent Systems. In: Uchiya, T., Bai, Q., Marsá Maestre, I. (eds) PRIMA 2020: Principles and Practice of Multi-Agent Systems. PRIMA 2020. Lecture Notes in Computer Science(), vol 12568. Springer, Cham. https://doi.org/10.1007/978-3-030-69322-0_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-69322-0_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-69321-3

  • Online ISBN: 978-3-030-69322-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation