Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Model Checking and Artificial Intelligence

MoChArt 2010: Model Checking and Artificial Intelligence pp 95–111Cite as

Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic

  • Conference paper

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

Abstract

Bounded model checking is a verification technique based on searching for counter-examples to the validity of the specification using an encoding to propositional sastisfiability. The paper identifies a number of inefficiencies in prior encodings for bounded model checking for a logic of knowledge and branching time. An alternate encoding is developed, and theoretical and experimental results are presented that show this leads to improved performance of bounded model checking for a range of examples.

Work supported by Australian Research Council Linkage Grant LP0882961 and Defence Research and Development Canada (Valcartier) contract W7701-082453. An abstract of this paper also appears in the AAMAS 2010 proceedings.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)

    Google Scholar 

  2. Burgess, J.P.: Logic and time. J. Symb. Log. 44(4), 566–582 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  3. Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. J. Cryptology 1(1), 65–75 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  4. van Ditmarsch, H.P., van der Hoek, W., van der Meyden, R., Ruan, J.: Model checking russian cards. Electronic Notes in Theoretical Computer Science 149(2), 105–123 (2005); Proc. of MoChart 2005

    Article  MATH  Google Scholar 

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

    MATH  Google Scholar 

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

  7. Kacprzak, M., Lomuscio, A., Niewiadomski, A., Penczek, W., Raimondi, F., Szreter, M.: Comparing BDD and SAT based techniques for model checking Chaum’s dining cryptographers protocol. Fundam. Inform. 72(1-3), 215–234 (2006)

    MathSciNet  MATH  Google Scholar 

  8. Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M., Wozna, B., Zbrzezny, A.: Verics 2007 - a model checker for knowledge and real-time. Fundam. Inform. 85(1-4), 313–328 (2008)

    MathSciNet  MATH  Google Scholar 

  9. Lamport, L., Shostak, R.E., Pease, M.C.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982)

    Article  MATH  Google Scholar 

  10. Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Luo, X., Su, K., Sattar, A., Reynolds, M.: Verification of multi-agent systems via bounded model checking. In: Sattar, A., Kang, B.-h. (eds.) AI 2006. LNCS (LNAI), vol. 4304, pp. 69–78. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. van der Meyden, R., Wong, K.: Complete axiomatizations for reasoning about knowledge and branching time. Studia Logica 75(1), 93–123 (2003)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  14. Penczek, W., Wozna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundam. Inform. 51(1-2), 135–156 (2002)

    MathSciNet  MATH  Google Scholar 

  15. Fabio Somenzi. CUDD: CU Decision Diagram Package, http://vlsi.colorado.edu/~fabio/CUDD

  16. Wozna, B.: ACTLS properties and bounded model checking. Fundam. Inform. 63(1), 65–87 (2004)

    MathSciNet  MATH  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The University of New South Wales, Australia

    Xiaowei Huang, Cheng Luo & Ron van der Meyden

Authors
  1. Xiaowei Huang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cheng Luo
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ron van der Meyden
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science and Engineering, University of New South Wales, 2052, Sydney, Australia

    Ron van der Meyden

  2. Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 79110, Freiburg, Germany

    Jan-Georg Smaus

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huang, X., Luo, C., van der Meyden, R. (2011). Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic. In: van der Meyden, R., Smaus, JG. (eds) Model Checking and Artificial Intelligence. MoChArt 2010. Lecture Notes in Computer Science(), vol 6572. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20674-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20674-0_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20673-3

  • Online ISBN: 978-3-642-20674-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation