package coq-karp-miller
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Certified Karp-Miller algorithm for the covering of Petri nets
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.tar.gz
sha256=02c35ae0701c5e5fd5e0974158d32dda30a07004d41f355ef0b6a5d27b6f269b
Description
Based on the Kruskal-AlmostFull library, we build two correct by construction Karp-Miller algorithms: the first one decides for the coverability problem; and the second one, a refined version, builds the Karp-Miller tree and, either a path in that tree giving a covering, or a proof that no such path exists in the Karp-Miller trees.
Tags
category:Computer Science/Data Types and Data Structures date:2024-03-13 logpath:KarpMillerPublished: 13 Mar 2024
Dependencies (4)
- coq-kruskal-finite
- coq-kruskal-trees
-
coq-kruskal-almostfull
>= "1.0" -
coq
>= "8.14" & < "8.20~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page