文章基本信息

标题：Ideal Decompositions for Vector Addition Systems (Invited Talk)
本地全文：下载
作者：J{\'e}r{\^o}me Leroux ; Sylvain Schmitz
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：47
页码：1:1-1:13
DOI：10.4230/LIPIcs.STACS.2016.1
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Vector addition systems, or equivalently Petri nets, are one of the most popular formal models for the representation and the analysis of parallel processes. Many problems for vector addition systems are known to be decidable thanks to the theory of well-structured transition systems. Indeed, vector addition systems with configurations equipped with the classical point-wise ordering are well-structured transition systems. Based on this observation, problems like coverability or termination can be proven decidable. However, the theory of well-structured transition systems does not explain the decidability of the reachability problem. In this presentation, we show that runs of vector addition systems can also be equipped with a well quasi-order. This observation provides a unified understanding of the data structures involved in solving many problems for vector addition systems, including the central reachability problem.
关键词：Petri net; ideal; well-quasi-order; reachability; verification