一般库所/变迁系统中无冲突情况下的抽象进程
计算机科学中的逻辑
2022-07-12 v1
摘要
Goltz 与 Reisig 将 Petri 关于单安全 Petri 网进程的概念推广到库所可携带多个令牌的一般网。BD-进程是通过 Best 与 Devillers 的交换变换相连的 Goltz-Reisig 进程的等价类；它们可被视为网运行的一种替代表示。此处我们给出可数网的 BD-进程与 FS-进程之间保序的双射，后者以类似方式定义为发射序列的等价类。利用此结果，我们证明无二元冲突的可数网具有（唯一的）最大 BD-进程。
引用
@article{arxiv.2207.04362,
title = {Abstract Processes in the Absence of Conflicts in General Place/Transition Systems},
author = {Rob van Glabbeek and Ursula Goltz and Jens-Wolfhard Schicke-Uffmann},
journal= {arXiv preprint arXiv:2207.04362},
year = {2022}
}
备注
The above result appeared already in our technical report arXiv:2103.00729, although formulated and proven differently, since there we didn't have the preorder $\sqsubseteq_1^\infty$, introduced in arXiv:2103.01490. Our revised proofs are conceptually simpler, as they avoid the auxiliary concepts of BD-runs and FS-runs