S. Purushothaman Iyer
Dept of Computer Systems - Uppsala University
SE-751 05 Uppsala, SWEDEN
Fax: +46+18+550 225
purush@docs.uu.se
http://www.csc.ncsu.edu/faculty/purush
Abstract
Symbolic techniques based on BDDs have had great success in the domain of synchronous systems. However, in the context of asynchronous systems BDDs fare very poorly. For the past ten years there has been a slew of work, by McMillan and by Esparza, on unfoldings as a technique to deal with the state explosion problem in asynchronous communication. They have show how unfoldings can be used in the context of finite state systems (typically n-safe petri nets) to avoid reasoning about all interleavings. In this talk I will discuss our efforts to generalize this technique to unbounded state space systems. In particular, I will detail the application of our technique to unbounded petri nets and to processes communicating over unbounded buffers.
Last Updated: May 10, 2000 by Elisabetta Ferrando