论文标题
等待网:州班和分类学
Waiting Nets: State Classes and Taxonomy
论文作者
论文摘要
随着时间的推移,Petri网(TPN),时间和控制紧密连接:过渡的时间测量仅在开火所需的所有资源时才开始。此外,启用持续时间上的上限可以迫使过渡到发射(这称为紧迫性)。对于许多系统,一个人希望将控制和时间解次,即,在填充过渡的一部分后,就开始测量时间,并在所有需要的资源可用时在延迟\下划线{and}后将其发射。本文考虑了分解时间测量和控制的TPN的扩展名为等待网。他们的语义允许时间测量从不完整的预设开始,当达到间隔的上限时,可以忽略紧迫性,但尚无启动所需的所有资源。一旦有丢失的资源,允许射击过渡。众所周知,扩展具有秒表的有界TPN会导致不可证明性。我们的扩展更弱,我们展示了如何计算有限的状态类图,以实现有限的等待网,从而产生可及性和覆盖性的可决定性。然后,我们将等待网的表现力与其他模型W.R.T.的表现力进行比较。定时的语言等效性,并表明它们比TPN更严格表达。
In time Petri nets (TPNs), time and control are tightly connected: time measurement for a transition starts only when all resources needed to fire it are available. Further, upper bounds on duration of enabledness can force transitions to fire (this is called urgency). For many systems, one wants to decouple control and time, i.e. start measuring time as soon as a part of the preset of a transition is filled, and fire it after some delay \underline{and} when all needed resources are available. This paper considers an extension of TPN called waiting nets that dissociates time measurement and control. Their semantics allows time measurement to start with incomplete presets, and can ignore urgency when upper bounds of intervals are reached but all resources needed to fire are not yet available. Firing of a transition is then allowed as soon as missing resources are available. It is known that extending bounded TPNs with stopwatches leads to undecidability. Our extension is weaker, and we show how to compute a finite state class graph for bounded waiting nets, yielding decidability of reachability and coverability. We then compare expressiveness of waiting nets with that of other models w.r.t. timed language equivalence, and show that they are strictly more expressive than TPNs.