Zhang, Nan; Yu, Chaofeng; Duan, Zhenhua; Tian, Cong A proof system for unified temporal logic. (English) Zbl 07657061 Theor. Comput. Sci. 949, Article ID 113702, 28 p. (2023). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 949, Article ID 113702, 28 p. (2023; Zbl 07657061) Full Text: DOI
Ning, Xinya; Zhang, Nan; Duan, Zhenhua; Tian, Cong PPTL specification mining based on LNFG. (English) Zbl 07605947 Theor. Comput. Sci. 937, 85-95 (2022). MSC: 68Qxx PDFBibTeX XMLCite \textit{X. Ning} et al., Theor. Comput. Sci. 937, 85--95 (2022; Zbl 07605947) Full Text: DOI
Zhang, Nan; Duan, Zhenhua; Tian, Cong Unified temporal logic. (English) Zbl 1497.68322 Theor. Comput. Sci. 864, 58-69 (2021). MSC: 68Q60 03B44 93C95 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 864, 58--69 (2021; Zbl 1497.68322) Full Text: DOI
Liu, Jin; Duan, Zhenhua; Tian, Cong Multi-matching nested relations. (English) Zbl 1477.68157 Theor. Comput. Sci. 854, 77-93 (2021). MSC: 68Q45 68Q60 PDFBibTeX XMLCite \textit{J. Liu} et al., Theor. Comput. Sci. 854, 77--93 (2021; Zbl 1477.68157) Full Text: DOI
Zhang, Nan; Yu, Bin; Tian, Cong; Duan, Zhenhua; Yuan, Xiaoshuai Temporal logic specification mining of programs. (English) Zbl 1477.68168 Theor. Comput. Sci. 857, 29-42 (2021). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 857, 29--42 (2021; Zbl 1477.68168) Full Text: DOI
Lu, Xu; Duan, Zhenhua; Tian, Cong; Du, Hongwei Verify heaps via unified model checking. (English) Zbl 1464.68209 Theor. Comput. Sci. 819, 35-49 (2020). MSC: 68Q60 03B44 03B70 68N30 68P05 PDFBibTeX XMLCite \textit{X. Lu} et al., Theor. Comput. Sci. 819, 35--49 (2020; Zbl 1464.68209) Full Text: DOI
Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei A novel approach to verifying context free properties of programs. (English) Zbl 1436.68200 Theor. Comput. Sci. 809, 519-530 (2020). MSC: 68Q60 03B44 68Q45 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 809, 519--530 (2020; Zbl 1436.68200) Full Text: DOI
Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang Translating Xd-C programs to MSVL programs. (English) Zbl 1436.68077 Theor. Comput. Sci. 809, 430-465 (2020). MSC: 68N15 68N20 68Q60 PDFBibTeX XMLCite \textit{M. Wang} et al., Theor. Comput. Sci. 809, 430--465 (2020; Zbl 1436.68077) Full Text: DOI arXiv
Duan, Zhenhua; Tian, Cong; Zhang, Nan; Ma, Qian; Du, Hongwei Index set expressions can represent temporal logic formulas. (English) Zbl 1498.03047 Theor. Comput. Sci. 788, 21-38 (2019). MSC: 03B44 PDFBibTeX XMLCite \textit{Z. Duan} et al., Theor. Comput. Sci. 788, 21--38 (2019; Zbl 1498.03047) Full Text: DOI
Tian, Cong; Duan, Zhenhua Model checking open systems with alternating projection temporal logic. (English) Zbl 1423.68293 Theor. Comput. Sci. 774, 65-81 (2019). MSC: 68Q60 03B44 68Q45 68Q85 PDFBibTeX XMLCite \textit{C. Tian} and \textit{Z. Duan}, Theor. Comput. Sci. 774, 65--81 (2019; Zbl 1423.68293) Full Text: DOI
Yang, Kai; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei A temporal logic programming approach to planning. (English) Zbl 1419.68101 J. Comb. Optim. 38, No. 2, 402-420 (2019). MSC: 68T20 68N17 68T30 PDFBibTeX XMLCite \textit{K. Yang} et al., J. Comb. Optim. 38, No. 2, 402--420 (2019; Zbl 1419.68101) Full Text: DOI
Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei Verifying a scheduling protocol of safety-critical systems. (English) Zbl 1423.90101 J. Comb. Optim. 37, No. 4, 1191-1215 (2019). MSC: 90B35 68M20 PDFBibTeX XMLCite \textit{M. Wang} et al., J. Comb. Optim. 37, No. 4, 1191--1215 (2019; Zbl 1423.90101) Full Text: DOI
Yang, Kai; Duan, Zhenhua; Tian, Cong; Zhang, Nan A compiler for MSVL and its applications. (English) Zbl 1407.68096 Theor. Comput. Sci. 749, 2-16 (2018). MSC: 68N20 68Q60 68T20 PDFBibTeX XMLCite \textit{K. Yang} et al., Theor. Comput. Sci. 749, 2--16 (2018; Zbl 1407.68096) Full Text: DOI
Shi, Ya; Tian, Cong; Duan, Zhenhua; Zhou, Mengchu Model checking Petri nets with MSVL. (English) Zbl 1427.68210 Inf. Sci. 363, 274-291 (2016). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{Y. Shi} et al., Inf. Sci. 363, 274--291 (2016; Zbl 1427.68210) Full Text: DOI
Lu, Xu; Duan, Zhenhua; Tian, Cong Using unified model checking to verify heaps. (English) Zbl 1483.68199 Chan, T-H. Hubert (ed.) et al., Combinatorial optimization and applications. 10th international conference, COCOA 2016, Hong Kong, China, December 16–18, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10043, 735-743 (2016). MSC: 68Q60 03B44 03B70 68N30 68P05 PDFBibTeX XMLCite \textit{X. Lu} et al., Lect. Notes Comput. Sci. 10043, 735--743 (2016; Zbl 1483.68199) Full Text: DOI
Zhang, Nan; Duan, Zhenhua; Tian, Cong A mechanism of function calls in MSVL. (English) Zbl 1353.68184 Theor. Comput. Sci. 654, 11-25 (2016). MSC: 68Q60 68N17 68Q85 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 654, 11--25 (2016; Zbl 1353.68184) Full Text: DOI
Liu, Yao; Duan, Zhenhua; Tian, Cong; Cui, Bin Satisfiability of linear time mu-calculus on finite traces. (English) Zbl 1476.68178 Dinh, Thang N. (ed.) et al., Computing and combinatorics. 22nd international conference, COCOON 2016, Ho Chi Minh City, Vietnam, August 2–4, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9797, 611-622 (2016). MSC: 68Q85 03B44 PDFBibTeX XMLCite \textit{Y. Liu} et al., Lect. Notes Comput. Sci. 9797, 611--622 (2016; Zbl 1476.68178) Full Text: DOI
Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong Verifying safety critical task scheduling systems in PPTL axiom system. (English) Zbl 1333.90055 J. Comb. Optim. 31, No. 2, 577-603 (2016). MSC: 90B35 PDFBibTeX XMLCite \textit{N. Zhang} et al., J. Comb. Optim. 31, No. 2, 577--603 (2016; Zbl 1333.90055) Full Text: DOI
Zhang, Nan; Duan, Zhenhua; Tian, Cong A complete axiom system for propositional projection temporal logic with cylinder computation model. (English) Zbl 1332.68145 Theor. Comput. Sci. 609, Part 3, 639-657 (2016). MSC: 68Q60 03B44 68T15 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 609, Part 3, 639--657 (2016; Zbl 1332.68145) Full Text: DOI
Duan, Zhenhua; Tian, Cong; Zhang, Nan A canonical form based decision procedure and model checking approach for propositional projection temporal logic. (English) Zbl 1370.68200 Theor. Comput. Sci. 609, Part 3, 544-560 (2016). Reviewer: Martin Lange (Kassel) MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{Z. Duan} et al., Theor. Comput. Sci. 609, Part 3, 544--560 (2016; Zbl 1370.68200) Full Text: DOI
Wang, Haiyang; Duan, Zhenhua; Tian, Cong Symbolic model checking for alternating projection temporal logic. (English) Zbl 1473.68108 Lu, Zaixin (ed.) et al., Combinatorial optimization and applications. 9th international conference, COCOA 2015, Houston, TX, USA, December 18–20, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9486, 481-495 (2015). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{H. Wang} et al., Lect. Notes Comput. Sci. 9486, 481--495 (2015; Zbl 1473.68108) Full Text: DOI
Duan, Zhenhua; Bu, Kangkang; Tian, Cong; Zhang, Nan Model checking MSVL programs based on dynamic symbolic execution. (English) Zbl 1465.68176 Xu, Dachuan (ed.) et al., Computing and combinatorics. 21st international conference, COCOON 2015, Beijing, China, August 4–6, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9198, 521-533 (2015). MSC: 68Q60 PDFBibTeX XMLCite \textit{Z. Duan} et al., Lect. Notes Comput. Sci. 9198, 521--533 (2015; Zbl 1465.68176) Full Text: DOI
Liu, Jin; Duan, Zhenhua; Tian, Cong; Zhang, Nan An extended strange planet protocol. (English) Zbl 1341.90114 J. Comb. Optim. 30, No. 2, 299-319 (2015). MSC: 90C27 PDFBibTeX XMLCite \textit{J. Liu} et al., J. Comb. Optim. 30, No. 2, 299--319 (2015; Zbl 1341.90114) Full Text: DOI
Luo, Ling; Duan, Zhenhua; Tian, Cong; Wang, Xiaobing A structural transformation from p-\(\pi\) to MSVL. (English) Zbl 1315.68182 J. Comb. Optim. 29, No. 1, 308-329 (2015). MSC: 68Q60 68Q85 PDFBibTeX XMLCite \textit{L. Luo} et al., J. Comb. Optim. 29, No. 1, 308--329 (2015; Zbl 1315.68182) Full Text: DOI
Tian, Cong; Duan, Zhenhua; Yang, Mengfei Transformation from PLTL to automata via NFGs. (English) Zbl 1319.68144 J. Comb. Optim. 29, No. 2, 406-417 (2015). MSC: 68Q60 03B44 03D05 68Q45 PDFBibTeX XMLCite \textit{C. Tian} et al., J. Comb. Optim. 29, No. 2, 406--417 (2015; Zbl 1319.68144) Full Text: DOI
Yu, Bin; Duan, Zhenhua; Tian, Cong Bounded model checking of traffic light control system. (English) Zbl 1351.68169 Xue, Jinyun (ed.) et al., Proceedings of the 6th international workshop on harnessing theories for tool support in software (TTSS 2013), Nanchang, China, October 27, 2013. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 309, 63-74, electronic only (2014). MSC: 68Q60 03B44 90B20 PDFBibTeX XMLCite \textit{B. Yu} et al., Electron. Notes Theor. Comput. Sci. 309, 63--74 (2014; Zbl 1351.68169) Full Text: DOI
Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Dingzhu A formal proof of the deadline driven scheduler in PPTL axiomatic system. (English) Zbl 1360.68771 Theor. Comput. Sci. 554, 229-253 (2014). MSC: 68T15 03B44 68M20 68N30 68Q60 68Q85 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 554, 229--253 (2014; Zbl 1360.68771) Full Text: DOI
Duan, Zhenhua; Tian, Cong A practical decision procedure for propositional projection temporal logic with infinite models. (English) Zbl 1358.68188 Theor. Comput. Sci. 554, 169-190 (2014). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{Z. Duan} and \textit{C. Tian}, Theor. Comput. Sci. 554, 169--190 (2014; Zbl 1358.68188) Full Text: DOI
Zhang, Nan; Duan, Zhenhua; Tian, Cong A cylinder computation model for many-core parallel computing. (English) Zbl 1416.68074 Theor. Comput. Sci. 497, 68-83 (2013). MSC: 68Q05 68Q10 68Q60 PDFBibTeX XMLCite \textit{N. Zhang} et al., Theor. Comput. Sci. 497, 68--83 (2013; Zbl 1416.68074) Full Text: DOI
Duan, Zhenhua; Ma, Qian; Tian, Cong; Zhang, Nan Some fixed-point issues in PPTL. (English) Zbl 1391.03018 Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 151-165 (2013). MSC: 03B44 PDFBibTeX XMLCite \textit{Z. Duan} et al., Lect. Notes Comput. Sci. 8051, 151--165 (2013; Zbl 1391.03018) Full Text: DOI
Tian, Cong; Duan, Zhenhua Expressiveness of propositional projection temporal logic with star. (English) Zbl 1221.03018 Theor. Comput. Sci. 412, No. 18, 1729-1744 (2011). MSC: 03B44 03C05 68Q45 68Q60 PDFBibTeX XMLCite \textit{C. Tian} and \textit{Z. Duan}, Theor. Comput. Sci. 412, No. 18, 1729--1744 (2011; Zbl 1221.03018) Full Text: DOI
Tian, Cong; Duan, Zhenhua A note on stutter-invariant PLTL. (English) Zbl 1214.03015 Inf. Process. Lett. 109, No. 13, 663-667 (2009). MSC: 03B44 68Q60 PDFBibTeX XMLCite \textit{C. Tian} and \textit{Z. Duan}, Inf. Process. Lett. 109, No. 13, 663--667 (2009; Zbl 1214.03015) Full Text: DOI
Tian, Cong; Duan, Zhenhua Complexity of propositional projection temporal logic with star. (English) Zbl 1161.03008 Math. Struct. Comput. Sci. 19, No. 1, 73-100 (2009). MSC: 03B44 03B25 68Q60 PDFBibTeX XMLCite \textit{C. Tian} and \textit{Z. Duan}, Math. Struct. Comput. Sci. 19, No. 1, 73--100 (2009; Zbl 1161.03008) Full Text: DOI