Skip to main content
SpringerLink
Log in

SAT-Based Bounded Model Checking for Deontic Interleaved Interpreted Systems

  • Conference paper
Agent and Multi-Agent Systems. Technologies and Applications (KES-AMSTA 2012)

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

Abstract

We propose a bounded model checking (BMC) method for the verification of multi-agent systems’ (MASs). The MASs are modelled by deontic interleaved interpreted systems, and specifications are expressed in the logic \(\sc{RTECTLKD}\). The verification approach is based on the state of the art solutions to BMC, one of the mainstream approaches in verification of reactive systems. We test our results on a typical communication scenario: train controller problem with faults.

Partly supported by National Science Center under the grant No. 2011/01/B/ST6/05317.

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 39.99
Price excludes VAT (USA)
  • Available as 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic Reachability Analysis Based on SAT-Solvers. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 411–425. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  3. Sistla, A.P., Emerson, E.A., Mok, A.K., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Systems 4(4), 331–352 (1992)

    Article  Google Scholar 

  4. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  5. Jones, A., Lomuscio, A.: A BDD-based BMC approach for the verification of multi-agent systems. In: CS&P 2009, vol. 1, pp. 253–264. Warsaw University (2009)

    Google Scholar 

  6. Kacprzak, M., Lomuscio, A., Łasica, T., Penczek, W., Szreter, M.: Verifying Multi-agent Systems via Unbounded Model Checking. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A. (eds.) FAABS 2004. LNCS (LNAI), vol. 3228, pp. 189–212. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Lomuscio, A., Penczek, W., Qu, H.: Partial order reduction for model checking interleaved multi-agent systems. In: AAMAS 2010, pp. 659–666. IFAAMAS Press (2010)

    Google Scholar 

  8. Lomuscio, A., Sergot, M.: Deontic interpreted systems. Studia Logica 75(1), 63–92 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  9. Męski, A., Penczek, W., Szreter, M.: Bounded model checking linear time and knowledge using decision diagrams. In: CS&P 2011, pp. 363–375. Biaystok University of Technology (2011)

    Google Scholar 

  10. Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: AAMAS 2003, pp. 209–216. ACM (2003)

    Google Scholar 

  11. Penczek, W., Woźna-Szcześniak, B., Zbrzezny, A.: Towards SAT-based BMC for LTLK over interleaved interpreted systems. In: CS&P 2011, pp. 565–576. Białystok University of Technology (2011)

    Google Scholar 

  12. Raimondi, F., Lomuscio, A.: Symbolic Model Checking of Deontic Interpreted Systems via OBDDs. In: Lomuscio, A., Nute, D. (eds.) DEON 2004. LNCS (LNAI), vol. 3065, pp. 228–242. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic 5(2), 235–251 (2005)

    Article  MathSciNet  Google Scholar 

  14. Wooldridge, M.: An introduction to multi-agent systems. John Wiley, England (2002)

    Google Scholar 

  15. Woźna, B., Lomuscio, A., Penczek, W.: Bounded model checking for deontic interpreted systems. In: LCMAS 2004. ENTCS, vol. 126, pp. 93–114. Elsevier (2005)

    Google Scholar 

  16. Woźna-Szcześniak, B., Zbrzezny, A., Zbrzezny, A.: The BMC Method for the Existential Part of RTCTLK and Interleaved Interpreted Systems. In: Antunes, L., Pinto, H.S. (eds.) EPIA 2011. LNCS (LNAI), vol. 7026, pp. 551–565. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1-4), 513–531 (2008)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IMCS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200, Czȩstochowa, Poland

    Bożena Woźna-Szcześniak & Andrzej Zbrzezny

Authors
  1. Bożena Woźna-Szcześniak
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrzej Zbrzezny
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Electrical Engineering and Computing, University of Zagreb, Unska 3, 10000, Zagreb, Croatia

    Gordan Jezic  & Mario Kusek  & 

  2. Institute of Informatics (I-32), Division of Knowledge Management Systems, Wroclaw University of Technology, Str. Wyb. Wyspianskiego 27, 50-370, Wroclaw, Poland

    Ngoc-Thanh Nguyen

  3. KES International, Shoreham-by-sea, P.O. Box 2115, BN43 9AF, UK

    Robert J. Howlett

  4. School of Electrical and Information Engineering, University of South Australia, Mawson Lakes Campus, 5095, Adelaide, SA, Australia

    Lakhmi C. Jain

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Woźna-Szcześniak, B., Zbrzezny, A. (2012). SAT-Based Bounded Model Checking for Deontic Interleaved Interpreted Systems. In: Jezic, G., Kusek, M., Nguyen, NT., Howlett, R.J., Jain, L.C. (eds) Agent and Multi-Agent Systems. Technologies and Applications. KES-AMSTA 2012. Lecture Notes in Computer Science(), vol 7327. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30947-2_54

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-30947-2_54

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-30946-5

  • Online ISBN: 978-3-642-30947-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation