{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:23:10Z","timestamp":1759638190880},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1997,7,1]],"date-time":"1997-07-01T00:00:00Z","timestamp":867715200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1997,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            A technique to model and to verify distributed algorithms is suggested. This technique (based on Petri nets) reduces the modelling and analysis effort to a reasonable level. The paper outlines the technique using the example of a typical network algorithm, the\n            <jats:italic>echo algorithm<\/jats:italic>\n            .\n          <\/jats:p>","DOI":"10.1007\/bf01211299","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:18:43Z","timestamp":1109369923000},"page":"409-424","source":"Crossref","is-referenced-by-count":12,"title":["Petri net based verification of distributed algorithms: An example"],"prefix":"10.1145","volume":"9","author":[{"given":"Ekkart","family":"Kindler","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Humboldt-Universit\u00e4t zu Berlin, D-10099, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reisig","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Humboldt-Universit\u00e4t zu Berlin, D-10099, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hagen","family":"V\u00f6lzer","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Humboldt-Universit\u00e4t zu Berlin, D-10099, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Walter","sequence":"additional","affiliation":[{"name":"Fraunhofer Institute for Software and Systems Engineering, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Abadi M.: An axiomatization of Lamport's temporal logic of actions. SRC Research Report 65 Digital Equipment Corporation Systems Research Center October 1990."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Apt K. R. and Olderog E.-R.: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer-Verlag 1991.","DOI":"10.1007\/978-1-4757-4376-0"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Best E. Devillers R. and Hall F. G.: The box calculus: A new causal algebra with multi-label communication. In G. Rozenberg editor Advances in Petri nets 1992 volume 609 of LNCS pages 21\u201369. Springer-Verlag 1992.","DOI":"10.1007\/3-540-55610-9_167"},{"key":"e_1_2_1_2_4_2","unstructured":"Best E. and Grahlmann B.: ProjectPEP. http:\/\/www.informatik.unihildesheim.de\/ pep\/HomePage.html."},{"key":"e_1_2_1_2_5_2","unstructured":"Boug\u00e9 L.: Modularit\u00e9 et sym\u00e9trie pour les syst\u00e8mes r\u00e9partis; application au langage CSP. Rapport de Recherche 87-2 Lab. d'Informatique de L'Ecole Normale Superieure Paris 1987."},{"key":"e_1_2_1_2_6_2","unstructured":"Cu\u00e9llar J. Barnard D. and Huber M.: A solution relying on the model checking of boolean transition systems. In M. Broy S. Merz and K. Spies editors Formal Systems Specification The RPC-Memory Specification Case Study LNCS 1169."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1982.235573"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Chandy K. M. and Misra J.: Parallel Program Design: A Foundation. Addison-Wesley 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00117-4"},{"key":"e_1_2_1_2_10_2","unstructured":"Dijkstra E. W. and Scholten C. S.: Diffusing computations. Information Processing Letters 1981."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Grahlmann B. and Best E.: PEP \u2014 more than a Petri net tool. In T. Margaria and B. Steffen editors Tools and Algorithms for the Construction and Analysis of Systems TACAS LNCS 1055 pp. 397\u2013401. Springer-Verlag March 1996.","DOI":"10.1007\/3-540-61042-1_58"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/357195.357200"},{"key":"e_1_2_1_2_13_2","unstructured":"Jensen K.: Coloured Petri Nets volume 1 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag 1992."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/978-1-4471-3078-9_14","volume-title":"Structures in Concurrency Theory","author":"Kindler E.","year":"1995"},{"key":"e_1_2_1_2_15_2","unstructured":"Lamport L.: The temporal logic of actions. SRC Research Report 79 Digital Equipment Corporation Systems Research Center December 1991."},{"issue":"2","key":"e_1_2_1_2_16_2","first-page":"219","article-title":"An introduction to input\/output automata","volume":"3","author":"Lynch N.","year":"1989","journal-title":"CWI-Quarterly"},{"key":"e_1_2_1_2_17_2","unstructured":"Lynch N. A.: Distributed Algorihms. Morgan Kaufmann 1996."},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Reisig W.: Petri net models of distributed algorithms. In Jan van Leeuwen editor Computer Science Today: Recent Trends and Developments LNCS 1000 pp. 441\u2013454. Springer-Verlag 1995.","DOI":"10.1007\/BFb0015259"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Reisig W.: Modelling and verification of distributed algorithms. In Ugo Montanari and Vladimiro Sassone editors CONCUR'96: Concurrency Theory LNCS 1119 pp. 579\u2013595. Springer-Verlag 1996.","DOI":"10.1007\/3-540-61604-7_77"},{"key":"e_1_2_1_2_20_2","unstructured":"Raynal M. and Helary J.-M.: Synchronization and Control of Distributed Systems and Programs . Series in parallel computing. Wiley 1990."},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03259394"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1109\/TIT.1983.1056620","article-title":"Distributed network protocols","volume":"29","author":"Segall A.","year":"1983","journal-title":"IEEE Transactions on Information Theory"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Shavit N. and Francez N.: A new approach to detection of locally indicative stability. In L. Kott editor Proc. of th 13th ICALP LNCS 226 pp. 344\u2013358. Springer-Verlag 1986.","DOI":"10.1007\/3-540-16761-7_84"},{"key":"e_1_2_1_2_24_2","unstructured":"Tel G.: Introduction to Distributed Algorithms. Cambridge University Press 1994."},{"key":"e_1_2_1_2_25_2","unstructured":"Walter R. V\u00f6lzer H. Vesper T. Reisig W. Kindler E. Freiheit J. and Desel J.: Memorandum: Petrinetzmodelle zur Verifikation Verteilter Algorithmen. Informatik-Bericht 67 Humboldt-Universit\u00e4t zu Berlin July 1996."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211299.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211299\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:25:16Z","timestamp":1641482716000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211299"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,7]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1997,7]]}},"alternative-id":["10.1007\/BF01211299"],"URL":"https:\/\/doi.org\/10.1007\/bf01211299","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,7]]}}}