ACネットの有界活性問題のNP困難性  [in Japanese] NP-Hardness of Liveness Problem of Bounded Asymmetric Choice Nets  [in Japanese]

ペトリネットはコンカレントシステムのモデルの一つである。活性問題はペトリネットの最も重要な解析問題の一つである。一般のペトリネットの活性問題の計算量は、決定性指数領域困難であることが知られている。ペトリネットのサブクラスの活性問題の計算量については、有界な自由選択(EFC)ネットの活性問題が決定性多項式時間で解けること、非有界EFCネットの活性問題がNP完全であることが知られている。EFCを包含するクラスである非対称選択(AC)ネットについては非有界ACネットの活性問題はNP困難であるが、有界なACネットについては著者らの知る限り、未解決である。本報告は、論理式の充足可能性問題が有界なACネットの活性問題に多項式時間で帰着可能であることから、この問題はNP困難であることが示される。

Petri net is a mathematical model for concurrent systems. Liveness is one of important properties of Petri net. Liveness problem of general Petri net is of exponential space complexity and subclasses are suggested with less computational complexity. It is well known that liveness problem of bounded free choice(EFC)net is solved in deterministic polynomial time. It is also known that liveness problem of general(unbounded)EFC net is NP-complete. This paper treats leveness problem of asymmetric choice(AC)nets. This class properly includes the class of free choice nets, so that liveness problem of general AC net is NP-hard. However, as far as the authors know, computational complexity of liveness problem of bounded AC net has been open problem. It is shown that satisfiability problem of boolean expressions is polynomial time reducible to liveness problem of bounded AC nets. This implies that the problem is NP-hard.