Fun with Temporal Logic

Hi guys! Today I’m gonna talk a little bit about some nice piece of math – temporal logic. It may not be so entertaining or interesting for you as some tech posts about technologies and languages, but I just have to make some kind of intro for you to understand what my master thesis really is about. Tl;dr at the bottom. ;)

Why Classical Predicate Calculus is not enough?

Through the ages mathematicians have developed and proved many concepts of logical reasoning. Classical Predicate Calculus is the tool that allows to write down relations in a form of formulas and then arbitrate its truthfulness. This system is well suited for describing some rules that are time – invariant. Sometimes that is not enough – we need to define these rules in different time moments. Attempts to modelling time-variant relations would result in necessity of analyzing an infinite number of time moments. Other words – we would have to define formulas for each time moment: \(i, i+1, i+2, … \). Obviously, that would be nearly impossible to implement in real computer system.

Unravelling the Temporal Logic

This type of logic introduces some special modal operators that allow to model the flow of time. It describes time-variant relations without specifying time explicit. There are many different types of temporal logic, but we will focus on one of the most straightforward - LC logic. It uses a \(C\) operator, which took its name from the term change, since it operates on the concept of change, rather than time itself. We read it as “it changes, that”, and it means that in time moment \(t\) and \(t+1\) the formula has a different value (value changes from true to false or vice versa). Without going into further details – that makes it possible to generate a whole family of events, that we can call a history graph, and it would simply reflect all of the possible story paths¹.

Time for the example

Let’s see how temporal logic can help us solve the so called “FWSC” problem. This is a puzzle, where we have a farmer, a sheep, a wolf and a cabbage. We need to take all of them to the other side of the river, using a boat that has only two seats (yep, it’s a really big cabbage…) and has to be steered by the farmer. If he leaves the cabbage and the sheep together on the riverside, the sheep will eat the vegetable. Obviously, we cannot leave alone the sheep and the wolf. We can write down there rules using temporal logic. Let’s start by defining our entities as first letters of the characters in the story \((F, W, S, C)\). We can also specify the state \(B\) – for the being being in a boat ((☞ﾟ∀ﾟ)☞) and the direction – \(R\) for going to the right. Note, that now we can specify all of the four states that the being can be in – for example, \(\neg B_W \land \neg R_W \) implies that wolf is not in a boat, but is on the left side of the river.

Then we can define all of the puzzle rules using logic operators, for example: \[ (C(B_X) \rightarrow ((R_X \leftrightarrow R_F) \land (B_X \leftrightarrow B_F) \land C(B_F))) \] would mean that whenever the being changes its place or direction, the farmer does so too.

Connecting all such rules with conjunctions we get one big formula to rule them all. Using this formula we can create the history graph and simply find the path between the starting state (all beings on the right side of the river) and the ending state (all beings on the left side of the river)².

What I wanna do with all of that

My tool would allow a game designer to define temporal rules without even knowing that there is some math behind it all. I believe that modelling game object relations would simplify creation of the in-game world and analyzing the history graph could help in catching all of the inconsistencies.

That’s it for now, if you would like to read something more about it, let me know in the comments. Otherwise, I won’t post any more math posts, I promise. :)

BONUS for databases freaks

There is something called a temporal database. From what I’ve read, such databases require its tables to contain two date time columns – one for the submission date and one for the date when the entity was valid. It means that we can take the screenshots of the world state using that additional time information. These databases often also offer some special query types for querying time periods and some correlations.

TL;DR

Temporal logic is the logic that has some special operators that allow to express time-variant rules (rules that change its value over time) without needing to analyze an infinite number of time moments. I want to use it for modelling interactions between objects in the in-game world.

Annotations

comments powered by Disqus