Inconsistency-tolerant temporal reasoning with hierarchical information

•This paper introduces a new temporal logic, SPCTL.•SPCTL is an extension of the well-known computation tree logic (CTL).•The complexity of the model-checking problem of SPCTL is settled.•An illustrative example for medical diagnosis is presented based on SPCTL.

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.