Modeling and formal verification of gaming storylines

Simple item page
dc.contributor.advisorFussell, Donald S., 1951
dc.contributor.advisorElster, Anne C.
dc.contributor.committeeMemberAbraham, Jacob
dc.contributor.committeeMemberChase, Craig
dc.contributor.committeeMemberMiikkulainen, Risto
dc.creatorHolloway, Lane Thomas
dc.creator.orcid0000-0002-1564-228X
dc.date.accessioned2016-10-04T19:47:24Z
dc.date.accessioned2018-01-22T22:30:40Z
dc.date.available2016-10-04T19:47:24Z
dc.date.available2018-01-22T22:30:40Z
dc.date.issued2016-05
dc.date.submittedMay 2016
dc.date.updated2016-10-04T19:47:25Z
dc.description.abstractVideo games are becoming more and more interactive with increasingly complex plots. These plots typically involve multiple parallel storylines that may converge and diverge based on player actions. This may lead to situations that are inconsistent or impassable. Current techniques for planning and testing game plots involve naive means such as text documents, spreadsheets, and critical path testing. Recent academic research [1] [2] [3] examines the design planning problems, but neglect testing and verification of the possible plot lines. These complex plots have thus until now been handled inadequately due to a lack of a formal methodology and tools to support them. In this dissertation, we describe how we develop methods to 1) characterize storylines (SChar), 2) define a storyline description language (SDL), and 3) create a storyline verification tool based in formal verification techniques (StoCk) that use our SDL as input. SChar (Storyline Characterization) help game developers characterize the category of story line they are working on (e.g. linear, branching and plot) through a tool that give a set of guided questions. Our SDL allows its users to describe storylines in a consistent format similar to how they reason about storylines, but in such a way that it can be used for formal verification. StoCk accepts storylines, described in SDL, to be formally verified using SPIN for errors. StoCk is also examined in three common use cases found in the gaming industry used as a tool 1) during storyline creation 2) during quality assurance and 3) during storyline implementation. The combination of SChar, SDL, and StoCk provides designers, writers, and developers a novel methodology and tools to verify consistency in large and complex game plots.
dc.description.departmentElectrical and Computer Engineering
dc.format.mimetypeapplication/pdf
dc.identifierdoi:10.15781/T2RF5KH20
dc.identifier.urihttp://hdl.handle.net/2152/41455
dc.language.isoen
dc.subjectFormal verification
dc.subjectGaming storyline
dc.subjectGames
dc.subjectModeling
dc.subjectModeling tools
dc.titleModeling and formal verification of gaming storylines
dc.typeThesis
dc.type.materialtext

Files

Collections

University of Texas at Austin