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 https://github.com/coq-community/reglang

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 https://github.com/coq-community/atbr or https://github.com/damien-pous/relation-algebra 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: Jan 27 2023 at 02:04 UTC