I'm sorry to say I know only the algorithm for non-timed
1-concervative Petri Net. This algorithm is based on linear algebra and all it can do is to determine
reachability of any location from any other location. For example, if you identify one or more locations as a
deadlock but can proof that none of the deadlock locations is reachable from a starting location, this serves as a proof that the whole system is deadlock-free. To proof that, you formalize the Petri Net into linear equations which you can solve automatically using the regular algorithm from linear algebra and/or computer-algebra system (CAS), which is not too hard to create
ad-hoc, just for this case.
See:
http://en.wikipedia.org/wiki/Petri_net[
^].
This is the article explaining linear algebra formalism in a informal manner, with examples:
http://msdn.microsoft.com/en-us/library/ms810303.aspx[
^].
Now, few words about timed
Petri Nets. Even though I'm not well familiar with them, I can tell you for sure that they wan't predict guaranteed times of execution unless your system is a
hard real-time one. (See
http://en.wikipedia.org/wiki/Real-time_operating_system[
^],
http://en.wikipedia.org/wiki/Hard_real_time#Hard.2C_firm.2C_and_soft_real-time[
^].) The problem is: the real-life multithreading but not hard real-time (:-)) system will introduce
nondeterministic time delay for any predicted execution times.
See:
http://www.google.com/url?sa=t&rct=j&q=%27timer+petri+net%27&source=web&cd=3&ved=0CDYQFjAC&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.69.5289%26rep%3Drep1%26type%3Dpdf&ei=bA_xTvjNOM3pggf8_sWzAg&usg=AFQjCNEnwxcAa-mKTBEV7-RGUsjMgdEZUw[
^],
http://www.lsv.ens-cachan.fr/Projects/anr-dots/PUBLIS/RS-concur09.pdf[
^],
http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DADSS-tacas07.pdf[
^].
Try to find some more, but this is not a very popular field of science and technology, not very easy to find what you want.
—SA
Submit an article or tip