×

A decision procedure and complete axiomatization for projection temporal logic. (English) Zbl 1506.03070

Summary: To specify and verify the concurrent and reactive systems with the theorem proving approach, a complete axiomatization is formalized for first order projection temporal logic (PTL) with both finite and infinite time. To this end, PTL is restricted to a finite domain, and the syntax, semantics as well as the axiomatization of PTL are presented. Further, the techniques of labeled normal form and labeled normal form graph of PTL formulas are introduced respectively, with which a decision procedure for quantifier free PTL (QFPTL) formulas is given. Moreover, a generalized labeled normal form graph is defined and employed to transform a quantified PTL formula into its equivalent QFPTL formula. Finally, a decision procedure for PTL is formalized and the completeness of the axiomatic system is proved based on the decidability of PTL formulas.

MSC:

03B44 Temporal logic
03B35 Mechanization of proofs and logical operations
68V20 Formalization of mathematics in connection with theorem provers

Software:

MSVL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Duan, Z., An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming (1996), Newcastle University: Newcastle University Newcastle upon Tyne, UK, Ph.D. Thesis
[2] Duan, Z., Temporal Logic and Temporal Logic Programming (2005), Science Press
[3] 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
[4] Tian, C.; Duan, Z., Expressiveness of propositional projection temporal logic with star, Theoret. Comput. Sci., 412, 18, 1729-1744 (2011) · Zbl 1221.03018
[5] Duan, Z.; Koutny, M., A framed temporal logic programming language, J. Comput. Sci. Tech., 19, 3, 341-351 (2004)
[6] Duan, Z.; Yang, X.; Koutny, M., Framed temporal logic programming, Sci. Comput. Program., 70, 1, 31-61 (2008) · Zbl 1131.68036
[7] Shu, X.; Duan, Z., Extending MSVL with semaphore, (COCOON 2016 (2016)), 599-610 · Zbl 1476.68183
[8] Zhang, N.; Duan, Z.; Tian, C., A mechanism of function calls in MSVL, Theoret. Comput. Sci., 654, 11-25 (2016) · Zbl 1353.68184
[9] Wang, X.; Tian, C.; Duan, Z.; Zhao, L., MSVL: a typed language for temporal logic programming, Front. Comput. Sci. (2017)
[10] Duan, Z.; Tian, C., A unified model checking approach with projection temporal logic, (ICFEM 2008 (2008)), 167-186
[11] Clarke, E. M.; Wang, Q., 25 years of model checking, (Perspectives of System Informatics - 9th International Ershov Informatics Conference. Perspectives of System Informatics - 9th International Ershov Informatics Conference, PSI 2014 (2014)), 26-40 · Zbl 1434.68296
[12] Kanso, K.; Setzer, A., A light-weight integration of automated and interactive theorem proving, Math. Structures Comput. Sci., 26, 1, 129-153 (2016) · Zbl 1361.68189
[13] McMillan, K. L., Symbolic Model Checking (1993), Kluwer · Zbl 0784.68004
[14] Duan, Z.; Tian, C., A practical decision procedure for propositional projection temporal logic with infinite models, Theoret. Comput. Sci., 554, 169-190 (2014) · Zbl 1358.68188
[15] Duan, Z.; Tian, C.; Zhang, N., A canonical form based decision procedure and model checking approach for propositional projection temporal logic, Theoret. Comput. Sci., 609, 544-560 (2016) · Zbl 1370.68200
[16] Zhang, N.; Duan, Z.; Tian, C., Model checking concurrent systems with MSVL, Sci. China Ser. F, 59, 11, Article 118101 pp. (2016)
[17] Duan, Z., Modeling and Analysis of Hybrid Systems (2004), Science Press
[18] Shu, X.; Duan, Z., Model checking process scheduling over multi-core computer system with MSVL, (SOFL + MSVL 2015 (2015)), 103-117
[19] Yang, K.; Duan, Z.; Tian, C., Modeling and verification of RBC handover protocol, Electron. Notes Theor. Comput. Sci., 309, 51-62 (2014)
[20] Zhang, N.; Duan, Z.; Tian, C., A cylinder computation model for many-core parallel computing, Theoret. Comput. Sci., 497, 68-83 (2013) · Zbl 1416.68074
[21] Duan, Z.; Yang, X.; Koutny, M., Semantics of framed temporal logic programs, (ICLP 2005 (2005)), 356-370 · Zbl 1165.68329
[22] Kesten, Y.; Pnueli, A., Complete proof system for QPTL, J. Logic Comput., 12, 5, 701-745 (2002) · Zbl 1013.03012
[23] Duan, Z.; Zhang, N.; Koutny, M., A complete proof system for propositional projection temporal logic, Theoret. Comput. Sci., 497, 84-107 (2013) · Zbl 1417.03146
[24] Bowman, H.; Thompson, S. J., A decision procedure and complete axiomatization of finite interval temporal logic with projection, J. Logic Comput., 13, 2, 195-239 (2003) · Zbl 1050.03012
[25] Tarjan, R. E., Depth-first search and linear graph algorithms, SIAM J. Comput., 1, 2, 146-160 (1972) · Zbl 0251.05107
[26] Winskel, G., The Formal Semantics of Programming Languages - An Introduction, Foundation of Computing Series (1993), MIT Press · Zbl 0919.68082
[27] Gabbay, D. M.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal basis of fairness, (Conference Record of the 7th Annual ACM Symposium on Principles of Programming Languages (1980)), 163-173
[28] Moszkowski, B. C., A complete axiom system for propositional interval temporal logic with infinite time, Logical Methods in Computer Science, 8, 3 (2012) · Zbl 1256.03023
[29] Lichtenstein, O.; Pnueli, A., Propositional temporal logics: decidability and completeness, Log. J. IGPL, 8, 1, 55-85 (2000) · Zbl 1033.03009
[30] Moszkowski, B. C., A hierarchical completeness proof for propositional interval temporal logic with finite time, J. Appl. Non-Classical Logics, 14, 1-2, 55-104 (2004) · Zbl 1181.03015
[31] Rosner, R.; Pnueli, A., A choppy logic, (LICS 1986 (1986)), 306-313
[32] Zhang, N.; Duan, Z.; Tian, C., A complete axiom system for propositional projection temporal logic with cylinder computation model, Theoret. Comput. Sci., 609, 639-657 (2016) · Zbl 1332.68145
[33] Abadi, M., The power of temporal proofs, Theoret. Comput. Sci., 65, 1, 123-130 (1987)
[34] Chaochen, Z.; Hansen, M. R.; Sestoft, P., Decidability and undecidability results for duration calculus, (STACS 1993 (1993)), 58-68 · Zbl 0811.68115
[35] Hodkinson, I. M.; Wolter, F.; Zakharyaschev, M., Decidable and undecidable fragments of first-order branching temporal logics, (LICS 2002 (2002)), 393-402
[36] Szalas, A.; Holenderski, L., Incompleteness of first-order temporal logic with until, Theoret. Comput. Sci., 57, 317-325 (1988) · Zbl 0677.03013
[37] Cook, S. A., Corrigendum: soundness and completeness of an axiom system for program verification, SIAM J. Comput., 10, 3, 612 (1981) · Zbl 0466.68015
[38] Manna, Z.; Pnueli, A., Completing the temporal picture, Theoret. Comput. Sci., 83, 1, 91-130 (1991) · Zbl 0795.68133
[39] Chaochen, Z.; Hansen, M. R., Duration Calculus - A Formal Approach to Real-Time Systems, Monographs in Theoretical Computer Science, An EATCS Series (2004), Springer · Zbl 1071.68062
[40] Pnueli, A.; Kesten, Y., A deductive proof system for CTL, (13th International Conference Concurrency Theory. 13th International Conference Concurrency Theory, CONCUR 2002 (2002)), 24-40 · Zbl 1012.68119
[41] French, T.; Reynolds, M., A sound and complete proof system for QPTL, (Advances in Modal logic (2002, 2002)), 127-148 · Zbl 1083.03022
[42] Reynolds, M., Axiomatising first-order temporal logic: until and since over linear time, Studia Logica, 57, 2/3, 279-302 (1996) · Zbl 0864.03015
[43] Dutertre, B., Complete proof systems for first order interval temporal logic, (LICS 1995 (1995)), 36-43
[44] Guelev, D. P., A complete proof system for first-order interval temporal logic with projection, J. Logic Comput., 14, 2, 215-249 (2004) · Zbl 1070.03009
[45] Moszkowski, B. C., A complete axiomatization of interval temporal logic with infinite time, (LICS 2000 (2000)), 241-252
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.