JSON ATL Formula for CGS checker

To run the CGS checker, a pair consisting of both LCGS (used to describe a CGS) and an ATL formula has to be supplied. This page describes writing the ATL formula. The ATL formula is supplied as a JSON file.

Essentially, the ATL formula consists of three parts;

1. Path quantifiers and temporal operators
2. Players
3. The formula

Path quantifiers and temporal operators

To denote whether we want to ask if the formula holds true for either "despite" what the players does, or we'll have the players to be able to "enforce" the formula to hold true, we simply just write despite or enforce before the temporal operator.

The following temporal operators are supported eventually", "next", "invariant" and "until".

Where combining the path quantifiers and temporal operators it would look like this "despite until" or "enforce until".

Players

Is provided as a JSON list, containing only integer. The players are provided as the index number of their declaration, so, no matter what the players is called in the LCGS, if we want to write a formula that checks if Player 1 is able to enforce a formula, he is denoted as 0 in the ATL formula.

{"enforce eventually":
  {"players": [0]}
}

It is possible to provide as many players in the formula as there is players in the LCGS.

The formula

The formula is the meat of the ATL formula, here we denote what labels, or propositions that we want to check is fulfilled. This is also denoted as a JSON object called "formula", it consists of one of the following Supported JSON objects;

Supported JSON objects

true

Always holds true

false

always holds false

and

is a JSON list consisting of exactly two elements, of the supported JSON objects. These will be and'ed

or

is a JSON list consisting of exactly two elements, of the supported JSON objects. These will be or'ed

not

takes a supported JSON object, this will be not'ed.

proposition

takes an int, the int represents a label declared in the LCGS, where, like the player, it is dependent on the indexed declaration.

Usage

Lets first define a LCGS to write our formulae for

const max_health = 1;

player billy = cowboy [target1=clayton, target2=jesse];
player clayton = cowboy [target1=jesse, target2=billy];
player jesse = cowboy [target1=billy, target2=clayton];

label is_a_fair_game = true;

template cowboy

    health : [0 .. max_health] init max_health;
    health' = max(health - target1.shoot_left - target2.shoot_right, 0);

    label alive = health > 0;

    [wait] true;
    [shoot_right] health > 0 & target1.health > 0;
    [shoot_left] health > 0 & target2.health > 0;

endtemplate

Here we can start by extracting the player numbers, billy is player 0, clayton is player 1, jesse is player 2

is_a_fair_game is proposition 0, as it is declared in global space. billy.alive is proposition 1, as he is the first player to have been declared, and there is a label called alive, that is inside the player template. clayton.alive is proposition 2 jesse.alive is proposition 3

now to write a formula for asking if despite what billy and clayton is doing, they cannot prevent billy to die.

or [[billy, clayton]] <> !alive(billy)

{"despite eventually": {
    "players": [0,1],
    "formula": {"not": {"proposition": 0}}
  }
}

It should be noted however that if the temporal operators until is used, then the formula is divided into two sub-forms, called "pre" and "until".

{"enforce until": {
  "players": [0],
  "pre": {
    "proposition": 0
  },
  "until": {
     "not": {
       "proposition": 1
     }
  }
}

~ Billy really was the sheriff of the town.