Paper Info
Title
Interpreting Message Flow Graphs
Abstract
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üchi 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üchi automaton by means of a set of MFGs.
Year
DOI
Venue
1995
10.1007/BF01211629
Formal Asp. Comput.
Keywords
Field
DocType
Message Flow Graph,Semantics,Büchi automaton,Temporal logic,Liveness
Transition system,Logic model,Sequence diagram,Concurrency,Computer science,Automaton,Theoretical computer science,Temporal logic,Büchi automaton,Liveness
Journal
Volume
Issue
Citations 
7
5
26
PageRank 
References 
Authors
5.64
22
2
Name
Order
Citations
PageRank
Peter B. Ladkin162690.51
Stefan Leue21199108.55