temporal properties in IF
Chris Pickett
Many IF games can be modelled straightforwardly using finite state
machines (automata). What are some of the interesting properties? I
know several of these have been discussed. So far I have:
1) Winnability:
"There exists a path from the current state to a winning state"
In CTL: EF win
1b) Path to winning state:
Counterexample produced by model checker when fed:
"There does not exist a path from the current state to a winning state"
In CTL: !EF win
2) Extend (1) to arbitrary reachability:
EF door.unlocked
EF lose
etc.
3) No zombie states possible:
"From all states, there is a path to either a winning state or a losing
state"
In CTL: AG(EF win || EF lose)
4) Distance between states:
"What is the minimal number of commands needed to reach state s"
or, length of counterexample produced by "!EF s" (see 1b), where each
transition in the FSM is labelled with a command the user must enter.
Counterexamples produced by model checkers are minimal, since a BFS is
used by most if not all tools.
5) Minimal change in some variable s between current state and state s
(extension of (4)):
a) what is the cheapest way to reach state s (in zorkmids)?
b) what is the fastest way to reach state s (in game time)?
c) what is the fastest way to reach state s (in commands entered, where
some transitions are not labelled with/guarded by commands and are
silent, occurring internally)
6) "Separation" between states:
Maximum number of transitions (or commands entered, per 5c), without
cycles.
7) Degree of "pointlessness":
A game is pointless if it is not possible to win. The degree of
pointlessness is the maximum separation between not being able to win
and actually losing. For example, a game is 5-pointless if no matter
what, as soon as you are unable to win, you will lose in a maximum of 5
moves, as long as each new state you enter is unique.
This can also be thought of as the "reoccurrence radius" between not
being able to win and losing. The reoccurrence radius is the longest
path from some initial state (here, an unwinnable state) to any other
state. Assuming we don't have a zombied game, the last state on the
path is the losing state. This is the last state in a reoccurrence
radius path from an unwinnable state.
8) Non-linearity:
Given two states A and B (e.g. start and win), the number of different
paths between them without cycles.
8b) True non-linearity (it's probably a bad name):
# of paths between A and B, but only computable if there are no common
intermediate states.
8c) Effective non-linearity (not sure about this one semantically):
Take two states A and B, identify all paths between them, find all of
the common intermediate states. Compute true non-linearity between all
common states on each path between A and B.
The effective non-linearity is the maximum value you get by considering
an arbitrary path and summing together all of the true non-linearity
values between A and B.
Cheers,
Chris
Chris Pickett
Just replying to myself re: the lack of responses.
A thread entitled "Unwinnable" recently had 32 messages in it.
However, I think there are lots of interesting things to talk about in
narrative verification and analysis besides reachability of win/lose.
Nobody else?
I'm not complaining, I just feel dumb/awkward for not getting any
responses. What's wrong with what I wrote? In my mind it's just
barely formal. I'd be happy to explain something that doesn't make
sense.
Chris
Depresiv
I think the problem is that tere are TOO MANY things to talk about in
your resume above, and also I think that not many people here would be
able to understand what you are talking about (I also find it very
difficult). Just guessing, maybe you would find more interest in an
algebra-related forum.
Just some comments:
> 3) No zombie states possible:
> "From all states, there is a path to either a winning state or a losing
> state"
Not true for all IF works. I have written an experimental IF work,
"Lemniscata", where it is not possible to win nor to lose.
Also, there are games where an action locks the player from reaching a
winning or losing state. (Say, being inside a cell, you accidentally
break the key)
> 4) Distance between states:
Is it possible to know this "minimum" easily? In "The Hobbit", by
Melbourne House, lots of situations happen randomly: Characters move
about through the game world, there is a "chance" where some difficult
actions succeed or fail, there is a "chance" for something happening
(or not) in a location...
Well, anyway, as you see, I may have completely missed the point of
what you were saying :-)
Depresiv
Dan Shiovitz
Hrm. I did have the post on my to-reply pile for a bit, but eventually
decided I didn't really have anything interesting to say on the
matter. I think for me the difficulty is that the way you're
presenting this topic is both too complex and too simple -- on the one
hand it's aiming at a powerful high-level analysis of all IF games,
but on the other it doesn't really seem to be producing anything
useful or applicable to how I write or play games.
Like, yeah, I'd definitely be interested in something that could look
at my source code and decide if the game can be made unwinnable and
how, but that's quite a ways off from what you're talking about (and
I'm not sure how much restriction on the programming language I'd be
willing to accept to get this analysis capability added, because I can
already get pretty close to 100% analysis on my own). The stuff
besides winnability isn't generally that interesting to me -- unless I
was writing an extremely resource-limited game like All Things Devours
I don't generally care about minimum number of moves to win or the
like.
All that said, there are two areas where this kind of analysis might
be more useful for me. The first one is on puzzles -- while I don't
generally write stuff where the overall game has resource limits, I
often write puzzles that have them, or puzzles that can be easily
mapped to state machines. It'd potentially be useful, if the puzzles
are complicated enough, to have automatic proof that there still
exists a winning solution and I haven't broken anything, or to make
sure the player can get through it in at most 5 turns or whatever. It
seems like it might be possible to write an adaptive hint system by
analyzing where the player is in the puzzle too. The other place is
plot. Analysis and self-modification of plot a la Emily Short's scene
manager is something I'm extremely interested in -- I'd very much like
to know where the player is in the story and what the best next scene
to have is, given what's gone before. But I'm not sure how much your
stuff can do that automatically, since it seems like it'd require a
lot of hand-coding by the author anyway.
So, yeah, that's why I didn't reply, I guess -- what you've talked
about seems theoretically interesting but not particularly applicable
in practice.
>Chris
--
Dan Shiovitz :: d...@cs.wisc.edu :: http://www.drizzle.com/~dans
"He settled down to dictate a letter to the Consolidated Nailfile and
Eyebrow Tweezer Corporation of Scranton, Pa., which would make them
realize that life is stern and earnest and Nailfile and Eyebrow Tweezer
Corporations are not put in this world for pleasure alone." -PGW
Samwyse
> In article <1134530755.6...@z14g2000cwz.googlegroups.com>,
> Chris Pickett <cpi...@gmail.com> wrote:
>
>>Just replying to myself re: the lack of responses.
>>
>>A thread entitled "Unwinnable" recently had 32 messages in it.
>>However, I think there are lots of interesting things to talk about in
>>narrative verification and analysis besides reachability of win/lose.
>>Nobody else?
>
> be more useful for me. The first one is on puzzles -- while I don't
> generally write stuff where the overall game has resource limits, I
> often write puzzles that have them, or puzzles that can be easily
> mapped to state machines. It'd potentially be useful, if the puzzles
> are complicated enough, to have automatic proof that there still
> exists a winning solution and I haven't broken anything, or to make
> sure the player can get through it in at most 5 turns or whatever. It
> seems like it might be possible to write an adaptive hint system by
> analyzing where the player is in the puzzle too. The other place is
> plot. Analysis and self-modification of plot a la Emily Short's scene
> manager is something I'm extremely interested in -- I'd very much like
> to know where the player is in the story and what the best next scene
> to have is, given what's gone before. But I'm not sure how much your
> stuff can do that automatically, since it seems like it'd require a
> lot of hand-coding by the author anyway.
I think that this sort of analysis could be useful to someone designing
a new IF platform (and we all know how successful those are). I have a
long interest in describing games using higher-level constructs.
(Unfortunately, I don't have the time to implement many of my ideas.)
Rather than analyzing an existing game, I'd like to see a tool that
describes a game using your concepts and then turns that description
into a game (possibly with Inform or TADS source as an intermediate step).
Chris Pickett
> Hi Chris:
>
> I think the problem is that tere are TOO MANY things to talk about in
> your resume above, and also I think that not many people here would be
> able to understand what you are talking about (I also find it very
> difficult). Just guessing, maybe you would find more interest in an
> algebra-related forum.
Hmm, maybe I just need to motivate things more. I'm interested in
specifying various properties in IF games, and then using some software
to look for them automatically. I have something that handles
reachability for small examples, and can print a path to winning or
losing states, and am now working on improving it to handle larger
examples. At the same time, I am trying to think of other things
besides reachability that we might want to look for.
> Just some comments:
>
> > 3) No zombie states possible:
> > "From all states, there is a path to either a winning state or a losing
> > state"
Okay, so this is just something you _might_ want. It depends on the
game author/designer.
> Not true for all IF works. I have written an experimental IF work,
> "Lemniscata", where it is not possible to win nor to lose.
For example :)
> Also, there are games where an action locks the player from reaching a
> winning or losing state. (Say, being inside a cell, you accidentally
> break the key)
Right, so this would be an example of a zombie state. The point is,
the game designer might not actually realize such a state exists -- it
would be nice to discover them. Similarly, the player might want to
ask the game, "Am I in a zombie state?" or perhaps even be notified
after 5 turns of being zombied or something.
> > 4) Distance between states:
>
> Is it possible to know this "minimum" easily? In "The Hobbit", by
> Melbourne House, lots of situations happen randomly: Characters move
> about through the game world, there is a "chance" where some difficult
> actions succeed or fail, there is a "chance" for something happening
> (or not) in a location...
Ok, so randomness certainly introduces a lot of complexity, but there
are ways of dealing with it (probabilistic automata and such).
However, for now I am thinking about games that are single-player,
turn-based, and don't use any random or floating point numbers.
Integer multiplication and division are probably out of the question as
well. Still, I think that many things can still be expressed.
> Well, anyway, as you see, I may have completely missed the point of
> what you were saying :-)
No, not at all, thanks for replying. I'm just trying to get ideas
about what people think might be interesting properties that vary over
the course of a game.
Another one that recently occurred to me:
"Object liveness"
Many adventure games revolve around collecting huge numbers of objects,
moving them between rooms, and using them. Yet, for many of these
objects, there is only a short period during the game in which they are
actually used.
The weakest definition of object liveness could be the period in the
game between when an object is first interacted with by the player or
game world, and when the same object is interacted with for the last
time.
A stronger definition might exclude actions like "pick up, drop,
examine" after the object has been "usefully" used for the last time.
The points of determining liveness might be:
1) showing the designer how many objects the player has to think about
at once.
2) letting the player know which objects he still has to carry around
with him
3) reducing complexity of reachability analyses -- if objects O1 and O2
are never live at the same time, then we can possibly use the same bits
to represent them.
Cheers,
Chris
Chris Pickett
> Hrm. I did have the post on my to-reply pile for a bit, but eventually
> decided I didn't really have anything interesting to say on the
> matter. I think for me the difficulty is that the way you're
> presenting this topic is both too complex and too simple -- on the one
> hand it's aiming at a powerful high-level analysis of all IF games,
> but on the other it doesn't really seem to be producing anything
> useful or applicable to how I write or play games.
We have some software that handles small examples (5 or 6 steps) using
a very rudimentary IF language, and we wrote a paper about it in the
summer.
I'm trying to find ways to make it more useful, even if only for these
small examples. At this point I'm not so worried about the practical
implementation details, I'm just assuming they're already sorted out
(they will be eventually... hopefully I don't die first).
> Like, yeah, I'd definitely be interested in something that could look
> at my source code and decide if the game can be made unwinnable and
> how, but that's quite a ways off from what you're talking about (and
> I'm not sure how much restriction on the programming language I'd be
> willing to accept to get this analysis capability added, because I can
> already get pretty close to 100% analysis on my own). The stuff
> besides winnability isn't generally that interesting to me -- unless I
> was writing an extremely resource-limited game like All Things Devours
> I don't generally care about minimum number of moves to win or the
> like.
Yeah, for larger things it's still impractical... we expressed "The
Count" in our language but there's no way we could verify it at the
moment.
> All that said, there are two areas where this kind of analysis might
> be more useful for me. The first one is on puzzles -- while I don't
> generally write stuff where the overall game has resource limits, I
> often write puzzles that have them, or puzzles that can be easily
> mapped to state machines. It'd potentially be useful, if the puzzles
> are complicated enough, to have automatic proof that there still
> exists a winning solution and I haven't broken anything, or to make
> sure the player can get through it in at most 5 turns or whatever.
> It seems like it might be possible to write an adaptive hint system by
> analyzing where the player is in the puzzle too.
A small puzzle is definitely something where we can handle
reachability, and print full or partial winning solutions at any point.
But, ok, fair enough, all you're really interested in here is
reachability, and that's already been discussed ad nauseum.
The other place is
> plot. Analysis and self-modification of plot a la Emily Short's scene
> manager is something I'm extremely interested in -- I'd very much like
> to know where the player is in the story and what the best next scene
> to have is, given what's gone before. But I'm not sure how much your
> stuff can do that automatically, since it seems like it'd require a
> lot of hand-coding by the author anyway.
Thanks, I'll take a look at that. Verification techniques might well
be able to ensure an appropriate ordering of scenes (e.g. X never
occurs before Y, or Y always occurs between X and Z, if it occurs at
all, etc.). But yes, of course the author would still have to write
the software that causes changes between scenes.
Cheers,
Chris
schi...@altern.org
The project of characterizing IF games (IFG) formally looks like a very
interesting one! Some thoughts from the top of my head:
You say IFG are automata. I would have thought it more natural to
approximate them as nondeterministic Turing Machines (NTM). Every
choice open to the player is equivalent to a situation in which the NTM
is in a state Qi, and scanning a symbol Sj with its head and there are
more than one quadruple beginning with "Qi Sj..." of the form
Qi Sj A Qm
(where A is either L (move the head to the left), R (move the head to
the right), or Sk (print symbol Sk).
That is, the IFG is in one state (defined by Qi and Sj) and the player
has to choose which quadruple to follow. If you are not familiar with
this terminology (its the one I've studied, but I'm not sure whether
it's completely standard!) please let me know.
If this is true, and an analysis of IFG can be offered in terms of NTM,
some of the problems you mention can be rephrased as well-known
problems of recursion theory. In particular there may be something
fishy with your Zombie operator:
"From all states, there is a path to either a winning state or a losing
state"
You want a Zombie predicate such that, when applied to an IFG, gives
you the information of whether the IFG will stop or not. This is
analogous to the well-known "Halting Problem": it can be
demonstrated that the predicate
HALT (x,y) = program number y eventually halts on input
is not a computable one. That is, if IFG can be analysed as NTM, there
is no way to compute the Zombie predicate.
Another interesting thing. Normally programs calculate functions, that
is, they expect an input x by the user and offer a result y = f(x).
Nevertheless, in IFG there is no input as such. Every "input" is
fixed by the programmer, and the interactivity comes rather in the
choosing of the different alternative quadruples that form the NTM.
But, formally, every NTM is equivalent to a deterministic Turing
Machine so, from the point of view of computability, IFG are not
interactive at all. This is simply a bombastic way to put the following
trivial point: a machine could reach the winning halt (and, for that
matter, all losing halts) by simply following every alternative in
turns at each crossroad.
Best,
Manolo
Charles A. Crayne
schi...@altern.org wrote:
:You want a Zombie predicate such that, when applied to an IFG, gives
:you the information of whether the IFG will stop or not.
To the contrary, he wants a predicate which indicates if it is possible
for the IFG to reach a stop state -- which is an entirely different
matter.
-- Chuck
Chris Pickett
> In particular there may be something
> fishy with your Zombie operator:
>
> "From all states, there is a path to either a winning state or a losing
>
> state"
> You want a Zombie predicate such that, when applied to an IFG, gives
> you the information of whether the IFG will stop or not.
Not will stop, but can stop. I want to know if there exists some
sequence of commands the player can type in to make it stop. Since the
state space is finite, this is possible to check exhaustively (assuming
you have an efficient representation).
> This is
> analogous to the well-known "Halting Problem": it can be
> demonstrated that the predicate
>
> HALT (x,y) = program number y eventually halts on input
>
> is not a computable one. That is, if IFG can be analysed as NTM, there
> is no way to compute the Zombie predicate.
Don't think about it in terms of the Halting Problem, it's not the same
thing. Think about it in terms of reachability between two nodes in a
directed graph, where each node is some state in your finite state
machine, and the edges are transitions, some of which may be labelled
with inputs and/or outputs.
> Another interesting thing. Normally programs calculate functions, that
> is, they expect an input x by the user and offer a result y = f(x).
> Nevertheless, in IFG there is no input as such. Every "input" is
> fixed by the programmer, and the interactivity comes rather in the
> choosing of the different alternative quadruples that form the NTM.
> But, formally, every NTM is equivalent to a deterministic Turing
> Machine so, from the point of view of computability, IFG are not
> interactive at all. This is simply a bombastic way to put the following
> trivial point: a machine could reach the winning halt (and, for that
> matter, all losing halts) by simply following every alternative in
> turns at each crossroad.
Yes, I think so too. Model checking algorithms usually depend on some
kind of BFS to determine satisfiability or validity of properties.
I think the key point as far as your argument is concerned is that the
state space is finite, there is no infinite tape. This may not be true
for all IF games (okay, I suppose we always have physical hardware
limitations), but it is true for the ones I'm talking about. Note that
I think this is an important class of narratives.
Cheers,
Chris
Samwyse
> schi...@altern.org wrote:
>>You want a Zombie predicate such that, when applied to an IFG, gives
>>you the information of whether the IFG will stop or not.
>
> Not will stop, but can stop. I want to know if there exists some
> sequence of commands the player can type in to make it stop. Since the
> state space is finite, this is possible to check exhaustively (assuming
> you have an efficient representation).
I suspect that the two problems are equivalent, since a Turing machine
with a finite tape can also be modeled as a finite state space. Given
enough time, one can determine whether it will stop or not, the question
is whether there's enought time to find out before the sun cools.
As a practical matter, we are interested in a vanishingly small fraction
of all possible IFGs, so we are more interested in practical matters,
like whether a resource deadlock can occur. The earlier that one can
detect that, the better; thus my interest in higher level tools that
make it difficult to create such situations.
Charles A. Crayne
Samwyse <sam...@gmail.com> wrote:
:I suspect that the two problems are equivalent,
Not at all equivalent, as can be demonstrated by a trivial example:
Consider a game consisting of a single room, in which the only way to
win is to get out, by saying "Rumblestiltskin" (a typo by the game
author). In this example, it is clear that the player CAN win
the game at any time, but is highly unlikely to ever actually do so.
-- Chuck
Samwyse
What, you think the player will never make the same typo? "Highly
unlikly" is not the same as "never".
Charles A. Crayne
Samwyse <sam...@gmail.com> wrote:
:"Highly unlikely" is not the same as "never".
Indeed so, and if the player has seen some references to spinning straw
into gold, then the odds are cut even more. However, the topic under
discussion is not probability, but "The art of the possible".
Consider a more realistic example:
A player is placed in a set of connected rooms, which initially have no
exit. However, the player has a stock of dynamite, and is aware that an
exit may be created by setting off an explosion at the appropriate point.
If, however, the blast occurs at any other point, the ceiling collapses.
[i.e. the room is removed from the game.]
Assuming that the game is initially winnable, and that the player has
enough sense not to be blown up while setting off the dynamite, then,
after each explosion, it is desirable that the game be able to calculate
if the game is still winnable.
The required calculation is merely to determine if a path still exists
between the player's current location, and the correct place to create an
exit. Algorithms for such calculations are well known, and have nothing to
do with the 'halting problem'.
-- Chuck
Chris Pickett
You can represent this particular example with a two-state transition
system. The initial state s0 is labelled by the proposition "the
player is in the single room", and the accepting (final) state s1 is
labelled by the proposition "the player has won". There is a single
transition between these two states, labelled by the input string
"Rumblestiltskin" and perhaps the output string "Congratulations!" or
what have you. There are also many (infinitely many, if you like)
transitions from s0 back to s0 labelled by other input strings such as
"Rumplestiltskin", "asdf", and "fuck off", perhaps each with an output
string, "Sorry, try again".
I think the point is that to find a winning solution, all you have to
do is check all your states for the proposition "the player has won"
and then backtrack to those states that can make a transition into this
state; when you hit an initial state (in this case s0, the only
possible choice), you have an answer from the start of the game.
I think the other point is that this is clearly different from checking
all possible inputs or sequences of inputs starting from s0, finite or
infinite.
Not being too well-versed in complexity theory, I might have made a
mistake here. But I do know that model checking is well developed as a
field, and that if you can express your system as an FSM then it really
can work, for things as large as 2^200 potential states (200 boolean
variables). Indeed, we managed to express The Count by Scott Adams in
about this many booleans, we just can't model check it right now, but I
think it's mostly a representation issue that actually will be solved
sooner rather than later (touch wood).
Chris