A few days ago a diploma dropped in the door, meaning that after 3 years at Aalborg University I’ve got a “Bachelor of Science (BSc) in Computer Science”, as it says on the paper… I’m of course continuing as a master student next – no reason to get out “there” in the real world, where you have to work, assuming you don’t what to starve 🙂

Anyways, it occurred to me that I haven’t blogged about my Bachelor project. So I better get it done now, as I’m off for vacation in California later tonight… This semester we worked in groups of 3, and was supposed to write a 12-20 pages article, as opposed to a 100-200 pages report. Which turned out to be quite challenging, but also somewhat nice, because we got to polish every sentence.

As the title of the post indicates we did a project about Petri nets, a very simple but powerful modeling language. To achieve a “feeling” of novelty we introduced global discrete variables, that you can condition on and modify in transitions, and called our new model for Petri nets With Discrete Variables (PNDV). Whilst, to my knowledge, this have not been done before, we didn’t focus on showing that PNDVs where particularly useful for any specific purpose. So that part of the project feels a little shoehorned, at least to me, and maybe only me, because we all got an A for the project.

Nevertheless, assuming that the PNDV model (we invented) is interesting, then the graphical Petri net editor and verification tool we wrote during this project might also be interesting. In a desperate search for a name we came up with PeTe, yes is spelled pretty weird, but also quite cute 🙂

Given a PNDV or Petri net PeTe can determine if a state satisfying a given formula is possible. This problem is very hard (EXPSPACE-hard), but we had a lot of fun writing different search strategies for exploring the state space of a PNDV. Most notably we found that even quite simple heuristics can provide a huge performance improvement by guiding a search in state space. We also had great success with over-approximation, by using state equation and trap testing to disprove the satisfyability of a formula.

The heuristics and methods implemented in PeTe is presented in the article we wrote, available for download below. This article also present some, in my opinion, rather shoehorned results, like translation from Discrete Timed Arc Petri Net to PNDV. I also can’t help but feel that the direction and goal in the article could have been more clear. But done is done, and I’m off to vacation when I’ve added some links 🙂

• Petri Nets With Discrete Variables (pdf, 0.7MiB)
• PeTe project page at github