Inconsistency-tolerant temporal reasoning with hierarchical information. (English) Zbl 1390.68610
Summary: A formal method is proposed for modeling and verifying inconsistency-tolerant temporal reasoning with hierarchical information. For this purpose, temporal logic called sequential paraconsistent computation tree logic (SPCTL) is obtained from computation tree logic by adding a paraconsistent negation connective and some sequence modal operators. SPCTL can appropriately represent both inconsistency-tolerant reasoning by the paraconsistent negation connective and hierarchical information by the sequence modal operators. The validity, satisfiability, and model-checking problems of SPCTL are shown to be EXPTIME-complete, deterministic EXPTIME-complete, and deterministic PTIME-complete, respectively. Illustrative examples for inconsistency-tolerant temporal reasoning with hierarchical information are presented using the proposed SPCTL.
MSC:
| 68T27 | Logic in artificial intelligence |
| 03B44 | Temporal logic |
| 03B53 | Paraconsistent logics |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
computation tree logic; paraconsistent logic; complexity; inconsistency-tolerant reasoning; hierarchical informationReferences:
| [1] | Almukdad, A.; Nelson, D., Constructible falsity and inexact predicates, J. Symbol. Log., 49, 231-233 (1984) · Zbl 0575.03016 |
| [2] | (Baader, F.; Calvanese, D.; McGuinness, D.; Nardi, D.; Patel-Schneider, Peter F., The Description Logic Handbook: Theory, Implementation and Applications (2003), Cambridge University Press) · Zbl 1058.68107 |
| [3] | Blair, H. A.; Subrahmanian, V. S., Paraconsistent logic programming, Theor. Comput. Sci., 68, 2, 135-154 (1989) · Zbl 0686.68009 |
| [4] | Carnielli, W.; Coniglio, M.; Gabbay, D. M.; Gouveia, P.; Sernadas, C., Analysis and synthesis of logics: how to cut and paste reasoning systems, (Applied Logic Series, vol. 35 (2008), Springer) · Zbl 1137.03001 |
| [5] | Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronization skeletons using branching time temporal logic, Lect. Notes Comput. Sci., 131, 52-71 (1981) · Zbl 0546.68014 |
| [6] | Clarke, E. M.; Grumberg, O.; Peled, D. A., Model Checking (1999), The MIT Press |
| [7] | da Costa, N. C.A.; Béziau, J.; Bueno, O. A., Aspects of paraconsistent logic, Bull. IGPL, 3, 4, 597-614 (1995) · Zbl 0843.03014 |
| [8] | 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) · Zbl 0629.68020 |
| [9] | Emerson, E. A.; Sistla, P., Deciding full branching time logic, Inform. Control, 61, 175-201 (1984) · Zbl 0593.03007 |
| [11] | Kamide, N.; Wansing, H., Proof theory of Nelson’s paraconsistent logic: a uniform perspective, Theor. Comput. Sci., 415, 1-38 (2012) · Zbl 1382.03048 |
| [12] | Kaneiwa, K.; Kamide, N., Paraconsistent computation tree logic, New Gener. Comput., 29, 4, 391-408 (2011) · Zbl 1251.68227 |
| [13] | Kaneiwa, K.; Kamide, N., Conceptual modeling in full computation-tree logic with sequence modal operator, Int. J. Intell. Syst., 26, 7, 636-651 (2011) |
| [14] | Murata, T.; Subrahmanian, V. S.; Wakayama, T., A Petri net model for reasoning in the presence of inconsistency, IEEE Trans. Knowl. Data Eng., 3, 3, 281-292 (1991) |
| [15] | Nelson, D., Constructible falsity, J. Symbol. Log., 14, 16-26 (1949) · Zbl 0033.24304 |
| [16] | Priest, G., Paraconsistent logic, (Gabbay, D. M.; Guenthner, F., Handbook of Philosophical Logic, vol. 6 (2002), Kluwer Academic Publishers), 287-393 · Zbl 1065.03002 |
| [18] | Wagner, G., Logic programming with strong negation and inexact predicates, J. Log. Comput., 1, 6, 835-859 (1991) · Zbl 0738.68018 |
| [19] | Wansing, H., The logic of information structures, Lect. Notes Artif. Intell., 681, 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.
