Notebook 1: Finite-State Automata

Interactive notebook for Verification and Validation Techniques at UniUD. Explore alphabets, finite words, languages, and deterministic finite automata (DFAs) hands-on.

Interactive Chapter 1 Notebook

This notebook turns the first chapter into a small laboratory. The focus is on the objects that matter early in automata theory:

  • alphabets
  • finite words
  • languages as sets of words
  • deterministic finite automata

The page is intentionally concrete. Each section lets you manipulate the definition and immediately see what changes.

Mental Model

Alphabet

A finite set of symbols. Example: {a, b}.

Word

A finite sequence built from the alphabet. Example: abba.

Language

A set of words sharing a property, such as “ends in a”.

DFA

A finite machine that reads a word left to right and decides whether that word belongs to a language.

1. Alphabet and Word Playground

Use this section to build a finite alphabet and inspect the words it generates up to a bounded length.

The key definition here is \(A^*\): the set of all finite words over the alphabet \(A\). The playground only shows a finite prefix of \(A^*\), because the full set is infinite as soon as the alphabet is non-empty.

2. Language Explorer

Now fix an alphabet and choose a property. The resulting language is the set of all words satisfying that property.

This is the main shift in viewpoint: a language is not one word, but a criterion for membership.

3. DFA Simulator

This DFA recognizes the language

\[ L = \{ w \in \{a,b\}^* \mid w \text{ contains an even number of } a \text{'s} \}. \]

The machine has only two states because parity is the only information it needs to remember.

a a b b q_even q_odd

Current Configuration

Transition Trace

    Transition Table

    State Read a Read b
    q_even q_odd q_even
    q_odd q_even q_odd

    The deterministic point should be visible here: at every step there is exactly one next state.

    4. Running Example: A Document-Editor Session

    The parity DFA above is deliberately tiny, so that its transitions are easy to calculate by hand. The editor monitor is the semantic running example used in the book. It recognizes

    \[ L_{\mathrm{session}} = \texttt{open}\,(\texttt{edit}+\texttt{save})^*\,\texttt{close}. \]

    A valid finite session opens once, performs any finite sequence of edits and saves, and closes once. The monitor does not store the document: it remembers only the phase of the protocol that determines which futures are still valid.

    Before open Only open can begin a valid session.
    Editor open edit and save preserve this phase.
    Closed · accepting The whole input must end in this state.
    Protocol error No continuation can repair the malformed prefix.

      Try open close, open edit edit save close, and the counterexample open edit close save. The last save is not merely “unexpected”: once the session has closed, no suffix can make that prefix valid again. This is the future-behaviour distinction later formalized by the Myhill–Nerode theorem.

      Reading the Definitions Back Out of the Interaction

      The notebook is useful only if the interactions map back to the formal objects.

      \(A^*\)

      The alphabet playground shows finite prefixes of the set of all finite words over an alphabet.

      \(L \subseteq A^*\)

      The language explorer separates generated words into “in the language” and “not in the language”.

      \(\delta\) and \(\widehat{\delta}\)

      The DFA simulator applies one-symbol transitions and accumulates them over a whole input word.

      Acceptance

      The final verdict depends only on the state reached after the full word is consumed.

      Exercises to Try

      1. In the alphabet playground, compare the number of generated words for maximum lengths 2, 3, and 4.
      2. In the language explorer, check whether the empty word belongs to each sample language.
      3. In the DFA simulator, try abba, aaa, bbbb, and the empty word.
      4. Explain why the DFA only needs to remember parity, not the exact number of a’s.
      5. In the editor monitor, compare open save close with open close save. At which prefix do their possible valid futures become different?