Formal Computer Science / Languages & logic

Kenton Labs / Languages & logic

Automata

Compare complete transition systems through their reachable product, rather than checking a short sample of strings.

The vocabulary.

These definitions state the objects and properties used by the dataset. The complete instance specification remains the authority for each result.

DFA
A deterministic transition function over a finite state set and alphabet.
Product state
A pair of states reached by reading the same prefix in both automata.
Distinguishing word
A finite input accepted by exactly one of the compared machines.

How the dataset works.

Three deterministic instances define this family. Each includes its input model, a checked result, evidence, and an acceptance procedure. Download the complete dataset JSON ↘ or the area’s readable source ↘.

Acceptance procedure

  1. Start from the pair of initial states.
  2. Explore every symbol transition until no new pair is reachable.
  3. Compare acceptance in every reachable pair.
  4. For inequivalence, replay a distinguishing input from both initial states.

Cost and scope

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

A common failure

Bounded string testing is weaker than complete DFA product exploration.

Explore the mechanics.

Change a local input or follow the steps. The stored result and its scope remain attached to the downloadable record.

Worked records.

Three instances expose concrete claims and the artifacts that establish or refute them. Expand a record for the problem, checker reasoning, formal payload, and verification metadata.

KL-FCS-002
AutomataTwo automata, one parity languageComplete reachable product · 3 state pairs

The problem

Decide whether two complete deterministic automata accept the same binary strings.

The checked result

Equivalent: yes.

Starting from the initial pair, the checker explores every reachable pair of states and requires matching acceptance. No mismatch is reachable, so equivalence holds for every finite binary word. Both accept an even number of ones.

Why the checker accepts it

  1. Start from the pair of initial states.
  2. Explore every symbol transition until no new pair is reachable.
  3. Compare acceptance in every reachable pair.
  4. For inequivalence, replay a distinguishing input from both initial states.

Formal specification

{
  "alphabet": [
    "0",
    "1"
  ],
  "left": {
    "start": "E",
    "accepting": [
      "E"
    ],
    "transitions": {
      "E": {
        "0": "E",
        "1": "O"
      },
      "O": {
        "0": "O",
        "1": "E"
      }
    }
  }
}

Claim and evidence

{
  "claim": {
    "equivalent": true
  },
  "witness": {
    "right": {
      "start": "A",
      "accepting": [
        "A",
        "B"
      ],
      "transitions": {
        "A": {
          "0": "B",
          "1": "C"
        },
        "B": {
          "0": "A",
          "1": "C"
        },
        "C": {
          "0": "C",
          "1": "A"
        }
      }
    }
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 3 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

Applies only to these two specified complete deterministic automata; no claim of automaton minimality.

A boundary to investigate

Bounded string testing is weaker than complete DFA product exploration. Extend the checker to emit shortest distinguishing words and state-minimization partitions.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11. No external dataset import or model-generation evaluation. Reuse-license selection remains pending.

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-014 ↘Related KL-FCS-015 ↘
KL-FCS-014
AutomataParity language under renamingComplete product reachability

The problem

Compare two isomorphic parity automata.

The checked result

Equivalent: yes.

Renaming states preserves transitions and acceptance. The checker establishes equivalence over every finite binary word.

Why the checker accepts it

  1. Start from the pair of initial states.
  2. Explore every symbol transition until no new pair is reachable.
  3. Compare acceptance in every reachable pair.
  4. For inequivalence, replay a distinguishing input from both initial states.

Formal specification

{
  "alphabet": [
    "0",
    "1"
  ],
  "left": {
    "start": "E",
    "accepting": [
      "E"
    ],
    "transitions": {
      "E": {
        "0": "E",
        "1": "O"
      },
      "O": {
        "0": "O",
        "1": "E"
      }
    }
  }
}

Claim and evidence

{
  "claim": {
    "equivalent": true
  },
  "witness": {
    "right": {
      "start": "S",
      "accepting": [
        "S"
      ],
      "transitions": {
        "S": {
          "0": "S",
          "1": "T"
        },
        "T": {
          "0": "T",
          "1": "S"
        }
      }
    }
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 2 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

This certificate concerns the declared deterministic machines only.

A boundary to investigate

Bounded string testing is weaker than complete DFA product exploration. Extend the checker to emit shortest distinguishing words and state-minimization partitions.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11. No external dataset import or model-generation evaluation. Reuse-license selection remains pending.

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-002 ↘Related KL-FCS-015 ↘
KL-FCS-015
AutomataA one-symbol counterexampleComplete product + distinguishing-word replay

The problem

Compare even-parity acceptance with the same transitions but odd-parity acceptance.

The checked result

Equivalent: no.

Reading 1 moves both machines to O. The first rejects and the second accepts. The witness refutes equivalence immediately.

Why the checker accepts it

  1. Start from the pair of initial states.
  2. Explore every symbol transition until no new pair is reachable.
  3. Compare acceptance in every reachable pair.
  4. For inequivalence, replay a distinguishing input from both initial states.

Formal specification

{
  "alphabet": [
    "0",
    "1"
  ],
  "left": {
    "start": "E",
    "accepting": [
      "E"
    ],
    "transitions": {
      "E": {
        "0": "E",
        "1": "O"
      },
      "O": {
        "0": "O",
        "1": "E"
      }
    }
  }
}

Claim and evidence

{
  "claim": {
    "equivalent": false
  },
  "witness": {
    "right": {
      "start": "E",
      "accepting": [
        "O"
      ],
      "transitions": {
        "E": {
          "0": "E",
          "1": "O"
        },
        "O": {
          "0": "O",
          "1": "E"
        }
      }
    },
    "distinguishing_word": "1"
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 2 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

A counterexample is sufficient for inequivalence; it does not characterize all differing inputs.

A boundary to investigate

Bounded string testing is weaker than complete DFA product exploration. Extend the checker to emit shortest distinguishing words and state-minimization partitions.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11. No external dataset import or model-generation evaluation. Reuse-license selection remains pending.

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-002 ↘Related KL-FCS-014 ↘

Go further.

Extend the checker to emit shortest distinguishing words and state-minimization partitions.

Questions to investigate

  1. Bounded string testing is weaker than complete DFA product exploration.
  2. Which assumption in the specification can be changed to make the current evidence insufficient?
  3. Extend the checker to emit shortest distinguishing words and state-minimization partitions.

Conceptual references

These sources explain the surrounding theory. The linked material was not imported as a dataset, and these records do not claim checking by the source’s software.

Primary conceptual reference ↗

Related areas

Programming-language semanticsType systemsSAT / SMTFormal languagesTerm rewriting