formal analysis and verification of narratives
Chris Pickett
We just submitted a paper on formal analysis and verification of IF
games using Narrative Flow Graphs, a form of Petri Net. We'd love to
hear feedback, and there's a decent chance reasonable suggestions will
get incorporated before the final submission deadline (assuming
acceptance).
http://www.sable.mcgill.ca/~cpicke/papers/pickett-05-pnfg-GAMEON-submission.pdf
or, in case that gets broken:
This is also an official source code release of version 0.1.0 of our
(P)NFG software (it's significantly better than the 0.0.2 version so I
figured a version bump was a good idea)... where else are we supposed
to "release" it?
http://www.sable.mcgill.ca/~cpicke/nfg-0.1.0.tar.gz
(that's actually Subversion working copy, for convenience)
Yes, this is early work, but we're quite optimistic about the future.
Cheers,
Chris Pickett
http://www.sable.mcgill.ca/~cpicke
P.S. If you want to run and do useful things with the software, it
will help if you are UNIX-y; the interpreter and compiler are written
in Java, but the verifier NuSMV (which we did not write) is written in
C and I'm not very sure about portability.
David Fisher
news:1120200064.0...@g14g2000cwa.googlegroups.com...
> Hi,
>
> We just submitted a paper on formal analysis and verification
> of IF games using Narrative Flow Graphs, a form of Petri Net.
> We'd love to hear feedback, and there's a decent chance
> reasonable suggestions will get incorporated before the final
> submission deadline (assuming acceptance).
>
> http://www.sable.mcgill.ca/~cpicke/papers/pickett-05-pnfg-GAMEON-submission.pdf
>
> or, in case that gets broken:
>
> http://tinyurl.com/8b93l
Wow ... it's a bit overwhelming, actually (for someone who knows nothing
about "Petri Nets" ...)
I think you've done brilliantly in creating the PNFG language, though.
So, is this the basic idea:
* PNFG is an adventure game language, though it doesn't accept natural
language input (yet)
* PNFG is translated to NFG for analysis (which would be tedious to do by
hand)
* The system analyses all possible game states
* The system calculates the (minimum) number of moves from each state to a
"winning" or "losing" state
What would you say are the major uses for this system (and potential uses) ?
Do you think it would ever get to the state of becoming an "automatic game
verifier" (or a kind of "auto Beta tester") ? Are you planning to develop
the PNFG language further (perhaps to the point of being a fully fledged IF
language), or to create an Inform-to-(P)NFG translator ?
Thanks for sharing your ideas,
David Fisher
Chris Pickett
> Wow ... it's a bit overwhelming, actually (for someone who knows nothing
> about "Petri Nets" ...)
Petri Nets are actually pretty simple, they're just finite state
machines (FSMs). Clark previously described their use for IF (see "a
structure for modern computer narratives") so that's why we don't
elaborate too much here.
http://www.sable.mcgill.ca/~clump/papers/narrative.ps
[ That paper defines everything you might want to know... don't be
scared off by its formal presentation ]
> I think you've done brilliantly in creating the PNFG language, though.
Aw shucks :) -- although the other authors should get most of the
credit for the actual compiler. It's actually pretty limited in that
it doesn't support randomness or real math operations, and currently
only has room/person--object containment as a world model (but it does
allow for arbitrary states, so you could hack it in there).
> So, is this the basic idea:
>
> * PNFG is an adventure game language, though it doesn't accept natural
> language input (yet)
Well, to be pedantic, natural language input is usually accepted at
runtime, and then parsed by the VM, as far as I understand other
systems. Our NFG interpreter/VM does not support this. Many langagues
(e.g. Inform) do allow you to guide parsing decisions ahead of time,
and yes, PNFG doesn't let you do this either (yet).
I don't think the underlying NFGs (Petri Nets) that are generated will
ever accept natural language input... we are looking towards specifying
canonical strings for actions, and having an external parser take
natural language and try to match against these strings. The idea is
that we don't want parsing to introduce extra verification complexity
(it could be verified as a separate component perhaps).
It would be interesting to learn about an LGPL-compatible parser that
we can drop into our system, if such a beast consists.
> * PNFG is translated to NFG for analysis (which would be tedious to do by
> hand)
Well, certainly the translation could be done by hand, and yes it would
be tedious, or you could just ditch PNFG altogether and write NFGs
directly (which we did at first for the Cloak of Darkness game) --
slightly less tedious, but still way too much work, too error prone,
and we don't get the high level information about the NFG structure
that lets us encode things more efficiently.
> * The system analyses all possible game states
If it's possible to do within space and time constraints. Complexity
is a big problem, and we can't currently analyse something of realistic
IF size like "The Count" (which we reimplemented). However, we have
ideas about how to attack this in future work.
> * The system calculates the (minimum) number of moves from each state to a
> "winning" or "losing" state
Yes -- it's always minimal since it's a breadth-first search in the
verifier.
> What would you say are the major uses for this system (and potential uses) ?
Well, basically it's a platform for systematic analysis of narratives.
It's still very research level (as indicated by the sub-1.0 version
number), so its major utility will be in research and not authoring
(for the time being).
However, the system can currently be used to verify small narratives,
perhaps to check all paths in a single puzzle that are too numerous and
confusing to check by hand.
Another currently useful thing (that I'm only noting from a recent
discussion) is that it's absolutely trivial to get rid of n/e/s/w
movement... you can easily have (you,go,kitchen) as one of the actions
for a room, and maybe even (you,go,back) as a global action that
attempts to return you to where you just were. In fact I think room
descriptions should change depending on whether or not you've been out
an exit (e.g. "There is a dark hallway leading out of the far side of
the room" becomes "The hallway to the kitchen leads out of the far side
of the room"). But this is all probably doable in other systems
(haven't tried).
You can see our future work section as well as the "IDEAS" file in the
tarball for things that we've thought of to date.
* Concurrent movement of (possibly non-player) characters through a
narrative, and cooperative/competitive games, and analysis thereof.
Petri Nets are normally used for concurrent analysis...
* Incorporation of sound, graphics, and different forms of I/O --
pretty easy to get since the VM is written in Java. Could be used as
the formal backbone for more genres than just IF.
* Analysis of other properties besides winnability and losability
-- how branching / linear is a narrative?
-- minimum number of steps between two states
-- e.g. "How do I get this door unlocked?", or an automatic
hint system
-- maximum number of steps (without cycles) between two states
-- partial orderings of plot points; progress towards a winning goal;
automated scoring systems based on progress
-- "pointlessness": once it becomes unwinnable, how many steps
(without cycles) until the game is over?
> Do you think it would ever get to the state of becoming an "automatic game
> verifier" (or a kind of "auto Beta tester") ?
That's the most practical, non-research goal. It won't get there for
"all games", since we can only handle a finite amount of complexity,
but hopefully we'll be able to cover an important subset. We're also
going to extend it to allow for arbitrary invariant specifications,
maybe with a syntax like, "assert(door.locked <--> torch.lit);".
Our most immediate goal wrt verification is to produce a solution for
The Count and analyse a bunch of its properties (for example, it does
have some flaws that we know of).
Are you planning to develop
> the PNFG language further (perhaps to the point of being a fully fledged IF
> language), or to create an Inform-to-(P)NFG translator ?
Both of those are are definite goals for future work. We would aim for
Inform to PNFG, not Inform to NFG. We're probably going have to define
a limited subset of the Inform language... I'm not sure if we'd ever be
able to support everything that the compiler accepts (especially since
you can do inline Z-machine assembly -- although a Z-code to NFG
translator would be an interesting exercise in its own right).
I'd like for it to be a IF language that people would actually want to
write games in, and being able to convert back-and-forth with Inform
(and/or TADS) would certainly help; the other thing that's going to
help is providing real incentive, namely getting the verification able
to handle more complex narratives and being able to look at more things
besides winnability and losability. Its current syntax needs to be
cleaned up a little too.
Cheers,
Chris
Chris Pickett
> It's actually pretty limited in that
> it doesn't support randomness or real math operations, and currently
> only has room/person--object containment as a world model (but it does
> allow for arbitrary states, so you could hack it in there).
s/hack it/hack whatever you want/
> It would be interesting to learn about an LGPL-compatible parser that
> we can drop into our system, if such a beast consists.
s/consists/exists/ :(
Chris