{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T00:08:12Z","timestamp":1770682092363,"version":"3.49.0"},"reference-count":18,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2015,11,14]],"date-time":"2015-11-14T00:00:00Z","timestamp":1447459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Intelligent &amp; Fuzzy Systems"],"published-print":{"date-parts":[[2016,3]]},"abstract":"<jats:p>\n                    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                    <jats:sub>\n                      <jats:italic>n<\/jats:italic>\n                    <\/jats:sub>\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 LTL formula has an equivalent formula in temporal normal form.\n                  <\/jats:p>","DOI":"10.3233\/ifs-151874","type":"journal-article","created":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T10:47:51Z","timestamp":1456829271000},"page":"1657-1662","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Temporal normal form for Linear Temporal Logic formulae"],"prefix":"10.1177","volume":"30","author":[{"given":"Hui-Xian","family":"Shi","sequence":"first","affiliation":[{"name":"College of Mathematics and Information Science, Shaanxi Normal University, South Chang\u2019an Road, Yanta District, Xi\u2019an, P.R. China"}]},{"given":"Yong-Ming","family":"Li","sequence":"additional","affiliation":[{"name":"College of Computer Science, Shaanxi Normal University, West Chang\u2019an Avenue, Chang\u2019an District, Xi\u2019an,  P.R. China"}]}],"member":"179","published-online":{"date-parts":[[2015,11,14]]},"reference":[{"key":"e_1_3_1_2_2","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"BaierC. and KatoenJ.P., Principles of Model Checking, MIT Press, 2008."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_3_1_4_2","first-page":"52","article-title":"In: Logic ofrograms, LNCS","volume":"131","author":"Clarke E.M.","year":"1981","unstructured":"ClarkeE.M. and EmersonE.A., Design and synthesis of synchronization skeletons using branching time temporal logic, In: Logic ofrograms, LNCS 131, 1981, pp. 52\u201371.","journal-title":"Design and synthesis of synchronization skeletons using branching time temporal logic"},{"key":"e_1_3_1_5_2","volume-title":"Model Checking","author":"Clarke E.M.","year":"1999","unstructured":"ClarkeE.M., GrumbergO. and PeledD., Model Checking, MIT Press 1999."},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/6.499951"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2298143"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(92)90109-4"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.06.017"},{"key":"e_1_3_1_12_2","volume-title":"Temporal Logic and State Systems","author":"Kroger F.","year":"2008","unstructured":"KrogerF. and MerzS., Temporal Logic and State Systems, Springer-Verlag, Berlin 2008."},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2012.2232298"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_3_1_16_2","first-page":"337","article-title":"Specification and verification of concurrent systems in CESAR","volume":"137","author":"Queille J.P.","year":"1982","unstructured":"QueilleJ.P. and SifakisJ., Specification and verification of concurrent systems in CESAR, In: Proceedings 5th International Symposium on Programming, LNCS 137, 1982, pp. 337\u2013351.","journal-title":"In: Proceedings 5th International Symposium on Programming"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-010-4098-2"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610007"},{"key":"e_1_3_1_19_2","volume-title":"Introduction to Mathematical Logic and Resolution Principle","author":"Wang G.J.","year":"2009","unstructured":"WangG.J. and ZhouH.J., Introduction to Mathematical Logic and Resolution Principle, Science Press, Beijing, U.K. Alpha Science International Limited, Oxford, 2009."}],"container-title":["Journal of Intelligent &amp; Fuzzy Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/IFS-151874","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/IFS-151874","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/IFS-151874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T06:49:23Z","timestamp":1770619763000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/IFS-151874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,14]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["10.3233\/IFS-151874"],"URL":"https:\/\/doi.org\/10.3233\/ifs-151874","relation":{},"ISSN":["1064-1246","1875-8967"],"issn-type":[{"value":"1064-1246","type":"print"},{"value":"1875-8967","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11,14]]}}}