Symbolic Analysis of Concurrent Systems

The complexity of current digital systems requires an early introduction of formal methods in the analysis and synthesis cycle. Medium complexity system may easily contain more than states. It is clearly impossible to explicitly represent such a number of states in any existing computer. In particular, highly concurrent systems requires the utilization of symbolic techniques in order to overcome the limitations introduced by its exponential number of states. The current work of the group is based on the utilization of high-level models such as Petri nets, and the development of symbolic methodologies supported by Binary Decision Diagrams. The generality of the Petri net formalism allows tackling multiple research areas, like synthesis and verification of asynchronous systems, test-pattern generation, general Petri net analysis and synthesis, code generation for embedded systems, etc... Hence, this research area must concentrate on the development of efficient models and algorithms for the analysis of concurrent systems based on underlying Petri nets or Transition System formalisms. Memory and CPU preserving state encoding and state exploration techniques are required to --in combination with Binary Decision Diagrams and similar data structures-- alleviate the state explosion problem.

• Enric Pastor, Oriol Roig, Jordi Cortadella, and Rosa M. Badia. Petri net Analysis Using Boolean Manipulation . In 15th International Conference on Application and Theory of Petri Nets , volume 815 of Lecture Notes in Computer Science , pp. 416-435. Springer-Verlag, June 1994.

• Oriol Roig, Jordi Cortadella, and Enric Pastor. Verification of asynchronous circuits by BDD-based model checking of Petri nets . In 16th International Conference on Application and Theory of Petri Nets , volume 935 of Lecture Notes in Computer Science , pp. 374-391, Torino, June 1995. Springer-Verlag.

• Jordi Cortadella, Michael Kishinevsky, Luciano Lavagno, and Alexandre Yakovlev. Synthesizing Petri Nets from State-Based Models. In Proc. of the IEEE/ACM International Conference on Computer Aided Design , pp. 164-171. IEEE Computer Society Press, November 1995.

• Jordi Cortadella, Michael Kishinevsky, Alex Kondratyev, Luciano Lavagno, and Alexandre Yakovlev. Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers. In XI Conference on Design of Integrated Circuits and Systems , Barcelona, November 1996. (To appear).