Unfolding Models of Asynchronous Systems:
  Applications to Analysis and Synthesis

                            Victor Khomenko

                          Newcastle University
                          School of Computing
                      victor.khomenko@ncl.ac.uk



 Abstract. Analysis and synthesis of concurrent systems suffers from
 combinatorial state space explosion. That is, even a relatively small sys-
 tem specification can (and often does) yield a very large state space.
 One of the prominent techniques for alleviating this problem is based on
 complete prefixes of Petri net unfoldings. It relies on the partial order
 view of concurrent computation, and represents system states implicitly,
 using an acyclic Petri net. This talk describes applications of the un-
 folding technique to analysis of concurrent systems in general, and to
 verification and synthesis of asynchronous circuits in particular.