{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T08:50:47Z","timestamp":1766047847003},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10703-005-4592-0","type":"journal-article","created":{"date-parts":[[2005,2,15]],"date-time":"2005-02-15T10:47:35Z","timestamp":1108464455000},"page":"7-25","source":"Crossref","is-referenced-by-count":3,"title":["Deciding Global Partial-Order Properties"],"prefix":"10.1007","volume":"26","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Ken","family":"McMillan","sequence":"additional","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1109\/LICS.1996.561322","volume-title":"LICS96, 11th IEEE Symposium on Logic in Computer Science","author":"R. Alur","year":"1996","unstructured":"R. Alur, K. McMillan, and D. Peled, ?model-checking of correctness conditions for concurrent objects,? in LICS96, 11th IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, USA, 1996, pp. 219?228."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, W. Penczek, and D. Peled, ?Model-checking of causality properties,? in 10th Symposium on Logic in Computer Science, 1995, pp. 90?100.","DOI":"10.1109\/LICS.1995.523247"},{"key":"CR3","unstructured":"W. Ebinger, ?Logical definability of trace languages,? in V. Diekert and G. Rozenberg (Eds.), The Book of Traces, World Scientific, 1995, pp. 382?390."},{"issue":"2","key":"CR4","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P. Godefroid","year":"1994","unstructured":"P. Godefroid and P. Wolper, ?A partial approach to model checking,? Information and Computation, Vol. 110, No. 2, pp. 305?326, 1994.","journal-title":"Information and Computation"},{"key":"CR5","first-page":"385","volume":"1102","author":"G. Holzmann","year":"1996","unstructured":"G. Holzmann and D. Peled, ?The state of SPIN,? in 8th Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 1102, 1996, pp. 385?389.","journal-title":"8th Conference on Computer-Aided Verification, Lecture Notes in Computer Science"},{"key":"CR6","first-page":"21","volume":"75","author":"S. Katz","year":"1992","unstructured":"S. Katz and D. Peled, ?Interleaving set temporal logic,? Theoretical Computer Science, Vol. 75, pp. 21?43, 1992.","journal-title":"Theoretical Computer Science"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, ?Checking that finite-state concurrent programs satisfy their linear specification,? in 11th ACM Symposium on Principles of Programming Languages, 1984, pp. 97?107.","DOI":"10.1145\/318593.318622"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1995.1078","volume":"119","author":"K. Lodaya","year":"1985","unstructured":"K. Lodaya, R. Parikh, R. Ramanujam, and P.S. Thiagarajan, ?A logical study of distributed transitions systems,? Information and Computation, Vol. 119, pp. 91?118, 1985.","journal-title":"Information and Computation"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"A. Mazurkiewicz, ?Trace theory,? in W. Brauer, W. Reisig, and G. Rozenberg (Eds.), Advances in Petri Nets 1986, Vol. 255, Lecture Notes in Computer Science, 1987, pp. 279?324.","DOI":"10.1007\/3-540-17906-2_30"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, ?Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits,? in 4th Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 663, 1992, pp. 164?177.","DOI":"10.1007\/3-540-56496-9_14"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"D. Peled, ?Combining partial order reductions with on-the-fly model checking,? in Proc. 6th Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 818, 1994, pp. 377?390.","DOI":"10.1007\/3-540-58179-0_69"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"W. Penczek and R. Kuiper, ?Traces and logic,? in V. Diekert and G. Rozenberg (Eds.), The Book of Traces, World Scientific, 1995, pp. 307?390.","DOI":"10.1142\/9789814261456_0010"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/0020-0190(92)90007-I","volume":"43","author":"W. Penczek","year":"1992","unstructured":"W. Penczek, ?On undecidability of propositional temporal logics on trace systems,? Information Processing Letters, Vol. 43, pp. 147?153, 1992.","journal-title":"Information Processing Letters"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0304-3975(94)90009-4","volume":"126","author":"D. Peled","year":"1994","unstructured":"D. Peled and A. Pnueli, ?Proving partial order properties,? Theoretical Computer Science, Vol. 126, pp. 143?182, 1994.","journal-title":"Theoretical Computer Science"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"S. Pinter and P. Wolper, ?A temporal logic for reasoning about partially ordered computations,? in 3rd ACM Symposium on Principles of Distributed Computing, 1984, pp. 28?37.","DOI":"10.1145\/800222.806733"},{"issue":"1","key":"CR16","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF01379149","volume":"15","author":"V.R. Pratt","year":"1986","unstructured":"V.R. Pratt, ?Modeling concurrency with partial orders,? Intl. J. of Parallel Programming, Vol. 15, No. 1, pp. 33?71, 1986.","journal-title":"Intl. J. of Parallel Programming"},{"key":"CR17","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"W.J. Savitch, ?Relationship between nondeterministic and deterministic tape complexities,? J. on Computer and System Sciences, Vol. 4, pp. 177?192, 1970.","journal-title":"J. on Computer and System Sciences"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"P.S. Thiagarajan, ?A trace based extension of linear time temporal logic,? in Ninth Symposium on Logic in Computer Science, 1994, pp. 438?447.","DOI":"10.1109\/LICS.1994.316047"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"A. Valmari, ?A Stubborn attack on state explosion,? in Proc. 2nd Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 531, 1990, pp. 156?165.","DOI":"10.1007\/BFb0023729"},{"key":"CR20","unstructured":"M.Y. Vardi and P. Wolper, ?An automata-theoretic approach to automatic program verification,? in First Symposium on Logic in Computer Science, 1986, pp. 332?344."},{"issue":"5","key":"CR21","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"D. Peled and T. Wilke, ?Stutter invariant temporal properties are expressible without the next-time operator,? Information Processing Letters, Vol. 63, No. 5, pp. 243?246, 1997.","journal-title":"Information Processing Letters"},{"key":"CR22","first-page":"99","volume":"21","author":"W. Zielonka","year":"1987","unstructured":"W. Zielonka, ?Notes on finite asynchronous automata,? R.A.I.R.O.-Informatique Th\u00e9orique et. Applications, Vol. 21, pp. 99?135, 1987.","journal-title":"R.A.I.R.O.-Informatique Th\u00e9orique et. Applications"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-4592-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-005-4592-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-4592-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,2]],"date-time":"2023-05-02T05:07:00Z","timestamp":1683004020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-005-4592-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["4592"],"URL":"https:\/\/doi.org\/10.1007\/s10703-005-4592-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,1]]}}}