×

Temporal normal form for linear temporal logic formulae. (English) Zbl 1361.03012

Summary: In the present paper, the concepts of characters as well as the least characters for LTL (Linear Temporal Logic) formulae are introduced. It is pointed out that those LTL formulae with characters can always be checked within finite steps during model checking even in some cases when the underlying transition system contains infinite states. What is more, the class of LTL formulae with characters can be characterized by full LTL\(_n\), the bounded case for LTL. Meanwhile, two types of temporal normal form for LTL formulae are proposed. A necessary and sufficient condition is given in which an LTLformula has an equivalent formula in temporal normal form.

MSC:

03B44 Temporal logic
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

Software:

CESAR
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baier, Principles of Model Checking (2008)
[2] Blackburn, Modal Logic (2001) · doi:10.1017/CBO9781107050884
[3] Clarke, In: Logic ofrograms, LNCS, Design and synthesis of synchronization skeletons using branching time temporal logic 131 pp 52– (1981)
[4] Clarke, Model Checking (1999)
[5] Clarke, Computer-aided verification, IEEE Spectrum 33 (6) pp 61– (1996) · doi:10.1109/6.499951
[6] Ding, Optimal control of Markov decision processes with linear temporal logic constraints, IEEE Transactions on Automatic Control 59 (5) pp 1244– (2014) · Zbl 1360.90276 · doi:10.1109/TAC.2014.2298143
[7] Feng, Model checking quantum Markov chains, Journal of Computer and System Sciences 79 pp 1181– (2013) · Zbl 1311.68086 · doi:10.1016/j.jcss.2013.04.002
[8] Gotzhein, Temporal logic and applications: A tutorial, Computer Networks and ISDN Systems 24 (3) pp 203– (1992) · Zbl 0767.68042 · doi:10.1016/0169-7552(92)90109-4
[9] Huth, Logic in Computer Science-Modelling and Reasoning about Systems (2nd ed.) (2004) · Zbl 1073.68001 · doi:10.1017/CBO9780511810275
[10] Ito, Qualitative analysis of gene regulatory networks by temporal logic, Theoretical Computer Science 594 pp 151– (2015) · Zbl 1329.92049 · doi:10.1016/j.tcs.2015.06.017
[11] Kroger, Temporal Logic and State Systems (2008)
[12] Li, Model checking of linear-time properties based on possibility measure, IEEE Transactions on Fuzzy Systems 21 (5) pp 842– (2013) · doi:10.1109/TFUZZ.2012.2232298
[13] Manna, Temporal Verification of Reactive Systems (1995) · Zbl 1288.68169
[14] Manna, The Temporal Logic of Reactive and Concurrent Systems: Specification (1995) · Zbl 0753.68003 · doi:10.1007/978-1-4612-4222-2
[15] Queille, Specification and verification of concurrent systems in CESAR, In: Proceedings 5th International Symposium on Programming 137 pp 337– (1982) · Zbl 0482.68028
[16] Shi, Lattice-valued modal propositional logic and its completeness, Science China Information Sciences 53 pp 2230– (2010) · Zbl 1219.03025 · doi:10.1007/s11432-010-4098-2
[17] Wang, A topological characterization of consistency of logic theories in propositional logic, Mathematical Logic Quarterly 52 pp 470– (2006) · Zbl 1112.03007 · doi:10.1002/malq.200610007
[18] Wang, Introduction to Mathematical Logic and Resolution Principle (2009)
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.