package lstar-rocq

lstar-rocq

A collection of formally-verified implementations of automata learning algorithms.

These notes summarize each of the main proof arguments and algorithm designs.

Functions return sigma types, so each sub-component of each algorithm provides a proof of correctness alongside its computational outputs.

Layout

• automata - definitions for alphabets, regular languages, and automata, including the correctness properties of language encoding and minimality
• Teacher.v - definitions for the Minimum Adequate Teacher model
• ListLemmas.v - miscellaneous lemmas about lists
• RS.v - a general-purpose implementation of Rivest-Schapire counterexample analysis, used in the implementations of L*, KV, and TTT
• Teacher.ml - OCaml entrypoint for using the extracted library, provides a single module interface to instantiate all of the learning algorithms

Installation

# Will install both lstar (the OCaml release) and lstar-rocq (the Rocq theory development)
opam install lstar

Building

# Install Dependencies
opam switch create rocq 5.3.0
opam pin add rocq-runtime 9.1.0
opam install rocq-prover dune

# Clone and build
git clone https://github.com/CharlesAverill/lstar-rocq && cd lstar-rocq
make # will build lstar-rocq, extract, then build lstar

Example

An example execution is provided in alternating.ml. The target language is alternating bit strings (e.g., "01", "10", "101", "0101", etc.). Running dune exec lstar.alternating will start the learning algorithm, report that it has found a DFA that encodes the language, and then run some test cases for bit strings of length 3:

$ dune exec lstar.alternating
DFA found                          
Input       Expected  Got       Correct 
[000]       false     false     Y
[001]       false     false     Y
[010]       true      true      Y
[011]       false     false     Y
[100]       false     false     Y
[101]       true      true      Y
[110]       false     false     Y
[111]       false     false     Y
Accuracy: 8/8

Examples lstar.div7 and lstar.mod3 show the learning of DFAs for decimal strings divisible by 7, and binary strings where the number of 1s is divisible by 3.