How is the verification of computer role-playing games carried out?

Question

Game development

Suppose a game (like Fallout) has an extensive dialogue system. Some branches of the dialogue appear, others disappear. Exhaustive testing is extremely difficult.
Tell me what formalisms are better to use (both in the engine and in the checker) in order (assuming that the engine is correct) to prove some statements about this very system of dialogues. For example…
* From any state the game is passable.
* The player will be able to cooperate with any of the Mordino, Salvatore, Bishop or Wright families, but only with one.
Well, of course, the tester should be written in a couple of days: after all, we are not writing a tester, but a game. Or maybe you can do without a checker at all - the model itself is designed in such a way that you can see what state it can go into and which one it can’t.
Petri nets? Even they seem to be complex and must be limited by something - for example, chips do not appear and disappear.

Answer 1

I have one idea. Let's build some finite automata. For each replica, the following are specified:
— automaton (zero or one);
- a set of states in which the replica is visible (one or more; it makes sense if the automaton is set);
- where to switch the machine;
- some additional conditions depending on the game (for example, the level of intelligence or conversation);
- a link to the function-special condition (there should be a couple of dozen of them for the entire large Fallout).
For example, for the four "Mordino / Salvatore / Bishop / Wright" there will be five states: with no one and with some of the families. Then it is enough to see that it is impossible to go from Mordino to any other, and here is the proof for you: you are a member of the Mordino gang for life. And if some line of dialogue includes special conditions or two automata at the same time, the checker will display a message: be on your guard here.
Some automata may have one or more "final" states - you can establish a hierarchy of automata. Top-level automata may require lower-level automata to be in a final state, but not vice versa.