Pith Number

pith:3NGDADBH

pith:2026:3NGDADBHSKLQYZDXPS2S2P6HWC

not attested not anchored not stored refs resolved

Kofola 1.0: A Modular Approach to {\omega}-Regular Complementation and Inclusion Checking (Technical Report)

Luk\'a\v{s} Hol\'ik, Nicolas Mazzocchi, Ondrej Alexaj, Ond\v{r}ej Leng\'al, Vojt\v{e}ch Havlena, Yong Li

Kofola decomposes Büchi automata into strongly connected components and applies tailored complementation to each.

arxiv:2605.15390 v1 · 2026-05-14 · cs.LO · cs.FL

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{3NGDADBHSKLQYZDXPS2S2P6HWC}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

Kofola implements a state-of-the-art modular complementation framework that decomposes the input automaton into strongly connected components and applies to each component a complementation algorithm tailored to its structural properties. Building on this modular construction, Kofola also provides modular inclusion checking with new heuristics. Empirical evaluation shows that Kofola is highly competitive with state-of-the-art complementation and inclusion-checking tools: it is the most robust tool in our evaluation and often outperforms competitors by several orders of magnitude on benchmarks from practical applications.

C2weakest assumption

The decomposition into strongly connected components combined with per-component tailored complementation algorithms and the new on-the-fly emptiness checker for the produced generalized Rabin pair condition together preserve correctness while delivering the reported efficiency gains (abstract, paragraphs describing the framework and the emptiness-checking algorithm).

C3one line summary

Kofola 1.0 implements a modular SCC-based complementation framework for Büchi automata with tailored per-component algorithms, a new on-the-fly emptiness checker, and modular inclusion heuristics, showing strong empirical performance.

References

56 extracted · 56 resolved · 0 Pith anchors

[1] Automata-benchmarks.https://github.com/ondrik/automata-benchmarks/ tree/master/omega/(2025) 2.Kofola.https://github.com/VeriFIT/kofola(2025) 2025

[2] In: Touili, T., Cook, B., Jackson, P.B 2010

[3] Springer (2010).https://doi.org/10.1007/978-3-642-14295-6_14,https: //doi.org/10.1007/978-3-642-14295-6_14 2010 · doi:10.1007/978-3-642-14295-6_14

[4] In: Katoen, J., K¨ onig, B 2011 · doi:10.1007/978-3-642-23217-6_13

[5] Alexaj, O., Havlena, V., Hol´ ık, L., Leng´ al, O., Li, Y., Mazzocchi, N.: Artifact: Kofola1.0: A modular approach toω-regular complementation and inclusion checking (october 2025).https://doi.org/10. 2025 · doi:10.5281/zenodo.17478623

Receipt and verification

First computed	2026-05-20T00:00:56.098358Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

db4c300c2792970c64777cb52d3fc7b0883e49b58a42a3e93ff22fd29502ea96

Aliases

arxiv: 2605.15390 · arxiv_version: 2605.15390v1 · doi: 10.48550/arxiv.2605.15390 · pith_short_12: 3NGDADBHSKLQ · pith_short_16: 3NGDADBHSKLQYZDX · pith_short_8: 3NGDADBH

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/3NGDADBHSKLQYZDXPS2S2P6HWC \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: db4c300c2792970c64777cb52d3fc7b0883e49b58a42a3e93ff22fd29502ea96

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "d56b5b01980c7473eea1178dd9d06b82a3c765de2287d061b7add6512127c103",
    "cross_cats_sorted": [
      "cs.FL"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-14T20:19:30Z",
    "title_canon_sha256": "c7c4a37945d4f76daea25c74a9562c76653dfe35c9d652df990015010fee34db"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.15390",
    "kind": "arxiv",
    "version": 1
  }
}