@InProceedings{Isobe11,
  title =        "{CONPASU}-tool: {A} {C}oncurrent {P}rocess {A}nalysis {S}upport {T}ool based on {S}ymbolic {C}omputation",
  author=        "Isobe,  Yoshinao",
  editor=        "Welch, Peter H. and Sampson,  Adam T. and Pedersen,  Jan Bækgaard and Kerridge,  Jon and Broenink,  Jan F. and Barnes,  Frederick R. M.",
  pages =        "341--362",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn=          "978-1-60750-773-4",
  year=          "2011",
  month=         "jun",
  abstract=      "This paper presents an analysis-method of concurrent
     processes with
value-passing which may cause infinite-state
     systems. The method
consists of two steps: sequentialisation
     and state-reduction.  In the
sequentialisation, the symbolic
     transition graph of a given concurrent
process is derived by
     symbolic operational semantics.  In the
state-reduction, the
     number of states in the symbolic transition graph
is reduced
     by removing needless internal transitions.  Furthermore,
     this
paper introduces an analysis-tool called CONPASU, which
     implements the
analysis-method, and demonstrates how CONPASU
     can be used for
automatically analyzing concurrent
     processes. For example, it can
extract abstract behaviors,
     which are useful for understanding complex
behaviors, by
     focusing on some interesting events."
}