Stream: Coq users

Topic: Encoding and reasoning about FSMs

view this post on Zulip Soren (May 28 2020 at 18:53):

I have a IsEmpty: MyState -> Prop and Steps: MyState -> list MyState. I want to prove that, for every starting state that satisfies IsEmpty, there exists at least one state that satisfies IsEmpty after exactly 10 steps. Is there a good guide/example on how to prove stuff FSM stuff like this with Coq?

Additionally, is it possible to _enumerate_ valid IsEmpty output states given an input state?

view this post on Zulip Karl Palmskog (May 28 2020 at 19:18):

something with type MyState -> list MyState is not necessarily an FSM, so it can't be proven in general. If you're looking for more carefully constructed Coq types for which FSM properties hold, see

If MyState is indeed finite you can show that it is a finite type (finType) and hook into all the results about, e.g., DFAs and NFAs. finTypes give access to all kinds of enumerations as lists/finite sets.

view this post on Zulip Soren (May 28 2020 at 19:25):

Ah, MyState -> list MyState is the list of "next" states by a certain transformation. I'm certain I can express it as a DFA, I'll check that out.

view this post on Zulip Karl Palmskog (May 28 2020 at 19:31):

first step would simply be to prove that MyState is finite by defining a list with type members and showing that the list is sound and complete. This means that MyState -> list MyState can be expressed as a finite function (finfun), which is essentially what NFAs and DFAs use for their transition relation. Note that if your only goal is to prove a simple reachability property, reglang might be considered a heavyweight library, so you could also take a look at or for other encodings of FSMs.

view this post on Zulip Soren (May 28 2020 at 19:49):

I'll probably use reglang just in case I need to do more with it than prove reachability

view this post on Zulip Christian Doczkal (May 29 2020 at 08:04):

@Soren As the main developer of the reglang package, I would be happy to know if the library turns out useful for you or not, and for what reason. IIRC, the representation for "finite automata" in relation-algebra is matrices over regular expressions (elements of a Kleene algebra), with NFAs carved out as a predicate. Can't say much about atbr except that that I recall the automata model do be geared for execution (the statespace ist described as "all n below a given bound") rather than for simple proofs (by using finite types).

Last updated: Jun 18 2024 at 00:02 UTC