Advertisement

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

  • Norihiro KamideEmail author
  • Kazuki Endo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11352)

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.

Notes

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

References

  1. 1.
    Almukdad, A., Nelson, D.: Constructible falsity and inexact predicates. J. Symbol. Log. 49, 231–233 (1984)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Béziau, J.-Y.: A new four-valued approach to modal logic. Logique et Analyse 54(213), 109–121 (2011)MathSciNetzbMATHGoogle Scholar
  3. 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)CrossRefGoogle Scholar
  4. 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. 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_18CrossRefGoogle Scholar
  6. 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/BFb0025774CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    da Costa, N.C.A., Béziau, J., Bueno, O.A.: Aspects of paraconsistent logic. Bull. IGPL 3(4), 597–614 (1995)MathSciNetCrossRefGoogle Scholar
  9. 9.
    De, M., Omori, H.: Classical negation and expansions of Belnap-Dunn logic. Studia Logica 103(4), 825–851 (2015)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Dunn, J.M.: Intuitive semantics for first-degree entailment and ‘coupled trees’. Philos. Stud. 29(3), 149–168 (1976)MathSciNetCrossRefGoogle Scholar
  11. 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. 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)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Emerson, E.A., Sistla, P.: Deciding full branching time logic. Inf. Control 61, 175–201 (1984)MathSciNetCrossRefGoogle Scholar
  14. 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. 15.
    Gurevich, Y.: Intuitionistic logic with strong negation. Studia Logica 36, 49–59 (1977)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2006)Google Scholar
  17. 17.
    Kamide, N.: Extended full computation-tree logics for paraconsistent model checking. Log. Log. Philos. 15(3), 251–276 (2006)MathSciNetzbMATHGoogle Scholar
  18. 18.
    Kamide, N.: Inconsistency-tolerant temporal reasoning with hierarchical information. Inf. Sci. 320, 140–155 (2015)MathSciNetCrossRefGoogle Scholar
  19. 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. 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. 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. 22.
    Kamide, N., Koizumi, D.: Method for combining paraconsistency and probability in temporal reasoning. J. Adv. Comput. Intell. Intell. Inform. 20, 813–827 (2016)CrossRefGoogle Scholar
  23. 23.
    Kamide, N., Shramko, Y.: Embedding from multilattice logic into classical logic and vice versa. J. Log. Comput. 27(5), 1549–1575 (2017)MathSciNetzbMATHGoogle Scholar
  24. 24.
    Kamide, N., Wansing, H.: A paraconsistent linear-time temporal logic. Fundamenta Informaticae 106(1), 1–23 (2011)MathSciNetzbMATHGoogle Scholar
  25. 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.)CrossRefGoogle Scholar
  26. 26.
    Kaneiwa, K., Kamide, N.: Paraconsistent computation tree logic. New Gener. Comput. 29(4), 391–408 (2011)CrossRefGoogle Scholar
  27. 27.
    Nelson, D.: Constructible falsity. J. Symbol. Log. 14, 16–26 (1949)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Odintsov, S.P.: The class of extensions of Nelson paraconsistent logic. Studia Logica 80, 291–320 (2005)MathSciNetCrossRefGoogle Scholar
  29. 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. 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. 31.
    Rautenberg, W.: Klassische und nicht-klassische Aussagenlogik. Vieweg, Braunschweig (1979)CrossRefGoogle Scholar
  32. 32.
    Vorob’ev, N.: A constructive propositional logic with strong negation. Doklady Akademii Nauk SSSR 85, 465–468 (1952). (in Russian)Google Scholar
  33. 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-8CrossRefzbMATHGoogle Scholar
  34. 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. 35.
    Zaitsev, D.: Generalized relevant logic and models of reasoning. Moscow State Lomonosov University doctoral dissertation (2012)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Faculty of Science and Engineering, Department of Information and Electronic EngineeringTeikyo UniversityUtsunomiyaJapan
  2. 2.Faculty of Science and Engineering, Department of Human Information SystemsTeikyo UniversityUtsunomiya-shiJapan

Personalised recommendations