{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T08:44:09Z","timestamp":1648716249988},"reference-count":23,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2017,7,4]],"date-time":"2017-07-04T00:00:00Z","timestamp":1499126400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/about_us\/legal\/notices"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,5,1]]},"DOI":"10.1093\/comjnl\/bxx064","type":"journal-article","created":{"date-parts":[[2017,6,9]],"date-time":"2017-06-09T11:08:11Z","timestamp":1497006491000},"page":"629-644","source":"Crossref","is-referenced-by-count":0,"title":["Partial Order Reduction for the full Class of State\/Event Linear Temporal Logic"],"prefix":"10.1093","volume":"61","author":[{"given":"Shuanglong","family":"Kan","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China"}]},{"given":"Zhiqiu","family":"Huang","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China"}]}],"member":"286","published-online":{"date-parts":[[2017,7,4]]},"reference":[{"key":"key\n\t\t\t\t20180425035430_bxx064C1","first-page":"52","volume-title":"Logics of Programs, Yorktown Heights, New York, May, Lecture Notes in Computer Science","author":"Clarke","year":"1981"},{"key":"key\n\t\t\t\t20180425035430_bxx064C2","first-page":"337","volume-title":"Int. Symposium on Programming, 5th Colloquium, Torino, Italy, 6\u20138 April, Lecture Notes in Computer Science","author":"Queille","year":"1982"},{"key":"key\n\t\t\t\t20180425035430_bxx064C3","doi-asserted-by":"crossref","first-page":"21:1","DOI":"10.1145\/1592434.1592438","article-title":"Software model checking","volume":"41","author":"Jhala","year":"2009","journal-title":"ACM Comput. Surv."},{"key":"key\n\t\t\t\t20180425035430_bxx064C4","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1007\/s00165-005-0071-z","article-title":"Concurrent Software Verification with States, Events, and Deadlocks","volume":"17","author":"Chaki","year":"2005","journal-title":"Formal Asp. Comput."},{"key":"key\n\t\t\t\t20180425035430_bxx064C5","volume-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"key\n\t\t\t\t20180425035430_bxx064C6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"Huth","year":"2004"},{"key":"key\n\t\t\t\t20180425035430_bxx064C7","first-page":"409","volume-title":"Computer Aided Verification (CAV1993), Elounda, Greece, 28 June\u20131 July, Lecture Notes in Computer Science","author":"Peled","year":"1993"},{"key":"key\n\t\t\t\t20180425035430_bxx064C8","first-page":"491","volume-title":"10th Int. Conf. Applications and Theory of Petri Nets, Bonn, Germany, June, Lecture Notes in Computer Science","author":"Valmari","year":"1989"},{"key":"key\n\t\t\t\t20180425035430_bxx064C9","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1006\/inco.1994.1035","article-title":"A Partial Approach to Model Checking","volume":"110","author":"Godefroid","year":"1994","journal-title":"Inf. Comput."},{"key":"key\n\t\t\t\t20180425035430_bxx064C10","doi-asserted-by":"crossref","first-page":"877","DOI":"10.1016\/j.scico.2010.02.008","article-title":"Partial Order Reduction for State\/event LTL with Application to Component-Interaction Automata","volume":"76","author":"Benes","year":"2011","journal-title":"Sci. Comput. Program."},{"key":"key\n\t\t\t\t20180425035430_bxx064C11","first-page":"307","volume-title":"7th Int. Conf. Integrated Formal Methods, IFM 2009, D\u00fcsseldorf, Germany, 16\u201319 February, Lecture Notes in Computer Science","author":"Benes","year":"2009"},{"key":"key\n\t\t\t\t20180425035430_bxx064C12","first-page":"329","volume-title":"18th Int. Conf. Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, 14\u201318 November, Lecture Notes in Computer Science","author":"Kan","year":"2016"},{"key":"key\n\t\t\t\t20180425035430_bxx064C13","doi-asserted-by":"crossref","DOI":"10.1093\/logcom\/exw004","article-title":"Partial Order Reduction for Checking LTL Formulae with the Next-Time Operator","author":"Kan","year":"2016","journal-title":"Journal of Logic and Computation"},{"key":"key\n\t\t\t\t20180425035430_bxx064C14","first-page":"5","volume-title":"Formal Methods and Software Engineering, 10th Int. Conf. Formal Engineering Methods, ICFEM 2008, Kitakyushu City, Japan, 27\u201331 October, Lecture Notes in Computer Science","author":"Sun","year":"2008"},{"key":"key\n\t\t\t\t20180425035430_bxx064C15","first-page":"70","volume-title":"Proc. Conf. Design, Automation and Test in Europe: Designers\u2019 Forum, DATE 2006, Munich, Germany, 6\u201310 March","author":"Das","year":"2006"},{"key":"key\n\t\t\t\t20180425035430_bxx064C16","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/s00165-014-0311-1","article-title":"Language and tool support for event refinement structures in event-b","volume":"27","author":"Fathabadi","year":"2015","journal-title":"Formal Asp. Comput."},{"key":"key\n\t\t\t\t20180425035430_bxx064C17","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The Model Checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans. Software Eng."},{"key":"key\n\t\t\t\t20180425035430_bxx064C18","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann","year":"2004"},{"key":"key\n\t\t\t\t20180425035430_bxx064C19","first-page":"53","volume-title":"Int. Confer. Computer Aided Verification (CAV2001), Paris, France, 18\u201322 July, Lecture Notes in Computer Science","author":"Gastin","year":"2001"},{"key":"key\n\t\t\t\t20180425035430_bxx064C20","first-page":"95","volume-title":"18th Tools and Algorithms for the Construction and Analysis of Systems (TACAS2012), Tallinn, Estonia, 24 March\u20131 April, LNCS","author":"Babiak","year":"2012"},{"key":"key\n\t\t\t\t20180425035430_bxx064C21","volume-title":"Design and Validation of Computer Protocols","author":"Holzmann","year":"1990"},{"key":"key\n\t\t\t\t20180425035430_bxx064C22","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/s100090050045","article-title":"Formalization and Validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN","volume":"2","author":"Kamel","year":"2000","journal-title":"STTT"},{"key":"key\n\t\t\t\t20180425035430_bxx064C23","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial","year":"2010"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/article-pdf\/61\/5\/629\/24724528\/bxx064.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T20:49:50Z","timestamp":1569444590000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article\/61\/5\/629\/3920737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,4]]},"references-count":23,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2017,7,4]]},"published-print":{"date-parts":[[2018,5,1]]}},"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxx064","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"value":"0010-4620","type":"print"},{"value":"1460-2067","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2018,5]]},"published":{"date-parts":[[2017,7,4]]}}}