zbMATH — the first resource for mathematics

Efficient decision procedure for propositional projection temporal logic. (English) Zbl 07242322
Summary: The decision problem for Propositional Projection Temporal Logic (PPTL) has been solved successfully, however time complexity of the procedure is increased exponentially to the length of the formula. To solve the problem, a labeled unified complete normal form is introduced as the intermediate form to rewrite a PPTL formula into its equivalent labeled normal form, based on which the labeled normal form graph is constructed, and an efficient decision procedure for PPTL is formalized with the time complexity linear to the length of the formula and the size of the power set of the atomic propositions in the formula. Besides, an example is given to show how the improved decision procedure works.
MSC:
 03B44 Temporal logic
MSVL; SPIN
Full Text:
References:
 [1] Duan, Z., Temporal Logic and Temporal Logic Programming (2005), Science Press [2] Duan, Z.; Yang, X.; Koutny, M., Framed temporal logic programming, Sci. Comput. Program., 70, 1, 31-61 (2008) · Zbl 1131.68036 [3] Moszkowski, B. C., Executing Temporal Logic Programs (1986), Cambridge University Press · Zbl 0658.68014 [4] Duan, Z.; Tian, C., A unified model checking approach with projection temporal logic, (ICFEM 2008 (2008)), 167-186 [5] Yang, K.; Duan, Z.; Tian, C.; Zhang, N., A compiler for MSVL and its applications, Theor. Comput. Sci., 749, 2-16 (2018) · Zbl 1407.68096 [6] Wang, X.; Tian, C.; Duan, Z.; Zhao, L., MSVL: a typed language for temporal logic programming, Front. Comput. Sci., 11, 5, 762-785 (2017) [7] Zhang, N.; Duan, Z.; Tian, C., A mechanism of function calls in MSVL, Theor. Comput. Sci., 654, 11-25 (2016) · Zbl 1353.68184 [8] Shu, X.; Duan, Z., Extending MSVL with semaphore, (COCOON 2016 (2016)), 599-610 · Zbl 06622062 [9] Tian, C.; Duan, Z., Expressiveness of propositional projection temporal logic with star, Theor. Comput. Sci., 412, 18, 1729-1744 (2011) · Zbl 1221.03018 [10] Tian, C.; Duan, Z., Complexity of propositional projection temporal logic with star, Math. Struct. Comput. Sci., 19, 1, 73-100 (2009) · Zbl 1161.03008 [11] Cui, J.; Duan, Z.; Tian, C.; Du, H., A novel approach to modeling and verifying real-time systems for high reliability, IEEE Trans. Reliab., 67, 2, 481-493 (2018) [12] Zhang, N.; Duan, Z.; Tian, C., Model checking concurrent systems with MSVL, Sci. China Inf. Sci., 59, 11, Article 118101 pp. (2016) [13] Yu, B.; Duan, Z.; Tian, C.; Zhang, N., Verifying temporal properties of programs: a parallel approach, J. Parallel Distrib. Comput., 118, 89-99 (2018) [14] Zhang, N.; Duan, Z.; Tian, C.; Du, D., A formal proof of the deadline driven scheduler in PPTL axiomatic system, Theor. Comput. Sci., 554, 229-253 (2014) · Zbl 1360.68771 [15] Ma, Q.; Duan, Z.; Zhang, N.; Wang, X., Verification of distributed systems with the axiomatic system of MSVL, Form. Asp. Comput., 27, 1, 103-131 (2015) · Zbl 1328.68032 [16] Holzmann, G., The model checker spin, IEEE Trans. Softw. Eng., 23, 5, 279-295 (1997) [17] McMillan, K. L., Symbolic Model Checking (1993), Kluwer · Zbl 0784.68004 [18] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic with infinite models, Acta Inform., 45, 1, 43-78 (2008) · Zbl 1141.68039 [19] Duan, Z.; Tian, C., A practical decision procedure for propositional projection temporal logic with infinite models, Theor. Comput. Sci., 554, 169-190 (2014) · Zbl 1358.68188 [20] Duan, Z.; Tian, C.; Zhang, N., A canonical form based decision procedure and model checking approach for propositional projection temporal logic, Theor. Comput. Sci., 609, 544-560 (2016) · Zbl 1370.68200 [21] Shu, X.; Duan, Z., A decision procedure and complete axiomatization for projection temporal logic, Theor. Comput. Sci., 819, 50-84 (2020) · Zbl 07188529 [22] Bowman, H.; Thompson, S. J., A decision procedure and complete axiomatization of finite interval temporal logic with projection, J. Log. Comput., 13, 2, 195-239 (2003) · Zbl 1050.03012
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.