×

Paraconsistent computation tree logic. (English) Zbl 1251.68227

Summary: It is known that paraconsistent logical systems are more appropriate for inconsistency-tolerant and uncertainty reasoning than other types of logical systems. In this paper, a paraconsistent computation tree logic, PCTL, is obtained by adding paraconsistent negation to the standard computation tree logic CTL. PCTL can be used to appropriately formalize inconsistency-tolerant temporal reasoning. A theorem for embedding PCTL into CTL is proved. The validity, satisfiability, and model-checking problems of PCTL are shown to be decidable. The embedding and decidability results indicate that we can reuse the existing CTL-based algorithms for validity, satisfiability, and model-checking. An illustrative example of medical reasoning involving the use of PCTL is presented.

MSC:

68T27 Logic in artificial intelligence
03B53 Paraconsistent logics
68Q60 Specification and verification (program logics, model checking, etc.)
68T37 Reasoning under uncertainty in the context of artificial intelligence

Software:

YASM
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Almukdad A., Nelson D.: ”Constructible falsity and inexact predicates”. Journal of Symbolic Logic 49, 231–233 (1984) · Zbl 0575.03016 · doi:10.2307/2274105
[2] Béziau, J.-Y., ”The future of paraconsistent logic,” Logical Studies, 2, Online available, 1999.
[3] Chechik, M. and MacCaull, W., ”CTL model-checking over logics with nonclassical negations,” Proc. of the 33rd IEEE International Conference on Multivalued logics (ISMVL’03), pp. 293–300, 2003.
[4] Chen D., Wu J.: ”Reasoning about inconsistent concurrent systems: A nonclassical temporal logic”. LNCS 3831, 207–217 (2006) · Zbl 1175.68275
[5] Clarke E.M., Emerson E.A.: ”Design and synthesis of synchronization skeletons using branching time temporal logic”. LNCS 131, 52–71 (1981)
[6] Clarke E.M., Grumberg O., Jha S., Lu Y., Veith H.: ”Counterexample-guided abstraction refinement for symbolic model checking”. Journal of the ACM, 50, 5 752–794 (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643
[7] Clarke, E. M., Grumberg, O. and Peled, D. A., Model checking, The MIT Press, 1999.
[8] da Costa N.C.A., Béziau J., Bueno O.A.: ”Aspects of paraconsistent logic”. Bulletin of the IGPL, 3, 4 597–614 (1995) · Zbl 0843.03014
[9] Easterbrook S. and Chechik, M., ”A framework for multi-valued reasoning over inconsistent viewpoints,” Proc. of the 23rd International Conference on Software Engineering (ICSE 2001), pp. 411–420, 2001.
[10] Gurfinkel A., Wei O., Chechik M.: ”Yasm: a software model-checker for verification and refutation”. Proc. of the 18th International Conference, Computer Aided Verification (CAV’06, LNCS 4144 4144, 170–174 (2006)
[11] Gurfinkel A., Chechik M.: ”Why wast a perfectly good abstraction?”. Proc. of the 18th International Conference Tools and Algorithms for Construction and Analysis of Systems (TACAS’06 LNCS. 3920, 212–226 (2006) · Zbl 1180.68174 · doi:10.1007/11691372_14
[12] Gurevich Y.: ”Intuitionistic logic with strong negation”. Studia Logica 36, 49–59 (1977) · Zbl 0366.02015 · doi:10.1007/BF02121114
[13] Kamide N.: ”Linear and affine logics with temporal, spatial and epistemic operators”. Theoretical Computer Science 353 1-3, 165–207 (2006) · Zbl 1175.03039 · doi:10.1016/j.tcs.2005.10.043
[14] Kamide N.: ”Extended full computation-tree logics for paraconsistent model checking”. Logic and Logical Philosophy 15(3), 251–276 (2006) · Zbl 1133.68045
[15] Kamide, N., ”A uniform proof-theoretic foundation for abstract paraconsistent logic programming,” Journal of Functional and Logic Programming, pp. 1–36, 2007. · Zbl 1214.68120
[16] Kamide, N. and Kaneiwa K., ”Paraconsistent negation and classical negation in computation tree logic,” Proc. of the 2nd International Conference on Agents and Artificial Intelligence (ICAART 2010), 1, AI, INSTICC Press, pp. 464–469, 2010.
[17] Kamide N., Wansing H.: ”Combining linear-time temporal logic with constructiveness and paraconsistency”. Journal of Applied Logic, 8, 33–61 (2010) · Zbl 1207.03022 · doi:10.1016/j.jal.2009.06.001
[18] Kaneiwa K.: ”Order-sorted logic programming with predicate hierarchy”. Artificial Intelligence, 158(2), 155–188 (2004) · Zbl 1086.68026 · doi:10.1016/j.artint.2004.05.001
[19] Kaneiwa K.: ”Description logics with contraries, contradictories, and subcontraries”. New Generation Computing, 25(4), 443–468 (2007) · Zbl 1137.68055 · doi:10.1007/s00354-007-0028-2
[20] Kaneiwa K., Satoh K.: ”On the complexities of consistency checking for restricted UML class diagrams”. Theoretical Computer Science 411(2), 301–323 (2010) · Zbl 1186.68052 · doi:10.1016/j.tcs.2009.04.030
[21] Murata T., SubrahmanianV.S. Wakayama T.: ”A Petri net model for reasoning in the presence of inconsistency”. IEEE Transactions on Knowledge and Data Engineering 3(3), 281–292 (1991) · Zbl 05109175 · doi:10.1109/69.91059
[22] Nelson D.: ”Constructible falsity”. Journal of Symbolic Logic 14, 16–26 (1949) · Zbl 0033.24304 · doi:10.2307/2268973
[23] Odintsov, S. P. and Wansing, H., ”Inconsistency-tolerant description logic: Motivation and basic systems,” in Trends in Logic: 50 Years of Studia Logica (Hendricks, V. F. and Malinowski, J. eds.), Kluwer Academic Publishers, Dordrecht, pp. 301–335, 2003. · Zbl 1048.03021
[24] Priest G., Routley R.: ”Introduction: paraconsistent logics”. Studia Logica, 43, 3–16 (1982) · Zbl 0575.03017 · doi:10.1007/BF00935736
[25] Pnueli, A., ”The temporal logic of programs,” Proc. of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57, 1977.
[26] Rautenberg W.: Klassische und nicht-klassische Aussagenlogik. Vieweg, Braunschweig (1979) · Zbl 0424.03007
[27] Vorob’ev N.N.: ”A constructive propositional calculus with strong negation (in Russian)”. Doklady Akademii Nauk SSR 85, 465–468 (1952)
[28] Wagner G.: ”Logic programming with strong negation and inexact predicates”. Journal of Logic and Computation 1(6), 835–859 (1991) · Zbl 0738.68018 · doi:10.1093/logcom/1.6.835
[29] Wansing H.: ”The logic of information structures”. Lecture Notes in Artificial Intelligence 681, 1–163 (1993) · Zbl 0788.03001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.