Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States
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(Q, +, <) and show that the sets of rationals definable in this fragment coincide with reachability sets of continuou...
| Main Authors: | , |
|---|---|
| 格式: | Conference item |
| 出版: |
Institute of Electrical and Electronics Engineers
2017
|
| _version_ | 1826260119376101376 |
|---|---|
| author | Haase, C Blondin, M |
| author_facet | Haase, C Blondin, M |
| author_sort | Haase, C |
| collection | OXFORD |
| description | 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(Q, +, <) 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(Q, +, <) 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. |
| first_indexed | 2024-03-06T19:00:34Z |
| format | Conference item |
| id | oxford-uuid:1362a013-35b8-4ca4-85fd-7744e9e2fba1 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T19:00:34Z |
| publishDate | 2017 |
| publisher | Institute of Electrical and Electronics Engineers |
| record_format | dspace |
| spelling | oxford-uuid:1362a013-35b8-4ca4-85fd-7744e9e2fba12022-03-26T10:13:36ZLogics for Continuous Reachability in Petri Nets and Vector Addition Systems with StatesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:1362a013-35b8-4ca4-85fd-7744e9e2fba1Symplectic Elements at OxfordInstitute of Electrical and Electronics Engineers2017Haase, CBlondin, MThis 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(Q, +, <) 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(Q, +, <) 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. |
| spellingShingle | Haase, C Blondin, M Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States |
| title | Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States |
| title_full | Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States |
| title_fullStr | Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States |
| title_full_unstemmed | Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States |
| title_short | Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States |
| title_sort | logics for continuous reachability in petri nets and vector addition systems with states |
| work_keys_str_mv | AT haasec logicsforcontinuousreachabilityinpetrinetsandvectoradditionsystemswithstates AT blondinm logicsforcontinuousreachabilityinpetrinetsandvectoradditionsystemswithstates |