Verification of asynchronous systems based on Petri Net unfoldings

スポンサーリンク

概要

• 論文の詳細を見る

• This paper deals with a verification of a formal specification of asynchronous system on its implementability by a speed-independent circuit. A specification model is Signal Transition Graphs which are an interpretation of Petri nets with falling and rising transitions of signals. The implementability conditions are formulated in such a way that they can be checked by analysis of ordering relations between signal transitions rather than by traversal of states. This allows to avoid the state explosion problem for highly parallel specifications. The method is based on PN unfolding into an equivalent acyclic description. The experimental results show that for higly parallel STGs checking the implementability by unfolding is by 1-2 orders of magnitude less time consuming than through a symbolic BDD traversal.

• 社団法人電子情報通信学会の論文
• 1996-05-23

著者

• KONDRATYEV Alex

  The University of Aizu

関連論文

• Petrify: A Tool for Manipulating Concurrent Specifications and Synthesis of Asynchronous Controllers (Special Issue on Asynchronous Circuit and System Design)
• Verification of asynchronous systems based on Petri Net unfoldings

スポンサーリンク