algorithm - 色付きペトリネットの境界基準

Question

色付きのペトリネットの境界基準 (状態空間が有限であることを意味する) をチェックするアルゴリズムはありますか (または、このプロパティは決定できません)?

Answer 1

はい、状態空間が無限の場合、状態グラフの構築アルゴリズムは中止されます。基本的に、現在のマーキングに到達できる厳密に小さいマーキング (少なくとも 1 つのコンポーネントで非常に小さく、すべてのコンポーネントでそれより小さいか等しい) を持つ別の状態があるかどうか、到達するすべての状態をチェックします。もしそうなら、ネットは - ペトリネットの単調な性質のために - 無限の状態空間を持っています。