{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:57:35Z","timestamp":1725487055886},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540437871"},{"type":"electronic","value":"9783540480686"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-48068-4_22","type":"book-chapter","created":{"date-parts":[[2007,6,18]],"date-time":"2007-06-18T11:01:43Z","timestamp":1182164503000},"page":"374-393","source":"Crossref","is-referenced-by-count":1,"title":["Transition Refinement for Deriving a Distributed Minimum Weight Spanning Tree Algorithm"],"prefix":"10.1007","author":[{"given":"Sibylle","family":"Peuker","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,6]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Comput. Sci., 82:253\u2013284, 1991. previously: SRC Research Report 27, April 1988.","journal-title":"Theoretical Comput. Sci."},{"key":"22_CR2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F. B. Schneider. Defining liveness. Inf. Process. Lett., 21:181\u2013185, Oct. 1985.","journal-title":"Inf. Process. Lett."},{"key":"22_CR3","first-page":"12","volume":"31","author":"L. Castellano","year":"1987","unstructured":"L. Castellano, G. D. Michelis, and L. Pomello. Concurrency vs interleaving: an instructive example. EATCS Bulletin, 31:12\u201315, 1987.","journal-title":"EATCS Bulletin"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"C.-T. Chou and E. Gafni. Understanding and verifying distributed algorithms using stratified decomposition (extended abstract). In Proceedings of the 7th Annual Symposium on Principles of Distributed Computing, pages 44\u201365. ACM, 1988.","DOI":"10.1145\/62546.62556"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison, volume 47 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9780511663079"},{"issue":"3","key":"22_CR6","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T. Elrad","year":"1982","unstructured":"T. Elrad and N. Francez. Decomposition of distributed programs into communication-closed layers. Science of Computer Programming, 2(3):155\u2013173, 1982.","journal-title":"Science of Computer Programming"},{"issue":"1","key":"22_CR7","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/357195.357200","volume":"5","author":"R. G. Gallager","year":"1983","unstructured":"R. G. Gallager, P. A. Humblet, and P. M. Spira. A distributed algorithm for minimum-weight spanning trees. ACM Transactions on Programming Languages and Systems, 5(1):66\u201377, Jan. 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"12","key":"22_CR8","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1145\/359897.359903","volume":"20","author":"D. Gries","year":"1977","unstructured":"D. Gries. An exercise in proving parallel programs correct. Communication of the ACM, 20(12):921\u2013930, 1977.","journal-title":"Communication of the ACM"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"W. H. Hesselink. The incremental design of a distributed spanning tree algorithm. Formal Aspects of Computing, 11(E):(electronic archive), 1999.","DOI":"10.1007\/s001650050035"},{"key":"22_CR10","series-title":"PhD thesis","volume-title":"Layered Design of Parallel Systems","author":"W. Janssen","year":"1994","unstructured":"W. Janssen. Layered Design of Parallel Systems. PhD thesis, University Twente, Enschede, 1994."},{"key":"22_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-54430-5_96","volume-title":"CONCUR\u2019 91","author":"W. Janssen","year":"1991","unstructured":"W. Janssen, M. Poel, and J. Zwiers. Action systems and action refinement in the development of parallel systems. In J. C. M. Baeten and J. F. Groote, editors, CONCUR\u2019 91, volume 527 of LNCS, pages 298\u2013316, 1991."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"W. Janssen and J. Zwiers. From sequential layers to distributed processes, deriving a distributed minimum weight spanning tree algorithm (extended abstract). In Proceedings of the 11th Annual Symposium on Principles of Distributed Computing, pages 215\u2013227. ACM, 1992.","DOI":"10.1145\/135419.135461"},{"issue":"1-2","key":"22_CR13","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/S0304-3975(00)00205-X","volume":"262","author":"E. Kindler","year":"2001","unstructured":"E. Kindler and H. V\u00f6lzer. Algebraic nets with flexible arcs. Theoretical Computer Science, 262(1-2):285\u2013310, 2001.","journal-title":"Theoretical Computer Science"},{"key":"22_CR14","unstructured":"E. Kindler and M. Weber. The petri net kernel. In K. H. Mortensen, editor, Tool Demonstrations, ICAPTN 99, pages 71\u201375, 1999."},{"key":"22_CR15","unstructured":"S. Peuker. Phased decomposition of distributed algorithms. Informatik-Bericht 120, Humboldt-Universit\u00e4t zu Berlin, 1999."},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"S. Peuker. Property preserving transition refinement with concurrent runs: An example. In International Conference on Application of Concurrency to System Design, pages 77\u201386. IEEE Computer Society, 2001.","DOI":"10.1109\/CSD.2001.981766"},{"key":"22_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Petri Net Technology for Communication Based Systems","author":"S. Peuker","year":"2002","unstructured":"S. Peuker. Concurrency based transition refinement for the verification of distributed algorithms. In H. Ehrig, W. Reisig, G. Rozenberg, and H. Weber, editors, Petri Net Technology for Communication Based Systems, LNCS. Springer, 2002. To appear."},{"key":"22_CR18","unstructured":"S. Peuker. Deriving a distributed minimum weight spanning tree algorithm with transition refinement for Algebraic Petri nets. Technical Report 02-10, Software Verification Research Centre, The University of Queensland, March 2002."},{"key":"22_CR19","unstructured":"S. Peuker. Halbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen. PhD thesis, Humboldt-Universit\u00e4t zu Berlin, available via http:\/\/dochost.rz.hu-berlin.de\/abstract.php3\/dissertationen\/peuker-sibylle-2001-07-03"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"W. Reisig. Petri Nets and Algebraic Specifications. Theoretical Computer Science, 80:1\u201334, May 1991.","DOI":"10.1016\/0304-3975(91)90203-E"},{"key":"22_CR21","unstructured":"F. A. Stomp. Design and Verification of Distributed Network Algorithms: Foundations and Applications. PhD thesis, Technische Universiteit Eindhoven, 1989."},{"key":"22_CR22","unstructured":"F. A. Stomp and W. P. de Roever. A correctness proof of a distributed minimum-weight spanning tree algorithm (extended abstract). In Proceedings of the 7th International Conference on Distributed Computing Systems, pages 440\u2013447. ACM, 1987."},{"key":"22_CR23","first-page":"1","volume":"6E","author":"F. A. Stomp","year":"1994","unstructured":"F. A. Stomp and W. P. de Roever. Principles for sequential reasoning about distributed algorithms. Formal Aspects of Computing, 6E:1\u201370, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"22_CR24","unstructured":"J. L. Welch. Topics in Distributed Computing. PhD thesis, MIT\/LCS\/TM-361, 1988."},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"J. L. Welch, L. Lamport, and N. Lynch. A lattice-structured proof technique applied to a minimum spanning tree algorithm (extended abstract). In Proceedings of the 7th Annual Symposium on Principles of Distributed Computing, pages 28\u201343. ACM, 1988.","DOI":"10.21236\/ADA198312"},{"key":"22_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/3-540-49213-5_24","volume-title":"Compositionality: The Significant Difference, Proc. of COMPOS\u2019 97","author":"J. Zwiers","year":"1998","unstructured":"J. Zwiers. Compositional transformational design for concurrent systems. In W.-P. de Roever, H. Langmaack, and A. Pnueli, editors, Compositionality: The Significant Difference, Proc. of COMPOS\u2019 97, volume 1536 of LNCS, pages 609\u2013631. Springer-Verlag, 1998."}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48068-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T03:59:09Z","timestamp":1556510349000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48068-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540437871","9783540480686"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-48068-4_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}