Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2015: Formal Methods and Software Engineering pp 84–99Cite as

A 3-Valued Contraction Model Checking Game: Deciding on the World of Partial Information

  • Conference paper
  • First Online:

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

Abstract

In this work we address the problem of model checking a desired property specified in Computation Tree Logic (CTL) in the presence of partial information. The Kripke Modal Transition System (KMTS) is used for modelling due its capacity to represent indefinitions explicitly which enables a KMTS interpretation as a set of Kripke structures. In this interpretation a specific model checking algorithm is required that can return one of the three possible values: true when all Kripke models of the set satisfy the property, false when no Kripke models of the set satisfy the property and indefinite when some models satisfy and others do not. To the best of our knowledge the literature lacks a KMTS model checking algorithm that fits this interpretation and in this paper we present an algorithm based on a game approach called a Contraction Model Checking algorithm for this purpose.

J.S. Ribeiro—This author is supported by the grant # 4576/2014, Bahia Research Foundation (FAPESB).

A. Andrade—This author is supported by the grant # 447178/2014-8, Brazilian Research Council (CNPq).

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.

    Although the CTL semantics consider Kripke structures with total relation transition, such a requirement can be released and we assume a Kripke structure with a partial transition relation instead.

References

  1. Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT press, Cambridge (1999)

    Google Scholar 

  4. Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Grumberg, O., Lange, M., Leucker, M., Shoham, S.: When not losing is better than winning: Abstraction and refinement for the full \(\mu \)-calculus. Inf. Comput. 205(8), 1130–1148 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  6. Guerra, P.T., Andrade, A., Wassermann, R.: Toward the revision of CTL models through Kripke modal transition systems. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 115–130. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Huth, M.: Model checking modal transition systems using Kripke structures. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 302–316. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  9. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)

    Book  MATH  Google Scholar 

  10. Kleene, S.C., de Bruijn, N., de Groot, J., Zaanen, A.C.: Introduction to Metamathematics. Van Nostrand, New York (1952)

    Google Scholar 

  11. Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Logic 9(1), 1 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  12. Wehrheim, H.: Bounded model checking for partial Kripke structures. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 380–394. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Distributed Systems Laboratory (LaSiD) Computer Science Department – Mathematics Institute, Federal University of Bahia, Salvador, Bahia, Brazil

    Jandson S. Ribeiro & Aline Andrade

Authors
  1. Jandson S. Ribeiro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aline Andrade
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jandson S. Ribeiro .

Editor information

Editors and Affiliations

  1. Electronics and Computer Science, University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Université Paris-Sud, Orsay, France

    Sylvain Conchon

  3. Université Paris-Sud, Orsay, France

    Fatiha Zaïdi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Ribeiro, J.S., Andrade, A. (2015). A 3-Valued Contraction Model Checking Game: Deciding on the World of Partial Information. In: Butler, M., Conchon, S., Zaïdi, F. (eds) Formal Methods and Software Engineering. ICFEM 2015. Lecture Notes in Computer Science(), vol 9407. Springer, Cham. https://doi.org/10.1007/978-3-319-25423-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25423-4_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25422-7

  • Online ISBN: 978-3-319-25423-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation