{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:45Z","timestamp":1725514905710},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540688549"},{"type":"electronic","value":"9783540688556"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-68855-6_6","type":"book-chapter","created":{"date-parts":[[2008,5,31]],"date-time":"2008-05-31T05:18:13Z","timestamp":1212211093000},"page":"84-98","source":"Crossref","is-referenced-by-count":1,"title":["Adapting Petri Nets Reductions to Promela Specifications"],"prefix":"10.1007","author":[{"given":"C.","family":"Pajault","sequence":"first","affiliation":[]},{"given":"J. -F.","family":"Pradat-Peyre","sequence":"additional","affiliation":[]},{"given":"P.","family":"Rousseau","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/3-540-57208-2_17","volume-title":"CONCUR\u201993","author":"P. Wolper","year":"1993","unstructured":"Wolper, P., Godefroid, P.: Partial-order methods for temporal verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 233\u2013246. Springer, Heidelberg (1993)"},{"issue":"2","key":"6_CR2","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Form. Methods Syst. Des.\u00a02(2), 149\u2013164 (1993)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Computer Aided Verification","author":"A. Valmari","year":"1993","unstructured":"Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 397\u2013408. Springer, Heidelberg (1993)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-56922-7_38","volume-title":"Computer Aided Verification","author":"A. Emerson","year":"1993","unstructured":"Emerson, A., Prasad Sistl, A.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 463\u2013478. Springer, Heidelberg (1993)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.P. Sistla","year":"2002","unstructured":"Sistla, A.P.: Symmetry reductions in model-checking. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575. Springer, Heidelberg (2002)"},{"key":"6_CR6","unstructured":"Haddad, S., Pradat-Peyre, J.: Efficient reductions for LTL formulae verification. Technical report, CEDRIC, CNAM, Paris (2004)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Haddad, S., Pradat-Peyre, J.F.: New coloured reductions for software validation. In: Workshop on Discrete Event Systems (2004)","DOI":"10.1016\/S1474-6670(17)30770-X"},{"issue":"1","key":"6_CR8","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1142\/S0129626406002502","volume":"16","author":"S. Haddad","year":"2006","unstructured":"Haddad, S., Pradat-Peyre, J.-F.: New efficient petri nets reductions for parallel programs verification. Parallel Processing Letters\u00a016(1), 101\u2013116 (2006)","journal-title":"Parallel Processing Letters"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2003","author":"S. Evangelista","year":"2003","unstructured":"Evangelista, S., Kaiser, C., Pradat-Peyre, J.F., Rousseau, P.: Quasar: a new tool for analysing concurrent programs. In: Rosen, J.-P., Strohmeier, A. (eds.) Ada-Europe 2003. LNCS, vol.\u00a02655. Springer, Heidelberg (2003)"},{"issue":"5","key":"6_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"Software Engineering"},{"key":"6_CR11","unstructured":"Pajault, C., Pradat-Peyre, J.: Static reductions for promela specifications. Technical Report 1005, Conservatoire National des Arts et M\u00e9tiers, laboratoire Cedric, Paris, France (2006)"},{"key":"6_CR12","unstructured":"http:\/\/quasar.cnam.fr\/atomicSpin\/"},{"issue":"12","key":"6_CR13","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM\u00a018(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: International Conference on Concurrency Theory, pp. 317\u2013331 (1998)","DOI":"10.1007\/BFb0055631"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S.D. Stoller","year":"2003","unstructured":"Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619. Springer, Heidelberg (2003)"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/781131.781169","volume-title":"Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp. 338\u2013349. ACM Press, New York (2003)"},{"key":"6_CR17","volume-title":"Electronic Notes in Theoretical Computer Science","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Transactions for software model checking. In: Cook, B., Stoller, S., Visser, W. (eds.) Electronic Notes in Theoretical Computer Science, vol.\u00a089. Elsevier, Amsterdam (2003)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Haddad, S., Pradat-Peyre, J.: Coloured Petri nets reductions for concurrent software validation. Technical report, CEDRIC, CNAM, Paris (2004)","DOI":"10.1016\/S1474-6670(17)30770-X"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Petri nets","author":"G. Berthelot","year":"1985","unstructured":"Berthelot, G.: Checking properties of nets using transformations. In: Rozenberg, G. (ed.) Advances in Petri nets. LNCS, vol.\u00a0222. Springer, Heidelberg (1985)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44988-4_22","volume-title":"Application and Theory of Petri Nets 2000","author":"D. Poitrenaud","year":"2000","unstructured":"Poitrenaud, D., Pradat-Peyre, J.: Pre and post-agglomerations for $\\mathit{LTL}$ model checking. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68855-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T16:30:19Z","timestamp":1557592219000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68855-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540688549","9783540688556"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68855-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}