Ceptre: A Language for Modeling Generative Interactive Systems.

We present a rule specification language called Ceptre, intended to enable rapid prototyping for experimental game mechanics, especially in domains that depend on procedural generation and multi-agent simulation. Ceptre can be viewed as an explication of a new methodology for understanding games based on linear logic, a formal logic concerned with resource usage. We present a correspondence between gameplay and proof search in linear logic, building on prior work on generating narratives. In Ceptre, we introduce the ability to add interactivity selectively into a generative model, enabling inspection of intermediate states for debugging and exploration as well as a means of play. We claim that this methodology can support game designers and researchers in designing, anaylzing, and debugging the core systems of their work in generative, multi-agent gameplay. To support this claim, we provide two case studies implemented in Ceptre, one from interactive narrative and one from a strategy-like domain. Introduction Today, game designers and developers have a wealth of tools available for creating executable prototypes. Freelyavailable engines such as Twine, Unity, PuzzleScript, and Inform 7 provide carefully-crafted interfaces to creating different subdomains of games. On the other hand, to invent interesting, novel mechanics in any of these tools typically requires the use of ill-specified, general purpose languages: in Twine, manipulating state requires dipping into JavaScript; in Unity, specifying any interactive behavior requires learning a language such as C# or JavaScript; Inform 7 contains its own general-purpose imperative, functional, and logic programming languages; and PuzzleScript simply prevents the author from going outside the well-specified 2D tile grid mechanisms. The concept of operational logics (Mateas and WardripFruin 2009), the underlying substrate of meaningful statechange operations atop which mechanics are built, was recently proposed as a missing but critical component of game design and analysis. In most prototyping tools, there is a Copyright c © 2015, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. fixed operational logic (e.g. tile grids and layers in PuzzleScript, or text command-based navigation of a space in Inform 7) atop which the designer may be inventive in terms of rules and appearance, but all rules must be formed out of entities that mean something in the given operational logic (or use a much more complex language to subvert that default logic). We lack good specification tools for inventing new operational logics, or combining elements from several. In particular, many novel systems of play arise from the investigation of interactive storytelling (Mateas and Stern 2003), multi-agent social interaction (McCoy et al. 2010), and procedurally generated behavior (Hartsook et al. 2011), and no existing tools make it especially straightforward for a novice developer to codify and reason about those systems. Ceptre is a proposal for an operational-logic-agnostic specification language that may form the basis of an accessible front-end tool. It is based on a tradition of logical frameworks (Harper, Honsell, and Plotkin 1993), which use logical formulas to represent the rules of a system (a specification). Then proof search may be used to simulate execution, answer queries, and perform analysis of the specification. In Ceptre, we specify games, generative systems, and narratives with similar payoff. Our logic of choice for representing games is linear logic (Girard 1987), unique among logics in its ability to model state change and actions without the need for a frame rule or other axiomatization of inertia for predicates that do not change in an action. Using linear logic to specify a space of play closely resembles planning approaches. Planning has been used extensively to study games, especially in the interactive storytelling domain (Mateas and Stern 2003; Porteous, Cavazza, and Charles 2010; Medler and Magerko 2006) but also as a general mechanic description language (Zook and Riedl 2014). In contrast to this work, we position Ceptre as unique among game description languages in its combination of (a) direct correspondence to a pre-existing logic and proof theory, providing a portable and robust foundation for reasoning about games, and (b) use as a native authoring language, rather than as a library or auxiliary tool. On the other hand, unlike prior executable description languages (e.g. (Dormans 2011; Osborn, Grow, and Mateas 2013)), we retain the planning-like ability to specify generalized rule schema that apply in a multi-agent setting, allowing for causal analysis of event sequences. These statements Proceedings, The Eleventh AAAI Conference on Artificial Intelligence and Interactive Digital Entertainment (AIIDE-15)