Back to Search
Start Over
The Complexity of Coverability in ν-Petri Nets
- Source :
- LICS, LICS 2016-31th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016-31th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2016, New York, United States. pp.467--476, ⟨10.1145/2933575.2933593⟩
- Publication Year :
- 2016
- Publisher :
- ACM, 2016.
-
Abstract
- We show that the coverability problem in ν-Petri nets is complete for ‘double Ackermann’ time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes ν-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals.Categories and Subject Descriptors F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems
- Subjects :
- Discrete mathematics
Computer science
Semantics (computer science)
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
0102 computer and information sciences
02 engineering and technology
Petri net
01 natural sciences
Ackermann function
Upper and lower bounds
Rotation formalisms in three dimensions
Well-quasi-order
Formal verification
ACM: F.: Theory of Computation/F.2: ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY/F.2.2: Nonnumerical Algorithms and Problems
Well-structured transition system
010201 computation theory & mathematics
Completeness (order theory)
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
QA
Order ideal
Fast-growing complexity
Analysis of algorithms
Subjects
Details
- ISBN :
- 978-1-4503-4391-6
- ISBNs :
- 9781450343916
- Database :
- OpenAIRE
- Journal :
- Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
- Accession number :
- edsair.doi.dedup.....9b8c194331bddf80c52dbc6e90318d11
- Full Text :
- https://doi.org/10.1145/2933575.2933593