Computation of summaries using net unfoldings

We study the following summarization problem: given a parallel composition A = A₁ ∥. . ∥ A_n of labelled transition systems communicating with the environment through a distinguished component A_i, efficiently compute a summary S_i such that E ∥ A and E ∥ S_i are trace-equivalent for every environment E. While S_i can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of Mole, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications.