Application of formal methods is always an interesting read, and this article is a gentle introduction to some of the ideas exploited in probabilistic model checking. However to me, the way the article is written, gives software verification, and CBMC in particular, an unnecessary bad reputation.

> There is no need to define “game progress” or implement a naive game AI, as formal verification methods appear to require.

> The mathematical verification code is about one-third the size of the formal verification code presented by the TTTM author

Most of the author's argumentation stems from the different levels of modelling. He pursues verification at model-level. That is, he does the interpretation that a "game progress"/"native game AI" would provide, and lifts the problem from the source-level to a formal representation as Markov process.

With that in mind, it should be clear that reasoning on that higher level can be done more efficiently. In fact, if the author of TTTM would have chosen to verify just the transition relation, an even simpler modelling would have sufficed, e.g. via Prism, ITSTools/GAL, SMV.

I just want to stress that the author of TTTM did not just formally verify that the concrete transition relation can not reach a "bad state", but proved that the actual implementation indeed cannot reach said states. For example, this also includes proving that the game's pseudo-random generation of initial states is safe to use.

> The TTTM formal verification code requires a value called MAX_FINISH_DEPTH, which represents the maximum number of steps required to finish the game from any valid state. It is unclear how the TTTM author arrived at the number 18, but the value can easily be calculated using the matrix representation of the game.

Again, when reasoning at the level of an actual implementation, i.e. software/binaries, such high-level reasoning is not applicable. Therefore, when employing bounded verification techniques, an educated guess about a sufficiently high number of steps must be provided.

I’m an engineer, have a degree in Gamedesign and turned UX/UI designer. Many lessons from adventure games/level design are very useful to apply when designing SaaS products (not talking about “gamification”. Dead ends is particularly an interesting point in the experience.

One way you could apply lessons from game design into crafting better software products is by breaking down what a game is. Think of it as 3 layers.

- 1. Set of rules (ex. Finish before opponent)

- 2. A story/shell around those rules (ex. Race car/horse riding/athletics/etc)

- 3. Rewarding Experience (ex. Real-world Monetary reward/nice video/animation with your character holding a trophy etc)

——

3. Is the reason people use your product. What real-world benefit are they seeking?

2. This is the UI of your product. A race game has a different vibe and audience than a horse racing game. Even though they have the same underlying ruleset. So make sure you tailor your UI to your audience.

1. This is the UX of your product. Here you’ll get core lessons from gamedesign (like dead ends discussed in the article)

You Can always contact me with Ui/UX questions, find my contact details in my bio.

Isn't this overkill to verify that you don't have any invalid states? Consider the state machine as a directed graph, reverse each edge and run DFS from the end state. if you have any vertices in the graph you didn't visit, they're dead ends. That should be more efficient than the O(n^3) way of finding eigenvectors.