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].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Almukdad, A., Nelson, D.: Constructible falsity and inexact predicates. J. Symbol. Log. 49, 231–233 (1984)
Béziau, J.-Y.: A new four-valued approach to modal logic. Logique et Analyse 54(213), 109–121 (2011)
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)
Belnap, N.D.: How a computer should think. In: Ryle, G. (ed.) Contemporary Aspects of Philosophy, pp. 30–56. Oriel Press, Stocksfield (1977)
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
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
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
da Costa, N.C.A., Béziau, J., Bueno, O.A.: Aspects of paraconsistent logic. Bull. IGPL 3(4), 597–614 (1995)
De, M., Omori, H.: Classical negation and expansions of Belnap-Dunn logic. Studia Logica 103(4), 825–851 (2015)
Dunn, J.M.: Intuitive semantics for first-degree entailment and ‘coupled trees’. Philos. Stud. 29(3), 149–168 (1976)
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)
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)
Emerson, E.A., Sistla, P.: Deciding full branching time logic. Inf. Control 61, 175–201 (1984)
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)
Gurevich, Y.: Intuitionistic logic with strong negation. Studia Logica 36, 49–59 (1977)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2006)
Kamide, N.: Extended full computation-tree logics for paraconsistent model checking. Log. Log. Philos. 15(3), 251–276 (2006)
Kamide, N.: Inconsistency-tolerant temporal reasoning with hierarchical information. Inf. Sci. 320, 140–155 (2015)
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)
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)
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)
Kamide, N., Koizumi, D.: Method for combining paraconsistency and probability in temporal reasoning. J. Adv. Comput. Intell. Intell. Inform. 20, 813–827 (2016)
Kamide, N., Shramko, Y.: Embedding from multilattice logic into classical logic and vice versa. J. Log. Comput. 27(5), 1549–1575 (2017)
Kamide, N., Wansing, H.: A paraconsistent linear-time temporal logic. Fundamenta Informaticae 106(1), 1–23 (2011)
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.)
Kaneiwa, K., Kamide, N.: Paraconsistent computation tree logic. New Gener. Comput. 29(4), 391–408 (2011)
Nelson, D.: Constructible falsity. J. Symbol. Log. 14, 16–26 (1949)
Odintsov, S.P.: The class of extensions of Nelson paraconsistent logic. Studia Logica 80, 291–320 (2005)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)
Priest, G.: Paraconsistent logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 6, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)
Rautenberg, W.: Klassische und nicht-klassische Aussagenlogik. Vieweg, Braunschweig (1979)
Vorob’ev, N.: A constructive propositional logic with strong negation. Doklady Akademii Nauk SSSR 85, 465–468 (1952). (in Russian)
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
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)
Zaitsev, D.: Generalized relevant logic and models of reasoning. Moscow State Lomonosov University doctoral dissertation (2012)
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)