{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:27Z","timestamp":1760202507966},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1995,5,1]],"date-time":"1995-05-01T00:00:00Z","timestamp":799286400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input\/output automata; both safety and liveness properties are considered. A small but typical circuit is verified in both of these ways, first using forward simulations, an execution correspondence lemma, and a simple fairness argument, and second using deductions within the process algebra DIOA for I\/O automata. An extended evaluation and comparison of the two methods is given.<\/jats:p>","DOI":"10.1007\/bf01211073","type":"journal-article","created":{"date-parts":[[2005,2,24]],"date-time":"2005-02-24T15:57:58Z","timestamp":1109260678000},"page":"231-265","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A comparison of simulation techniques and algebraic techniques for verifying concurrent systems"],"prefix":"10.1145","volume":"7","author":[{"given":"Nancy","family":"Lynch","sequence":"first","affiliation":[{"name":"MIT-Laboratory for Computer Science, 545 Technology Square, 02139, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Segala","sequence":"additional","affiliation":[{"name":"MIT-Laboratory for Computer Science, 545 Technology Square, 02139, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Baeten J. C. M.: Applications of Process Algebra . Cambridge Tracts in Theoretical Computer Science 17 Cambridge University Press 1990."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Baeten J. C. M. and Weijland W.P.: Process Algebra . Cambridge Tracts in Theoretical Computer Science 18 Cambridge University Press 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_2_4_2","unstructured":"De Nicola R. and Segala R.: A process algebraic view of I\/O automata. Technical Report SI-92\/05 Dipartimento di Scienze dell'Informazione Universit\u00e0 degli studi di Roma La Sapienza September 1992."},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Gawlick R. Segala R. S\u00f8gaard-Andersen J. F. and Lynch N.: Liveness in timed and untimed systems. Technical Report MIT\/LCS\/TR-587 MIT Laboratory for Computer Science November 1993.","DOI":"10.1007\/3-540-58201-0_66"},{"key":"e_1_2_1_2_6_2","unstructured":"Groote J. F. and van de Pol J. C.: A bounded retransmission protocol for large data packets. A case study in computer checked verification. Technical Report 100 Logic Group Preprint Series Utrecht University 1993."},{"key":"e_1_2_1_2_7_2","volume-title":"Algebraic Theory of Processes","author":"Hennessy M.","year":"1988"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Helmink L. Sellink M. P. A. and Vaandrager F. W.: Proof-checking a data link protocol. Technical Report CS-R9420 Programming Research Group University of Amsterdam 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178564"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Lin H.: PAM: A Process Algebra Manipulator. In Larsen and Skou [LaS91] pages 136\u2013146.","DOI":"10.1007\/3-540-55179-4_14"},{"key":"e_1_2_1_2_12_2","unstructured":"Lynch N. and Patt-Shamir B.: Distributed Algorithms. Fall 1992 Lecture Notes for 6.852. MIT\/LCS\/RSS 16 MIT Laboratory for Computer Science 1992."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Larsen K. G. and Skou A.: editors. Proceedings of the third international workshop on Computer Aided Verification volume 575 of Lecture Notes in Computer Science . Springer-Verlag 1991.","DOI":"10.1007\/3-540-55179-4"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Lynch N. A. and Tuttle M. R.: Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6 th Annual ACM Symposium on Principles of Distributed Computing pages 137\u2013151 Vancouver Canada August 1987. A full version is available as MIT Technical Report MIT\/LCS\/TR-387.","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Lynch N. A. and Vaandrager F. W.: Forward and backward simulations for timing-based systems. In J.W. de Bakker C. Huizing W.P. de Roever and G. Rozenberg editors Proceedings of the REX Workshop \u201cReal-Time: Theory in Practice\u201d volume 600 of Lecture Notes in Computer Science pages 397\u2013446. Springer-Verlag 1991.","DOI":"10.1007\/BFb0032002"},{"key":"e_1_2_1_2_17_2","unstructured":"Muller D. E. and Bartky W. S.: A theory of asynchronous circuits. Annals of the Computation Laboratory of Harvard University. Volume XXIX: Proceedings of an International Symposium on the Theory of Switching Part I pages 204\u2013243 1959."},{"key":"e_1_2_1_2_18_2","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Mauw S. and Veltink G. J.: A proof assistant for PSF. In Larsen and Skou [LaS91] pages 158\u2013168.","DOI":"10.1007\/3-540-55179-4_16"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Nipkow T.: Formal verification of data type refinement \u2014 theory and practice. In J.W. de Bakker W.P. de Roever and G. Rozenberg editors Proceedings of the REX Workshop \u201cStepwise Refinement of Distributed Systems\u201d volume 430 of Lecture Notes in Computer Science pages 561\u2013591. Springer-Verlag 1989.","DOI":"10.1007\/3-540-52559-9_79"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211473"},{"key":"e_1_2_1_2_22_2","unstructured":"Segala R.: A process algebraic view of I\/O automata. Technical Memo MIT\/LCS\/TR-557 MIT Laboratory for Computer Science Cambridge MA 02139 October 1992."},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Segala R.: Quiescence fairness testing and the notion of implementation. In E. Best editor Proceedings CONCUR 93 Hildesheim Germany volume 715 of Lecture Notes in Computer Science . Springer-Verlag 1993.","DOI":"10.1007\/3-540-57208-2_23"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"S\u00f8gaard-Andersen J. F. Garland S. J. Guttag J.V. Lynch N. A. and Pogosyants A.: Computer-assisted simulation proofs. In C. Courcoubetis editor Proceedings of the fifth international conference on Computer Aided Verification volume 697 of Lecture Notes in Computer Science . Springer-Verlag 1993.","DOI":"10.1007\/3-540-56922-7_25"},{"key":"e_1_2_1_2_25_2","unstructured":"S\u00f8gaard-Andersen J. F. Lampson B. and Lynch N. A.: Correctness of at-most-once message delivery protocols. In FORTE '93 \u2014 Sixth International Conference on Formal Description Techniques 1993."},{"key":"e_1_2_1_2_26_2","unstructured":"S\u00f8gaard-Andersen J. F. Lynch N. A. and Lampson B. W.: Correctness of communication protocols. a case study. Technical Report MIT\/LCS\/TR-589 MIT Laboratory for Computer Science November 1993."},{"key":"e_1_2_1_2_27_2","unstructured":"Stark E. W.: Foundations of a theory of specification for Distributed Systems . PhD thesis Department of Electrical Engineering and Computer Science Massachusetts Institute of Technology August 1984. Available as Technical Report MIT\/LCS\/TR-342."},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Stark E. W.: On the relations computable by a class of concurrent automata. In Proceedings of the 1990 SIGACT-SIGPLAN Symposium on Principles of Programming Languages 1990.","DOI":"10.1145\/96709.96743"},{"key":"e_1_2_1_2_29_2","unstructured":"Vaandrager F. W.: On the relationship between process algebra and Input\/Output automata. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science 1991."},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Welch J. L. Lamport L. and Lynch N.: A lattice-structured proof technique applied to a minimum spanning tree algorithm. Technical Report MIT\/LCS\/TM-361 MIT Laboratory for Computer Science June 1988.","DOI":"10.21236\/ADA198312"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211073.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211073\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211073","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:23:42Z","timestamp":1641482622000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211073"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,5]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995,5]]}},"alternative-id":["10.1007\/BF01211073"],"URL":"https:\/\/doi.org\/10.1007\/bf01211073","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,5]]}}}