时间验证 [英] time perti net verification

问题描述

我有一个用于电梯的PN，并且我正在使用定时PN，这样我就可以确定电梯是否可以在一定时间内到达特定点！

那是对的吗 ?

我可以确定时间条件，但是时间PN是否没有这样做的算法?

非常感谢您推荐有关此问题的任何参考文献:)

I have a PN for an elevator and I''m using timed PN so that I can find out if the elevator can get to a certain point within certain period of time!

is that correct ?

I can make sure of the time condition , but doesn''t time PN have algorithms to do so ?

any reference you recommend about this issue is highly appreciated :)

推荐答案

很抱歉，我只知道非定时 1-的算法精妙的 Petri Net.该算法基于线性代数，它所能做的就是从任何其他位置确定任何位置的可达性.例如，如果您将一个或多个位置标识为死锁，但是可以证明从起始位置无法到达任何死锁位置，则可以证明整个系统没有死锁.为了证明这一点，您可以将Petri网形式化为线性方程，您可以使用线性代数和/或计算机代数系统(CAS)中的常规算法自动将其求解，而创建 ad 并不是很困难，仅适用于这种情况.

参见:
http://en.wikipedia.org/wiki/Petri_net [ http://msdn.microsoft. com/en-us/library/ms810303.aspx [ ^ ].

现在，关于定时 Petri Nets 的几句话.即使我不太熟悉它们，但我可以肯定地说，除非您的系统是硬实时系统，否则它们不会预测有保证的执行时间. (请参见 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 [ /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 = AFQjCNEnwxcgaa-mKTBEV7_RblasjM"^ ]，
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 [ ^ ].

尝试找到更多的东西，但这不是一个非常受欢迎的科学技术领域，很难找到想要的东西.

—SA

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

这篇关于时间验证的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！