论文部分内容阅读
时间Petri网存在强语义和弱语义两种模型，弱语义模型更适合建模和分析外部环境触发的冲突选择问题，但其形式语义和可达性分析方面的研究，却很少有人问津。利用带标号的变迁系统定义时间Petri网弱语义模型的形式语义，采用时间戳状态类方法分析它的可达性，并证明了可达性问题的可判性和状态类时间戳的全局时间性质。