lstar-rocq

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

Algorithm	Resources	Proofs
L*	Angluin, 1987, Lecture Notes	Lstar.v
NL* (WIP)	Bollig et al., 2009	NLstar.v
Kearns-Vazirani	Kearns-Vazirani, 1994, Balle, 2010	KV.v
TTT	Isberner et al., 2014	TTT.v

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

Warning

By default, this project will build with ExtrOcamlNatInt, which is unsound in the event of overflow. Unless your DFAs could potentially include 2^63 states, this shouldn't be a problem. If you'd like me to support ExtrOcamlNatBigInt instead, please open an issue and I'll get on it.

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.