Skip to main content
SpringerLink
Log in

Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge

  • Conference paper
Book cover 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

The paper deals with symbolic approaches to bounded model checking (BMC) for Linear Time Temporal Logic extended with the epistemic component (LTLK), interpreted over Interleaved Interpreted Systems. Two translations of BMC for LTLK to SAT and to operations on BDDs are presented. The translations have been implemented, tested, and compared with each other as well as with another tool on several benchmarks for MAS. Our experimental results reveal advantages and disadvantages of SAT- versus BDD-based BMC for LTLK.

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

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. Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Highly Dependable Software. Advances in Computers, vol. 58. Academic Press (2003)

    Google Scholar 

  2. Bordini, R.H., Fisher, M., Pardavila, C., Visser, W., Wooldridge, M.: Model Checking Multi-Agent Programs with CASP. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 110–113. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. Cabodi, G., Camurati, P., Quer, S.: Can BDD compete with SAT solvers on bounded model checking? In: DAC 2002, pp. 117–122 (2002)

    Google Scholar 

  4. Clarke, E., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  5. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)

    Google Scholar 

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

    MATH  Google Scholar 

  7. Gammie, P., van der Meyden, R.: MCK: Model Checking the Logic of Knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. van der Hoek, W., Wooldridge, M.: Model Checking Knowledge and Time. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 95–111. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Huang, X., Luo, C., van der Meyden, R.: Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt 2010. LNCS (LNAI), vol. 6572, pp. 95–111. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. 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 

  11. Kacprzak, M., Nabiałek, W., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS 2007 - a Model Checker for Knowledge and Real-Time. Fundamenta Informaticae 85(1-4), 313–328 (2008)

    MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  13. van der Meyden, R., Shilov, N.V.: Model Checking Knowledge and Time in Systems with Perfect Recall. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003)

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, PAS, Poland

    Artur Męski

  2. University of Natural Sciences and Humanities, II, Poland

    Artur Męski, Wojciech Penczek & Maciej Szreter

  3. FMCS, University of Łódź, Poland

    Wojciech Penczek

  4. IMCS, Jan Długosz University, Poland

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

Authors
  1. Artur Męski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wojciech Penczek
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maciej Szreter
    View author publications

    You can also search for this author in PubMed Google Scholar

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

    You can also search for this author in PubMed Google Scholar

  5. 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

Męski, A., Penczek, W., Szreter, M., Woźna-Szcześniak, B., Zbrzezny, A. (2012). Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge. 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_56

Download citation

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

  • 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