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 LTLn, 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 LTL formula has an equivalent formula in temporal normal form.
BaierC. and KatoenJ.P., Principles of Model Checking, MIT Press, 2008.
2.
BlackburnP., de RijkeM. and VenemaY., , , Modal Logic,
Cambridge University PressNew York, 2001.
3.
ClarkeE.M. and EmersonE.A., Design and synthesis of synchronization skeletons using branching time temporal logic, In: Logic ofrograms, LNCS131, 1981, pp. 52–71.
4.
ClarkeE.M., GrumbergO. and PeledD., Model Checking, MIT Press1999.
5.
ClarkeE.M. and KurshanR., Computer-aided verification, IEEE Spectrum33(6) (1996), 61–67.
6.
DingX.C., SmithS.L., BeltaC., et al., Optimal control of Markov decision processes with linear temporal logic constraints, IEEE Transactions on Automatic Control59(5) (2014), 1244–1257.
7.
FengY., YuN.K. and YingM.S., Model checking quantum Markov chains, Journal of Computer and System Sciences79 (2013), 1181–1198.
8.
GotzheinR., Temporal logic and applications: A tutorial, Computer Networks and ISDN Systems24(3) (1992), 203–218.
9.
HuthM. and RyanM., Logic in Computer Science-Modelling and Reasoning about Systems (2nd ed.), Cambridge University Press, Cambridge, 2004.
10.
ItoS., IchinoseT., ShimakawaM., et al., Qualitative analysis of gene regulatory networks by temporal logic, Theoretical Computer Science594 (2015), 151–179.
11.
KrogerF. and MerzS., Temporal Logic and State Systems, Springer-Verlag, Berlin2008.
12.
LiY.M. and LiL.J., Model checking of linear-time properties based on possibility measure, IEEE Transactions on Fuzzy Systems21(5) (2013), 842–854.
13.
MannaZ. and PnueliA., Temporal Verification of Reactive Systems, Springer-Verlag, New York1995.
14.
MannaZ. and PnueliA., The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York,
1995.
15.
QueilleJ.P. and SifakisJ., Specification and verification of concurrent systems in CESAR, In: Proceedings 5th International Symposium on Programming, LNCS137, 1982, pp. 337–351.
16.
ShiH.X. and WangG.J., Lattice-valued modal propositional logic and its completeness, Science China Information Sciences53 (2010), 2230–2239.
17.
WangG.J. and SheY.H., A topological characterization of consistency of logic theories in propositional logic, Mathematical Logic Quarterly52 (2006), 470–477.
18.
WangG.J. and ZhouH.J., Introduction to Mathematical Logic and Resolution Principle, Science Press, Beijing, U.K. Alpha Science International Limited, Oxford, 2009.
