{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:50Z","timestamp":1761611150644},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1995,9,1]],"date-time":"1995-09-01T00:00:00Z","timestamp":809913600000},"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,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We give a semantics for Message Flow Graphs (MFGs), which play the role for interprocess communication that Program Dependence Graphs play for control flow in parallel processes. MFGs have been used to analyse parallel code, and are closely related to Message Sequence Charts and Time Sequence Diagrams in telecommunications systems. Our requirements are firstly, to determine unambiguously exactly what execution traces are specified by an MFG, and secondly, to use a finite-state interpretation. Our methods function for both asynchronous and synchronous communications. From a set of MFGs, we define a transition system of global states, and from that a B\u00fcchi automaton by considering safety and liveness properties of the system. In order easily to describe liveness properties, we interpret the traces of the transition system as a model of Manna-Pnueli temporal logic. Finally, we describe the expressive power of MFGs by mimicking an arbitrary B\u00fcchi automaton by means of a set of MFGs.<\/jats:p>","DOI":"10.1007\/bf01211629","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T13:02:46Z","timestamp":1109336566000},"page":"473-509","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":57,"title":["Interpreting Message Flow Graphs"],"prefix":"10.1145","volume":"7","author":[{"given":"Peter B.","family":"Ladkin","sequence":"first","affiliation":[{"name":"Dept. of Computing Science, University of Stirling, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Universit\u00e4t Bern, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"e_1_2_1_2_2_2","unstructured":"Aggrawal S. and Sabnani K.: editors. Protocol Specification Testing and Verification VIII. Proceedings of the IFIP WG 6.1 Eighth International Symposium on Protocol Specification Testing and Verification . North Holland 1989."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/59287.62028"},{"key":"e_1_2_1_2_4_2","volume-title":"Research Report 581","author":"Benveniste A.","year":"1991"},{"key":"e_1_2_1_2_5_2","unstructured":"Berry G. and Gonthier G.: The Esterel synchronous programming language: Design semantics implementation. Rapport de Recherche 842 Institut National de Recherche en Informatique et en Automatique (INRIA) 1988."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.53519"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90001-E"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Baeten J. C. M. and Mauw S.: Delayed choice: an operator for joining message sequence charts. In [ HoL95 ]. 1995. To appear.","DOI":"10.1007\/978-0-387-34878-0_27"},{"key":"e_1_2_1_2_10_2","volume-title":"Technical Report IBM RZ 2162","author":"Cockburn A. A. R.","year":"1991"},{"key":"e_1_2_1_2_11_2","unstructured":"Cockburn A. A. R. Citrin W. Hauser R. F. and K\u00e4nel J.: An environment for interactive design of communication architectures. In [ LPU91 ] 1990."},{"key":"e_1_2_1_2_12_2","volume-title":"Recommendation Z.120: Message Sequence Chart (MSC)","author":"CCITT","year":"1992"},{"key":"e_1_2_1_2_13_2","unstructured":"Cohen D. and Dorn N.: An experiment in analysing switch recovery procedures. In [ DiG93 ] pages 23\u201334 1993."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Clarke E. M. and Kurshan R. P.: editors. Computer Aided Verification: Proceedings of CAV'90 volume 531 of Lecture Notes in Computer Science . Springer Verlag 1991.","DOI":"10.1007\/BFb0023712"},{"key":"e_1_2_1_2_15_2","unstructured":"Courtiat J.-P.: ESTELLE*: a powerful dialect of ESTELLE for OSI protocol description. In [ AlS89a ] 1988."},{"key":"e_1_2_1_2_16_2","unstructured":"Courtiat J.-P: Estelle and Petri nets: introducing a rendezvous mechanism in Estelle: Estelle. In M. Diaz J.-P. Ansart J.-P. Courtiat P. Az\u00e9ma and V. Chari editors The Formal Description Technique Estelle pages 175\u2013203. North-Holland 1989."},{"key":"e_1_2_1_2_17_2","unstructured":"Diaz M. and Groz R.: editors. Formal Description Techniques V. IFIP Transactions C-10 Proceedings of the Fifth International Conference on Formal Description Techniques. North-Holland 1993."},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/139619.139621"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(92)90109-4"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Godefroid P. and Wolper P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In [ ClK91 ] pages 332\u2013341 1992.","DOI":"10.1007\/3-540-55179-4_32"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Hogrefe D. and Leue S.: editors. Formal Description Techniques VII. Proceedings of the Seventh International Conference on Formal Description Techniques. Chapman & Hall 1995.","DOI":"10.1007\/978-0-387-34878-0"},{"key":"e_1_2_1_2_22_2","unstructured":"Hoare C. A. R.: Communicating Sequential Processes. Prentice-Hall International 1985."},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Hogrefe D.: SDL and OSI: On the use of CCITT-SDL in the context of OSI. Habilitation Thesis University of Hamburg 1989.","DOI":"10.1007\/978-3-642-74238-5_5"},{"key":"e_1_2_1_2_24_2","unstructured":"Holzmann G. J.: Design and Validation of Computer Protocols. Prentice-Hall International 1991."},{"key":"e_1_2_1_2_25_2","unstructured":"Inmos Ltd.: The Occam Programming Manual. Prentice-Hall International 1984."},{"key":"e_1_2_1_2_26_2","unstructured":"International Standards Organisation. Information Processing Systems \u2014 Open Systems Interconnection \u2014 Basic Reference Model. International Standard 7498 ISO 1984."},{"key":"e_1_2_1_2_27_2","unstructured":"International Standards Organisation. Estelle: A formal description technique based on an extended state transition model. Draft International Standard 9074 ISO\/IFIP 1987."},{"key":"e_1_2_1_2_28_2","unstructured":"International Standards Organisation. Information Processing Systems \u2014 Open Systems Interconnection \u2014 LOTOS: A formal description technique based on the temporal ordering of observational behavior. International Standard 8807 ISO\/IEC 1988."},{"key":"e_1_2_1_2_29_2","unstructured":"International Standards Organisation. Information Processing Systems \u2014 Open Systems Interconnection \u2014 Conformance Testing Methodology and Framework Part 1: General Concepts. International Standard 9464 ISO ISO\/TC97\/SC21 1991."},{"key":"e_1_2_1_2_30_2","unstructured":"International Standards Organisation. Revised Text of CD 10731 Information Processing Systems \u2014 Open Systems Interconnection \u2014 Service Conventions. ISO\/IEC JTC 1\/SC21 N 6341 ISO\/IEC Jan 1991."},{"key":"e_1_2_1_2_31_2","unstructured":"Kurshan R. P.: Automata-theoretic verification of communicating processes. Unpublished lecture notes. AT & T Bell Laboratories Aug 1992."},{"key":"e_1_2_1_2_32_2","unstructured":"Ladkin P. B.: Using tense logic to describe digital computing systems. Technical Report TR 110 Department of Computing Science University of Stirling 1993."},{"key":"e_1_2_1_2_33_2","first-page":"08","article-title":"Applying finite-state methods to infinite-state systems","volume":"92","author":"Lamport L.","year":"1992","journal-title":"TLA Mailing List Note"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_2_35_2","unstructured":"Ladkin P. B. and Leue S.: Interpreting Message Sequence Charts. Technical Report TR 101 Department of Computing Science University of Stirling 1993."},{"key":"e_1_2_1_2_36_2","unstructured":"Ladkin P. B. and Leue S.: What do Message Sequence Charts mean? In [ TAU94 ] pages 301\u2013316. 1994."},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Ladkin P. B. and Leue S.: Four issues concerning the semantics of Message Flow Graphs. In [ HoL95 ]. 1995.","DOI":"10.1007\/978-0-387-34878-0_28"},{"key":"e_1_2_1_2_38_2","unstructured":"Logrippo L. Probert R. L. and Ural H.: editors. Protocol Specification Testing and Verification X. Proceedings of the IFIP WG 6.1 Tenth International Symposium on Protocol Specification Testing and Verification. North Holland 1991."},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Ladkin P. B. and Simons B. B.: Compile-time analysis of communicating processes. Technical Report RJ 8488 IBM Almaden Research Center Nov 1991.","DOI":"10.1145\/143369.143417"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Ladkin P. B. and Simons B. B.: Compile-time analysis of communicating processes. In Proceedings of the Sixth ACM International Conference on Supercomputing pages 248\u2013259. ACM Press 1992.","DOI":"10.1145\/143369.143417"},{"key":"e_1_2_1_2_41_2","unstructured":"Ladkin P. B. and Simons B. B.: Static analysis of concurrent communicating loops. Technical Report RJ 8625 IBM Almaden Research Center Feb 1992."},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Larsen K. G. and Skou A.: editors. Computer Aided Verification: Proceedings of CAV'91 volume 575 of Lecture Notes in Computer Science. Springer Verlag 1992.","DOI":"10.1007\/3-540-55179-4"},{"key":"e_1_2_1_2_43_2","unstructured":"Ladkin P. B. and Simons B. B.: Static Analysis of Interprocess Communication. Lecture Notes in Computer Science. Springer-Verlag 1995. To appear."},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Ladkin P. B. and Simons B. B.: Static deadlock analysis for CSP-type communications. In D. Fussell editor Responsive Computer Systems: Toward Integration of Fault-Tolerance and Real Time. Kluwer 1995.","DOI":"10.1007\/978-1-4615-2271-3_5"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz A.: Trace theory. In W. Brauer W. Reisig and G. Rozenberg editors Petri-Nets Applications and Relationship to other Models of Concurrency LNCS Vol. 255 volume LNCS 255 of Lecture Notes in Computer Science pages 279\u2013324. Springer Verlag 1987.","DOI":"10.1007\/3-540-17906-2_30"},{"key":"e_1_2_1_2_46_2","unstructured":"Milner R.: Communication and Concurrency. Prentice Hall International 1989."},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: A hierarchy of temporal properties. In Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing pages 377\u2013408. ACM Press Aug 1990.","DOI":"10.1145\/93385.93442"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/37.4.269"},{"key":"e_1_2_1_2_50_2","unstructured":"Rumbaugh J. Blaha M. Premerlani W. Eddy F. and Lorensen W.: Object-Oriented Modeling and Design. Prentice Hall International 1991."},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.210304"},{"key":"e_1_2_1_2_52_2","unstructured":"Selic B. Gullekson G. and Ward P. T. Real-Time Object-Oriented Modelling . John Wiley & Sons Inc. 1994."},{"key":"e_1_2_1_2_53_2","volume-title":"EWSD Softwareentwicklungshandbuch (Software Development Handbook), Kapitel B, Register 6, SDL Diagramme","author":"Siemens A. G.","year":"1988"},{"key":"e_1_2_1_2_54_2","unstructured":"Spivey J. M.: The Z Notation. Prentice-Hall International 1989."},{"key":"e_1_2_1_2_55_2","unstructured":"Tanenbaum A. S.: Computer Networks. Prentice-Hall International 2nd edition 1989."},{"key":"e_1_2_1_2_56_2","unstructured":"Tenney R. L. Amer P. D. and Uyar M. \u00dc.: editors. Formal Description Techniques VI. IFIP Transactions C Proceedings of FORTE '93 the Sixth International Conference on Formal Description Techniques. North-Holland 1994."},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Thomas W.: Automata on infinite objects. In Handbook of Theoretical Computer Science chapter 4 pages 132\u2013191. Elsevier Science Publishers B. V. (North-Holland) 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/35.5.478"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Weinberg H. B. and Zuck L. D.: Timed Ethernet: Real-time formal specification of Ethernet. In W. R. Cleaveland editor CONCUR '92 volume 630 of Lecture Notes in Computer Science pages 370\u2013385. Springer Verlag 1992.","DOI":"10.1007\/BFb0084804"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211629.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211629\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211629","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:28:49Z","timestamp":1641482929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211629"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,9]]},"references-count":60,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1995,9]]}},"alternative-id":["10.1007\/BF01211629"],"URL":"https:\/\/doi.org\/10.1007\/bf01211629","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,9]]}}}