Jasper Verelst - Reachability analysis of Petrinets models in AToMPM using model transformations 


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 report
presentation 11 dec (pptx)
presentation 11 dec (pdf)


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

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