Skip to main content
SpringerLink
Log in

Foundations of Inconsistency-Tolerant Model Checking: Logics, Translations, and Examples

  • Conference paper
  • First Online:
Agents and Artificial Intelligence (ICAART 2018)

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

Included in the following conference series:

  • 903 Accesses

Abstract

We develop logics and translations for inconsistency-tolerant model checking that can be used to verify systems having inconsistencies. Paraconsistent linear-time temporal logic (pLTL), paraconsistent computation tree logic (pCTL), and paraconsistent full computation tree logic (pCTL\(^*\)) are introduced. These are extensions of standard linear-time temporal logic (LTL), standard computation tree logic (CTL), and standard full computation tree logic (CTL\(^*\)), respectively. These novel logics can be applied when handling inconsistency-tolerant temporal reasoning. They are also regarded as four-valued temporal logics that extend Belnap and Dunn’s four-valued logic. Translations from pLTL into LTL, pCTL into CTL, and pCTL\(^*\) into CTL\(^*\), are defined, and these are used to prove the theorems for embedding pLTL into LTL, pCTL into CTL, and pCTL\(^*\) into CTL\(^*\). These embedding theorems allow the standard LTL-, CTL-, and CTL\(^*\)-based model checking algorithms to be used for verifying inconsistent systems that are modeled and specified by pLTL, pCTL, and pCTL\(^*\). Some illustrative examples for inconsistency-tolerant model checking are presented based on the proposed logics and translations.

A preliminary short version of the results of this paper was published in the Proceedings of the 10th International Conference on Agents and Artificial Intelligence (ICAART 2018) [20]. The results of Sect. 4 in the present paper are not included in [20] (i.e., these are new results presented in this paper). The results of Sect. 5 in the present paper include some new results which were not presented in [20]. The results of the other sections in the present paper are slight extensions (with some detailed proofs and explanations) of the results presented in [20].

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

Institutional subscriptions

References

  1. Almukdad, A., Nelson, D.: Constructible falsity and inexact predicates. J. Symbol. Log. 49, 231–233 (1984)

    Article  MathSciNet  Google Scholar 

  2. Béziau, J.-Y.: A new four-valued approach to modal logic. Logique et Analyse 54(213), 109–121 (2011)

    MathSciNet  MATH  Google Scholar 

  3. Belnap, N.D.: A useful four-valued logic. In: Epstein, G., Dunn, J.M. (eds.) Modern Uses of Multiple-Valued Logic, pp. 5–37. Reidel, Dordrecht (1977)

    Chapter  Google Scholar 

  4. Belnap, N.D.: How a computer should think. In: Ryle, G. (ed.) Contemporary Aspects of Philosophy, pp. 30–56. Oriel Press, Stocksfield (1977)

    Google Scholar 

  5. Chen, D., Wu, J.: Reasoning about inconsistent concurrent systems: a non-classical temporal logic. In: Wiedermann, J., Tel, G., Pokorný, J., Bieliková, M., Štuller, J. (eds.) SOFSEM 2006. LNCS, vol. 3831, pp. 207–217. Springer, Heidelberg (2006). https://doi.org/10.1007/11611257_18

    Chapter  Google Scholar 

  6. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

    Chapter  Google Scholar 

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

    Google Scholar 

  8. da Costa, N.C.A., Béziau, J., Bueno, O.A.: Aspects of paraconsistent logic. Bull. IGPL 3(4), 597–614 (1995)

    Article  MathSciNet  Google Scholar 

  9. De, M., Omori, H.: Classical negation and expansions of Belnap-Dunn logic. Studia Logica 103(4), 825–851 (2015)

    Article  MathSciNet  Google Scholar 

  10. Dunn, J.M.: Intuitive semantics for first-degree entailment and ‘coupled trees’. Philos. Stud. 29(3), 149–168 (1976)

    Article  MathSciNet  Google Scholar 

  11. Easterbrook, S., Chechik, M.: A framework for multi-valued reasoning over inconsistent viewpoints. In: Proceedings of the 23rd International Conference on Software Engineering (ICSE 2001), pp. 411–420 (2001)

    Google Scholar 

  12. Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)

    Article  MathSciNet  Google Scholar 

  13. Emerson, E.A., Sistla, P.: Deciding full branching time logic. Inf. Control 61, 175–201 (1984)

    Article  MathSciNet  Google Scholar 

  14. Endo, K.: Applications of inconsistency-tolerant model checking to clinical reasoning verification. Bachelor thesis, Faculty of Science and Engineering, Department of Human Information Systems, Teikyo University, 59 p. (2018). (in Japanese)

    Google Scholar 

  15. Gurevich, Y.: Intuitionistic logic with strong negation. Studia Logica 36, 49–59 (1977)

    Article  MathSciNet  Google Scholar 

  16. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2006)

    Google Scholar 

  17. Kamide, N.: Extended full computation-tree logics for paraconsistent model checking. Log. Log. Philos. 15(3), 251–276 (2006)

    MathSciNet  MATH  Google Scholar 

  18. Kamide, N.: Inconsistency-tolerant temporal reasoning with hierarchical information. Inf. Sci. 320, 140–155 (2015)

    Article  MathSciNet  Google Scholar 

  19. Kamide, N.: Paraconsistent double negation that can simulate classical negation. In: Proceedings of the 46th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2016), pp. 131–136 (2016)

    Google Scholar 

  20. Kamide, N., Endo, K.: Logics and translations for inconsistency-tolerant model checking. In: Proceedings of the 10th International Conference on Agents and Artificial Intelligence (ICAART 2018), vol. 2, pp. 191–200 (2018)

    Google Scholar 

  21. Kamide, N., Kaneiwa, K.: Paraconsistent negation and classical negation in computation tree logic. In: Proceedings of the 2nd International Conference on Agents and Artificial Intelligence (ICAART 2010), vol. 1, pp. 464–469. INSTICC Press (2010)

    Google Scholar 

  22. Kamide, N., Koizumi, D.: Method for combining paraconsistency and probability in temporal reasoning. J. Adv. Comput. Intell. Intell. Inform. 20, 813–827 (2016)

    Article  Google Scholar 

  23. Kamide, N., Shramko, Y.: Embedding from multilattice logic into classical logic and vice versa. J. Log. Comput. 27(5), 1549–1575 (2017)

    MathSciNet  MATH  Google Scholar 

  24. Kamide, N., Wansing, H.: A paraconsistent linear-time temporal logic. Fundamenta Informaticae 106(1), 1–23 (2011)

    MathSciNet  MATH  Google Scholar 

  25. Kamide, N., Yano, R.: Logics and translations for hierarchical model checking. In: Proceedings of the 21st International Conference on Knowledge-Based and Intelligent Information & Engineering Systems, vol. 112, pp. 31–40 (2017). (Procedia Comput. Sci.)

    Article  Google Scholar 

  26. Kaneiwa, K., Kamide, N.: Paraconsistent computation tree logic. New Gener. Comput. 29(4), 391–408 (2011)

    Article  Google Scholar 

  27. Nelson, D.: Constructible falsity. J. Symbol. Log. 14, 16–26 (1949)

    Article  MathSciNet  Google Scholar 

  28. Odintsov, S.P.: The class of extensions of Nelson paraconsistent logic. Studia Logica 80, 291–320 (2005)

    Article  MathSciNet  Google Scholar 

  29. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  30. Priest, G.: Paraconsistent logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 6, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)

    Google Scholar 

  31. Rautenberg, W.: Klassische und nicht-klassische Aussagenlogik. Vieweg, Braunschweig (1979)

    Book  Google Scholar 

  32. Vorob’ev, N.: A constructive propositional logic with strong negation. Doklady Akademii Nauk SSSR 85, 465–468 (1952). (in Russian)

    Google Scholar 

  33. Wansing, H.: The Logic of Information Structures. LNAI, vol. 681, pp. 1–163. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56734-8

    Book  MATH  Google Scholar 

  34. Yano, R.: Applications of hierarchical model checking to hierarchical reasoning process verification. Bachelor thesis, Faculty of Science and Engineering, Department of Human Information Systems, Teikyo University, 52 p. (2018). (in Japanese)

    Google Scholar 

  35. Zaitsev, D.: Generalized relevant logic and models of reasoning. Moscow State Lomonosov University doctoral dissertation (2012)

    Google Scholar 

Download references

Acknowledgments

This research was supported by JSPS KAKENHI Grant Numbers JP16KK0007 and JP18K11171. This research has been supported by the Kayamori Foundation of Informational Science Advancement and JSPS Core-to-Core Program (A. Advanced Research Networks).

Author information

Authors and Affiliations

  1. Faculty of Science and Engineering, Department of Information and Electronic Engineering, Teikyo University, Toyosatodai 1-1, Utsunomiya, Tochigi, 320-8551, Japan

    Norihiro Kamide

  2. Faculty of Science and Engineering, Department of Human Information Systems, Teikyo University, Toyosatodai 1-1, Utsunomiya-shi, Tochigi, 320-8551, Japan

    Kazuki Endo

Authors
  1. Norihiro Kamide
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kazuki Endo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Norihiro Kamide .

Editor information

Editors and Affiliations

  1. Leiden University, Leiden, The Netherlands

    Jaap van den Herik

  2. University of Porto, Porto, Portugal

    Ana Paula Rocha

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kamide, N., Endo, K. (2019). Foundations of Inconsistency-Tolerant Model Checking: Logics, Translations, and Examples. In: van den Herik, J., Rocha, A. (eds) Agents and Artificial Intelligence. ICAART 2018. Lecture Notes in Computer Science(), vol 11352. Springer, Cham. https://doi.org/10.1007/978-3-030-05453-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-05453-3_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-05452-6

  • Online ISBN: 978-3-030-05453-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation