{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T04:10:32Z","timestamp":1748923832061,"version":"3.41.0"},"reference-count":41,"publisher":"Oxford University Press (OUP)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"DOI":"10.1093\/logcom\/exw004","type":"journal-article","created":{"date-parts":[[2016,5,4]],"date-time":"2016-05-04T01:44:01Z","timestamp":1462326241000},"page":"exw004","source":"Crossref","is-referenced-by-count":4,"title":["Partial order reduction for checking LTL formulae with the next-time operator"],"prefix":"10.1093","author":[{"given":"Shuanglong","family":"Kan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiqiu","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhe","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weiwei","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yutao","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2016,5,3]]},"reference":[{"key":"2016050318434390000_exw004v1.1","doi-asserted-by":"crossref","unstructured":"Babiak T. K\u0159et\u00ednsk\u00fd M. \u0158eh\u00e1k V. Strej\u010dek J. Flanagan C. K\u00f6nig B. . LTL to B\u00fcchi automata translation: fast and more deterministic. In 18th Tools and Algorithms for the Construction and Analysis of Systems (TACAS2012), Vol. 7214 of LNCS, pp. 95\u2013109. Springer, 2012.","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"2016050318434390000_exw004v1.2","unstructured":"Baier C. Katoen J.-P. . Principles of Model Checking. MIT Press, 2008."},{"key":"2016050318434390000_exw004v1.3","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0071-z"},{"key":"2016050318434390000_exw004v1.4","doi-asserted-by":"crossref","unstructured":"Chechik M. Paun D.O. Dams D. Gerth R. Leue S. Massink M. . Events in property patterns. In 6th International SPIN Workshops, Vol. 1680 of Lecture Notes in Computer Science, pp. 154\u2013167. Springer, 1999.","DOI":"10.1007\/3-540-48234-2_13"},{"key":"2016050318434390000_exw004v1.5","doi-asserted-by":"crossref","unstructured":"Clarke E. Kroening D. Yorav K. . Behavioral consistency of C and verilog programs using bounded model checking. In 40th Design Automation Conference (DAC 2003), pp. 368\u2013371. ACM, 2003.","DOI":"10.1145\/775832.775928"},{"key":"2016050318434390000_exw004v1.6","doi-asserted-by":"crossref","unstructured":"Clarke E.M. Allen Emerson E. Kozen D. . Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, Vol. 131 of Lecture Notes in Computer Science, pp. 52\u201371. Springer, 1981.","DOI":"10.1007\/BFb0025774"},{"key":"2016050318434390000_exw004v1.7","unstructured":"Clarke E.M. Grumberg O. Peled D.A. . Model Checking. MIT Press, 1999."},{"key":"2016050318434390000_exw004v1.8","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1145\/1810295.1810396","article-title":"SMT-based bounded model checking for multi-threaded software in embedded systems","volume-title":"32nd ACM\/IEEE International Conference on Software Engineering (ICSE2010)","volume":"2","author":"Cordeiro","year":"2010"},{"key":"2016050318434390000_exw004v1.9","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"2016050318434390000_exw004v1.10","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1142\/9789814271059_0015","article-title":"Specification and verification using temporal logics","volume-title":"Modern Applications of Automata Theory, IISc Research Monographs Series","volume":"2","author":"Demri","year":"2012"},{"key":"2016050318434390000_exw004v1.11","doi-asserted-by":"crossref","unstructured":"Dotti F.L. Foss L. Ribeiro L. Marchi dos Santos O. Najm E. Nestmann U. Stevens P. . Verification of distributed object-based systems. In Formal Methods for Open Object-Based Distributed Systems, 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, 19.21, November 2003, Proceedings, Vol. 2884 of Lecture Notes in Computer Science, pp. 261\u2013275. Springer, 2003.","DOI":"10.1007\/978-3-540-39958-2_18"},{"key":"2016050318434390000_exw004v1.12","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A. Poitrenaud D. . SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata. In 12th Annual Internatinal Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS 2004), D. DeGroot and P. Harrison, eds, pp. 76-83. IEEE, 2004.","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"2016050318434390000_exw004v1.13","doi-asserted-by":"crossref","unstructured":"Dwyer M.B. Avrunin G.S. Corbett J.C. Boehm B.W. Garlan D. Kramer J. . Patterns in property specifications for finite-state verification. In Proceedings of the 1999 International Conference on Software Engineering, ICSE' 99, Los Angeles, CA, USA, 16-22, May 1999, pp. 411\u2013420. ACM, 1999.","DOI":"10.1145\/302405.302672"},{"key":"2016050318434390000_exw004v1.14","doi-asserted-by":"crossref","unstructured":"Gastin P. Oddoux D. Berry G. Comon H. Finkel A. . Fast LTL to B\u00fcchi automata translation. In Computer Aided Verification (CAV2001), Vol. 2102 of LNCS, pp. 53\u201365. Springer, 2001.","DOI":"10.1007\/3-540-44585-4_6"},{"key":"2016050318434390000_exw004v1.15","unstructured":"Godefroid P. . Partial-Order Methods for the Verification of Concurrent Systems. PhD Thesis, University of Liege, Place du 20 Ao\u00fbt 7, 4000 Li\u00e8ge, 1994."},{"key":"2016050318434390000_exw004v1.16","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1035"},{"key":"2016050318434390000_exw004v1.17","unstructured":"Holzmann G.J. . Design and Validation of Computer Protocols. Prentice Hall, 1990."},{"key":"2016050318434390000_exw004v1.18","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"2016050318434390000_exw004v1.19","unstructured":"Holzmann G.J. . The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004."},{"key":"2016050318434390000_exw004v1.20","doi-asserted-by":"crossref","unstructured":"Holzmann G.J. Kupferman O. Gr\u00e8goire J.-C. . Not checking for closure under stuttering. In Proceeding of the 2nd Spin Workshop, The Spin Verification System, pp. 17\u201322. American Mathematical Society, 1996.","DOI":"10.1090\/dimacs\/032\/02"},{"key":"2016050318434390000_exw004v1.21","doi-asserted-by":"crossref","unstructured":"Holzmann G.J. Peled D. Hogrefe D. Leue S. . An improvement in formal verification. In Formal Description Techniques VII, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques, Berne, Switzerland, 1994, Vol. 6 of IFIP Conference Proceedings, pp. 197\u2013211. Chapman & Hall, 1994.","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"2016050318434390000_exw004v1.22","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050045"},{"key":"2016050318434390000_exw004v1.23","unstructured":"Kr\u00f6ger F. Merz S. . Temporal Logic and State Systems. Springer, 2008."},{"key":"2016050318434390000_exw004v1.24","unstructured":"Kucera A. Strejcek J. Bradfield J.C. . The stuttering principle revisited: on the expressiveness of nested X and U operators in the logic LTL. In Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, 22-25, September 2002, Proceedings, Vol. 2471 of Lecture Notes in Computer Science, pp. 276\u2013291. Springer, 2002."},{"key":"2016050318434390000_exw004v1.25","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0164-4"},{"key":"2016050318434390000_exw004v1.26","unstructured":"Lamport L. Mason R.E.A. . What good is temporal logic? In Information Processing, pp. 657\u2013668. Elsevier Science, North-Holland, 1983."},{"key":"2016050318434390000_exw004v1.27","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"2016050318434390000_exw004v1.28","unstructured":"Lamport L. . Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"key":"2016050318434390000_exw004v1.29","doi-asserted-by":"crossref","unstructured":"Lewerentz C. Lindner T. , eds. In Formal Development of Reactive Systems \u2014 Case Study Production Cell, Vol. 891 of Lecture Notes in Computer Science. Springer, 1995.","DOI":"10.1007\/3-540-58867-1"},{"key":"2016050318434390000_exw004v1.30","doi-asserted-by":"crossref","unstructured":"Merz S. Wing J.M. Woodcock J. Davies J. . A more complete TLA. In FM'99 \u2014 Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, 20-24, September 1999, Proceedings, Volume II, Vol. 1709 of Lecture Notes in Computer Science, pp. 1226\u20131244. Springer, 1999.","DOI":"10.1007\/3-540-48118-4"},{"key":"2016050318434390000_exw004v1.31","doi-asserted-by":"crossref","unstructured":"Muller D.E. Schupp P.E. Nivat M. Perrin D. . Alternating automata on infinite objects, determinacy and rabin's theorem. In Automata on Infinite Words, Ecole de Printemps d'Informatique Th\u00e9orique, Le Mont Dore, 14-18, May 1984, Vol. 192 of Lecture Notes in Computer Science, pp. 100\u2013107. Springer, 1984.","DOI":"10.1007\/3-540-15641-0_27"},{"key":"2016050318434390000_exw004v1.32","unstructured":"Musuvathi M. Engler D.R. Anderson E. Burgess M. Couch A. . Model checking large network protocol implementations. In 1st Symposium on Networked Systems Design and Implementation (NSDI 2004), pp. 155\u2013168. USENIX, 2004."},{"key":"2016050318434390000_exw004v1.33","doi-asserted-by":"crossref","unstructured":"Paun D.O. Chechik M. . Events in linear-time properties. In 4th IEEE International Symposium on Requirements Engineering (RE '99), 7-11 June 1999, Limerick, Ireland, pp. 123\u2013132. IEEE Computer Society, 1999.","DOI":"10.1109\/ISRE.1999.777992"},{"key":"2016050318434390000_exw004v1.34","doi-asserted-by":"crossref","unstructured":"Peled D. Courcoubetis C. . All from one, one for all: on model checking using representatives. In Computer Aided Verification (CAV1993), Vol. 697 of LNCS, pp. 409\u2013423. Springer, 1993.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"2016050318434390000_exw004v1.35","doi-asserted-by":"crossref","unstructured":"Peled D. Gunter E.L. Felty A.P. . Verification for robust specification. In Conference on Theorem Proving in Higher Order Logic, pp. 231\u2013241. LNCS, Springer, 1997.","DOI":"10.1007\/BFb0028397"},{"key":"2016050318434390000_exw004v1.36","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(97)00133-6"},{"key":"2016050318434390000_exw004v1.37","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00219-3"},{"key":"2016050318434390000_exw004v1.38","doi-asserted-by":"crossref","unstructured":"Queille J.-P. Sifakis J. Dezani-Ciancaglini M. Montanari U. . Specification and verification of concurrent systems in CESAR. In International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, 1982, Proceedings, Vol. 137 of Lecture Notes in Computer Science, pp. 337\u2013351. Springer, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"2016050318434390000_exw004v1.39","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"2016050318434390000_exw004v1.40","doi-asserted-by":"crossref","unstructured":"Valmari A. Rozenberg G. . Stubborn sets for reduced state space generation. In Advances in Petri Nets 1990, Vol. 483 of Lecture Notes in Computer Science, pp. 491\u2013515. Springer Berlin Heidelberg, 1991.","DOI":"10.1007\/3-540-53863-1_36"},{"key":"2016050318434390000_exw004v1.41","doi-asserted-by":"publisher","DOI":"10.1007\/BF00709154"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/27\/4\/1095\/17660128\/exw004.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T00:08:12Z","timestamp":1748909292000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/exw004"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5,3]]},"references-count":41,"alternative-id":["10.1093\/logcom\/exw004"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/exw004","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published":{"date-parts":[[2016,5,3]]}}}