Abstract

The goal of this project is to do reachability analysis of petri nets using model transformations in AToMPM. An algorithm based on model driven transformations is introduced to create a reachability graph of a given petri net.
This algorithm is adapted from an existing reachability graph generating algorithm. Subsequently the reachability graph can be queried to find if a configuration of the petri net is reachable from the original state.

  Reading

Reading report
presentation 11 dec (pptx)
presentation 11 dec (pdf)

  Implementation

To use the implementation, extract the compressed folder PetriNetReachability in /Formalisms in AtomPM. The implementation depends on the PN_inhibitor formalism.

implementation
final presentation (pptx)
final presentation (pdf)
final report (pdf)