Data

Tools

Indexes

Applications

Experiments

Open Source Science

karp-miller

A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull

https://github.com/dmxlarchey/karp-miller

Science Score: 49.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ✓
    DOI references
    Found 1 DOI reference(s) in README
  • ✓
    Academic publication links
    Links to: acm.org
  • ○
    Committers with academic emails
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (8.2%) to scientific vocabulary
Last synced: 7 months ago · JSON representation

Repository

A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull

Basic Info
  • Host: GitHub
  • Owner: DmxLarchey
  • License: mpl-2.0
  • Language: Coq
  • Default Branch: main
  • Size: 38.1 KB
Statistics
  • Stars: 1
  • Watchers: 2
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Created about 2 years ago · Last pushed over 1 year ago
Metadata Files
Readme License Authors Codemeta

README.md

(**************************************************************) (* Copyright Dominique Larchey-Wendling [*] *) (* *) (* [*] Affiliation LORIA -- CNRS *) (**************************************************************) (* This file is distributed under the terms of the *) (* Mozilla Public License Version 2.0, MPL-2.0 *) (**************************************************************)

What is this project

The project contains a correct by construction algorithm for deciding coverability for Petri nets, based on the construction of the Karp-Miller tree. It crucially exploits Dickson's lemma from the Kruskal-AlmostFull library

coq af_vec_fall2 n X R : af R → af (λ u v : vec X n, ∀ i, R u⦃i⦄ v⦃i⦄).

The project is loosely inspired from an Mathematical Components based version based on the paper Formalization of Karp-Miller tree construction on Petri nets (CPP 2017).

It was started as a basis for further discussions with the team of Jérôme Leroux of LaBRI.

The main statement that we prove here is the following: ```coq (** with imports from Relations, KruskalTrees, KruskalFinite and KruskalAFProp *)

Variables (NbPlaces : nat) (* number of places ) (TrIdx : Type) ( type of indices of transitions ) (TrIdx_fin : finite TrIdx). ( finitely many transitions *)

Notation place := (idx NbPlaces). Notation marking := (vec nat NbPlaces).

(* Infix notations for the component wise sum and comparison of vectors *) Infix "+ₘ" := (vecscal plus) (at level 50, left associativity). Infix "≦⁺" := (vecfall2 le) (at level 70).

(* Description of a Petri net via its pre/post transitions *) Variables (pre post : TrIdx → marking).

(* One Petri net transition *) Inductive pntrans : X → X → Prop := | pntintro t u : pn_trans (u +ₘ pre t) (u +ₘ post t).

(* Reachability and coverability *) Definition pnreachable a b := closrefltrans pntrans a b. Definition pncoverable s a := ∃b, pnreacheable s b ∧ a ≦⁺ b.

(* One of the main results *) Theorem pncoverabledec s a : { pncoverable s a } + { ~ pncoverable s a }. ``` but notice that we also build the whole Karp-Miller tree as a variant. However, its statement requires many more definitions.

How to compile

First you need to install the dependencies via opam: console opam update opam install . --deps-only make all and then you can review the code, starting with the main file karp_miller.v.

Owner

  • Name: Dominique Larchey-Wendling
  • Login: DmxLarchey
  • Kind: user
  • Location: Nancy, France
  • Company: CNRS

CodeMeta (codemeta.json) 

{
  "@context": "https://doi.org/10.5063/schema/codemeta-2.0",
  "type": "SoftwareSourceCode",
  "author": [
    {
      "id": "https://orcid.org/0000-0001-9860-7203",
      "type": "Person",
      "affiliation": {
        "type": "Organization",
        "name": "Departement of Formal Method, TYPES team, LORIA, CNRS"
      },
      "email": "dominique.larchey-Wendling@loria.fr",
      "familyName": "Larchey-Wendling",
      "givenName": "Dominique"
    }
  ],
  "codeRepository": "git+https://github.com/DmxLarchey/Karp-Miller.git",
  "dateCreated": "2024-03-13",
  "dateModified": "2024-11-22",
  "datePublished": "2024-03-13",
  "description": "The project contains a Coq 8.14+ designed correct by construction algorithm for deciding coverability for Petri nets, based on the construction of the Karp-Miller tree. It crucially exploits Dickson's lemma from the Kruskal-AlmostFull library.",
  "downloadUrl": "https://github.com/DmxLarchey/Karp-Miller/archive/refs/tags/1.1.tar.gz",
  "funder": {
    "type": "Organization",
    "name": "CNRS"
  },
  "isPartOf": "https://github.com/DmxLarchey/Coq-Kruskal",
  "keywords": [
    "coq",
    "dependent types",
    "Petri nets",
    "coverability",
    "Karp Miller algorithm",
    "almost full relations"
  ],
  "license": "https://spdx.org/licenses/MPL-2.0",
  "name": "Karp-Miller",
  "operatingSystem": [
    "Linux",
    "MacOS"
  ],
  "programmingLanguage": "Coq",
  "relatedLink": "https://github.com/DmxLarchey/Kruskal-AlmostFull",
  "softwareRequirements": "opam, ocaml",
  "version": "1.1",
  "developmentStatus": "active",
  "issueTracker": "https://github.com/DmxLarchey/Karp-Miller/issues"
}

GitHub Events

Total
  • Release event: 1
  • Watch event: 1
  • Delete event: 1
  • Push event: 2
  • Pull request event: 2
  • Create event: 2
Last Year
  • Release event: 1
  • Watch event: 1
  • Delete event: 1
  • Push event: 2
  • Pull request event: 2
  • Create event: 2

Committers

Last synced: 12 months ago

All Time
  • Total Commits: 11
  • Total Committers: 1
  • Avg Commits per committer: 11.0
  • Development Distribution Score (DDS): 0.0
Past Year
  • Commits: 3
  • Committers: 1
  • Avg Commits per committer: 3.0
  • Development Distribution Score (DDS): 0.0
Top Committers
Name Email Commits
Dominique Larchey-Wendling l****y@g****m 11

Issues and Pull Requests

Last synced: 12 months ago

All Time
  • Total issues: 0
  • Total pull requests: 3
  • Average time to close issues: N/A
  • Average time to close pull requests: 8 minutes
  • Total issue authors: 0
  • Total pull request authors: 1
  • Average comments per issue: 0
  • Average comments per pull request: 0.0
  • Merged pull requests: 3
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 1
  • Average time to close issues: N/A
  • Average time to close pull requests: 10 minutes
  • Issue authors: 0
  • Pull request authors: 1
  • Average comments per issue: 0
  • Average comments per pull request: 0.0
  • Merged pull requests: 1
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
Pull Request Authors
  • DmxLarchey (6)
Top Labels
Issue Labels
Pull Request Labels

Dependencies

.github/workflows/main.yml actions
  • actions/checkout v2 composite
  • coq-community/docker-coq-action v1 composite