# A one-symbol counterexample

KL-FCS-015 · Automata · version 1.0.0

## Problem

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

## Context

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

## Definitions

- **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.

## Checked result

Equivalent: no.

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

## Checker reasoning

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.

## Dataset construction

{
  "family": "automata",
  "task": "Compare even-parity acceptance with the same transitions but odd-parity acceptance.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete product + distinguishing-word replay",
  "acceptance": [
    "Start from the pair of initial states.",
    "Explore every symbol transition until no new pair is reachable.",
    "Compare acceptance in every reachable pair.",
    "For inequivalence, replay a distinguishing input from both initial states."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

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

## Complexity

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

## Limits

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

## Common error and further work

Bounded string testing is weaker than complete DFA product exploration.

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

## Verification

Complete product + distinguishing-word replay. 2 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

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

- [Conceptual reference](https://ocw.mit.edu/courses/18-404j-theory-of-computation-fall-2020/download/)