Linear Logic System Architecture

Our architecture is based on two components: an Interactive Storytelling rendering and an Interactive Storytelling controller.

The controller aims to manage the unfolding of the history by taking into account the player actions and according to the structure of the narrative pre-defined. The controller is based on a computational model of Interactive Storytelling: Linear Logic. We adapt Greimas analysis to the constraints of Interactive Storytelling.

Greimas was the first to develop narrative formalism as an abstract formula to represent an action (narrative program). He proposed to define an action as a transition from one state to another state where the subject gains or loses an object (conjunctive or disjunctive narrative program).

Linear Logic has been introduced by J.-Y. Girard as a restriction of classical logic. Unlike classical logic, Linear Logic is not used to determine whether an assertion is true or not but rather the validity of how formulas are used (and then consumed) when proving an assertion. Linear Logic is well suited to derive a computational model to partially ordered problems with resource sharing.

The main connector of Linear Logic are:


  • ⊸: Implication (imply), express the possibility of deduction. Example: 2€ ⊸ trawberries . Means that I can give 2 € to buy strawberries.
  • ⊗: Multiplicative conjunction (times), a set of resources (not ordered). Example: strawberry strawberry . Means that there are two different strawberries (strawberry 2)
  • ℘: Multiplicative disjunction (par). Example: strawberry ⊗2 ℘ strawberry ⊗5. Means that there is two set of strawberries (one belongs to Alice and the other one to Bob for instance)

  • ⊕: Additive disjunction (plus), external choice. Example: strawberry ⊕ raspberry . Expresses a choice (external to the process). The player can choose strawberry or raspberry 
  • &: Additive conjunction (with). Example: strawberry & raspberry . Expresses a choice (internal to the process). The game can choose strawberry or raspberry 

  • ⊢: Turnstile, separate the left part (antecedent) and the right part (consequent) of a sequent. Example: D , D E E Linear implication express the possibility to produce a copy of E by consuming a copy of D AND a copy of ⊸ E 


A sequent of Linear Logic expresses all the possible narratives of a story. Each narrative corresponds to a proof of the sequent (Proving a sequent consists in rewriting the sequent by making a substitution of the formulas in order to have an initial sequent). As the proof is not unique, we can deduce various narratives.

The following sequent: A, C , D , A C B C , D E , E C F C B C  F; gives the following proof graph (simplified to the substitution of the linear implication).

It is then possible to compute a sequent by using Petri nets. It has been proved that there is an equivalence between a sequent of Linear Logic and a Petri net (with some restrictions). A token player algorithm is then used to compute the model of Interactive Storytelling.