Model

Formal Model of the Game

The formal model of the game is defined as follows:

• The set of agents A, where A = {A1, A2, A3, A4, A5}
• The set of roles R, where R = {LO, Vet, Doc, GF, May}
• The set of nights N, where N = {1, 2, .., 30}
• The Kripke structure 𝕄 for the game Town of Salem. 𝕄 is a tuple ⟨S, π, R₁, R₂, R₃, R₄, R₅⟩ where:
• S is a non-empty set of worlds.s
• π is the truth assignment to the propositional atoms per state; π: S → (P → {T,F}).
• R₁, R₂, R₃, R₄, and R₅ are the accessibility relations for every agent a ∈ A

Knowledge

Agents can obtain 4 different facts about agents and their actions. The first type of fact is about the role of an agent. The second and third type of fact are about the behaviour of the agents and the fourth type of fact is about an agent being killed. Each fact will be discussed in more detail below.

1. The first type of fact is about the role an agent has. It is represented in the following way: Ax_role, e.g. A1_LOO means that agent A1 has the 'lookout' role.


2. The second type of fact is about an agent visiting another agent. Only the lookout, the godfather and the doctor can visit other agents at night. Facts about agents visiting visiting other agents are represented in the following way: AxV Ay_Nn where x ≠ y, e.g. A1V A3_N1 means that agent A1 visited A3 during night 1.


3. The third type of fact is about the doctor healing someone. When the doctor heals an agent that was attacked, they receive a message stating that their target was attacked but that they saved them. The fact is represented in the following way: AxH Ay_Nn where x ≠ y and Ax_Doc. For example, A1H A3_N2 means that agent A1 (who is the doctor) healed agent A3 on night 2.


4. The last fact is about an agent dying during the night. The fact is represented in the following way: xD_Nn_role where x ≠ y, e.g. 2D_N3_GFR means that agent A2 was killed by the godfather during night 3. Because only the godfather and the veteran can kill, role can only be GFR or Vet.

Axioms

The axioms are the main way that the agents can infer and obtain knowledge. The axioms correspond to certain situations in the game where the agents can infer which roles other agents can or cannot have. There are 3 general axioms that every agent can use, 4 axioms that only the lookout can use and 1 axiom that only the doctor can use.

General Axioms

1. The first axiom states that if I know some agent has some role, different agents cannot have that same role. Formally:
   For all s ∈ S and Kripke structure 𝕄, for some x,y ∈ A, all z ∈ A and some role r ∈ R with z ≠ y; (𝕄 ,s) ⊨ K_xAy_r → K_x¬Az_r.


2. A. Axiom 2A states that if I know 4 different agents do not have a certain role, by process of elimination, the fifth (and last) agent has that role. Formally:
   For all s ∈ S and Kripke structure 𝕄, for some x, y ∈ A, all z ∈ A with z ≠ y and some role r ∈ R: (𝕄, s) ⊨ K_x¬Az_r → K_xAy_r.


2. B. Axiom 2B states that if I know some agent does not have 4 of the roles, by process of elimination, it must have the last remaining role. Formally:
   For some s ∈ S and Kripke structure 𝕄, for some x ∈ A, for some r ∈ R and all l ∈ R with r ≠ l : (𝕄, s) ⊨ K_x¬As_l → K_xAs_r.

3. Axiom 3, only used by the lookout, states that if some agent is visited by two other agents, all the agents that did not visit are not the godfather or the doctor, since those are the only roles that can visit other agents. Formally:
   For all s ∈ S and Kripke structure 𝕄, for u, v, w, x, y ∈ A with u ≠ v ≠ w ≠ x ≠ y and some n ∈ N: (𝕄, s) ⊨ K_u (Au_LOO ∧ AvV Ax_Nn ∧ AwV Ax_Nn) → K_u (¬Ax_GFR ∧ ¬Ax_Doc ∧ ¬ AyGFR ∧ ¬Ay_Doc ).


4. Axiom 4, only used by the lookout, states that if some agent was visited by another agent, the visiting agent is not the veteran or the mayor. Formally:
   For all s ∈ S and Kripke structure 𝕄, for some u, x, y ∈ A with u ≠ x ≠ y and some n ∈ N : (𝕄, s) ⊨ K_u (Au_LOO ∧ AxV Ay_Nn) → Ku(¬Ax_Vet ∧ ¬Ax_May).


5. Axiom 5, only used by the lookout, states that if some agent was visited by only 1 other agent, and the visited agent was killed by the godfather in the same night, the visiting agent is the godfather. Formally:
   For all s ∈ S and Kripke structure 𝕄, for some u, v, x ∈ A and all w ∈ A where v ≠ x ≠ w and some n ∈ N: (𝕄, s) ⊨ K_u (Au_LOO ∧ AvV Ax_Nn ∧ ¬AwV Ax_Nn ∧ xD_Nn_GFR) → Av_GFR.


6. Axiom 6, only used by the lookout, if some agent (agent 1) was visited by some other agent (agent 2), and still some other agent (agent 3) was killed by the godfather in the same night, then the last remaining agent apart from the lookout (which is the current reasoning agent) is the godfather. Formally:
   For all s ∈ S and Kripke structure 𝕄, for some u, w, x, y, z ∈ A with u ≠ w ≠ x ≠ y ≠ z and some n ∈ N : (𝕄, s) ⊨ K_u (Au_LOO ∧ AxV Ay_Nn ∧ zD_Nn_GFR) → K_u(Aw_GFR ∧ Ay_Doc).

7. Axiom 7, only used by the doctor, states that if the veteran has died before the current night, and the doctor healed (successfully saved) its target, the doctor can infer that its target is not the godfather. Formally:
   For all s ∈ S and kripke structure 𝕄, for some x, y, z ∈ A where x ≠ y ≠ z, and for some n, m ∈ N where m<n : (𝕄, s) ⊨ K_x(Ax_Doc ∧ AxH Ay_Nn ∧ zD_Nm_GFR ∧ Az_Vet) → K_x¬Ax_GFR