Taking Complete Finite Prefixes To High Level, Symbolically.
Petri Nets(2023)
摘要
Unfoldings are a well known partial-order semantics of P/T Petri nets that
can be applied to various model checking or verification problems. For
high-level Petri nets, the so-called symbolic unfolding generalizes this
notion. A complete finite prefix of a P/T Petri net's unfolding contains all
information to verify, e.g., reachability of markings. We unite these two
concepts and define complete finite prefixes of the symbolic unfolding of
high-level Petri nets. For a class of safe high-level Petri nets, we generalize
the well-known algorithm by Esparza et al. for constructing small such
prefixes. We evaluate this extended algorithm through a prototype
implementation on four novel benchmark families. Additionally, we identify a
more general class of nets with infinitely many reachable markings, for which
an approach with an adapted cut-off criterion extends the complete prefix
methodology, in the sense that the original algorithm cannot be applied to the
P/T net represented by a high-level net.
更多查看译文
关键词
complete finite prefixes,high level
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要