Blondin, M; Haase, C; (2017) Logics for continuous reachability in Petri nets and vector addition systems with states. In: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE: Reykjavik, Iceland.

Preview

Text Haase_bh17_AAM.pdf - Accepted Version Download (559kB) | Preview

Abstract

This paper studies sets of rational numbers definable by continuous Petri nets and extensions thereof. First, we identify a polynomial-time decidable fragment of existential FO(ℚ,+,<;) and show that the sets of rationals definable in this fragment coincide with reachability sets of continuous Petri nets. Next, we introduce and study continuous vector addition systems with states (CVASS), which are vector addition systems with states in which counters may hold non-negative rational values, and in which the effect of a transition can be scaled by a positive rational number smaller or equal to one. This class strictly generalizes continuous Petri nets by additionally allowing for discrete control-state information. We prove that reachability sets of CVASS are equivalent to the sets of rational numbers definable in existential FO(ℚ,+,<;) from which we can conclude that reachability in CVASS is NP-complete. Finally, our results explain and yield as corollaries a number of polynomial-time algorithms for decision problems that have recently been studied in the literature.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as XMLJSONCSV

Archive Staff Only

View Item