Toward a Formal Foundation for Time Travel in Stories and Games

Research areas: Year: 2016
Type of Publication: In Proceedings
  • Michiel Helvensteijn, Farhad Arbab
Editor: Erika Ábrahám, Marcello Bonsangue, Einar Broch Johnsen
Book title: Theory and Practice of Formal Methods Number: 9660
Series: Lecture Notes in Computer Science Pages: 261-276
ISBN: 978-3-319-30733-6 978-3-319-3073
Time-travel is a popular topic not only in science fiction, but in physics as well, especially when it concerns the notion of “changing the past”. It turns out that if time-travel exists, it will follow certain logical rules. In this paper we apply the tools of discrete mathematics to two such sets of rules from theoretical physics: the Novikov Self Consistency Principle and the Many Worlds Interpretation of quantum mechanics. Using temporal logic, we can encode the dynamics of a time-travel story or game, and model-check them for adherence to the rules. We also present the first ever game-engine following these rules, allowing the development of technically accurate time-travel games.