-
Notifications
You must be signed in to change notification settings - Fork 1
Language for Concurrent Game Structures (LCGS)
Input to CGAAL is a pair consisting of a CGS (concurrent game structure) and a property written as ATL (alternating-time temporal logic). This page describes a language called LCGS which can be used to define a CGS for the checker. In LCGS a CGS is defined with a series of declarations such that it is possible to find the successors of any state from the declarations alone. The language allows us to save memory at the small cost of having to evaluate the expressions whenever successors are explored. The syntax of the language is inspired by PRISM-lang used by the PRISM-games model checker to model stochastic multi-player games with rewards. However, LCGS differs in multiple ways. For instance, LCGS has player templates instead of modules, and templates have no effect unless there exists an instance of it. Additionally, synchronizations affecting a player's internal state is much easier to declare.
Concurrent game structures (CGS) are state machines, where the transitions depend on the combination of choices made by independent players. Additionally, labels are given to some of the states. It is these labels, that we can use in our query.
Below is a Mexican standoff between three cowboys modeled using LCGS. Each of them can choose to wait, or shoot the cowboy to their right or to their left. If a cowboy is shot twice, he dies.
const max_health = 2;
player billy = cowboy [opp_right=clayton, opp_left=jesse];
player clayton = cowboy [opp_right=jesse, opp_left=billy];
player jesse = cowboy [opp_right=billy, opp_left=clayton];
template cowboy
health : [0 .. max_health] init max_health;
health' = max(health - opp_right.shoot_left - opp_left.shoot_right, 0);
label alive = health > 0;
[wait] true;
[shoot_right] health > 0 & opp_right.health > 0;
[shoot_left] health > 0 & opp_left.health > 0;
endtemplate
LCGS only has one type: Integer. All expressions evaluate to an integer. However, boolean operators are also present in the language. In a boolean expression, the value 0 acts as false, while every other value is true. The value of a boolean operator is also either 0 or 1.
Operators:
- Addition:
+ - Subtraction:
- - Multiplication:
* - Division (floored):
/ - Unary negation (negative):
- - Unary negation (not):
! - Equality:
= - Inequality:
!= - Greater than:
> - Less than:
< - Greather than or equal:
>= - Less than or equal:
<= - Logical and:
&& - Logical or:
|| - Logical xor:
^ - Implication:
->
Identifiers refer to (or is) the name of a declaration. Identifiers must start with a letter, but can otherwise contains letters, numbers, and underscore.
In expressions identifiers can have two parts seperated by a period ., e.g. controller.working. In this case the first part is the owner of the declaration. So for this example, we are refering to the working declaration of the player called controller. If the owner is not given, it is infered. If you are in a template, LCGS will look for a declaration with the given name in that template. If that does not exist, it will assume you are referring to a global declaration.
In short LCGS has 6 different kinds of declarations:
- Constants - Values that never changes.
- Variables - Values that changes and are part of the overall structure's state. A variable declaration also describes how the value updates during a transition based on the previous state and the actions of the players.
- Templates - A template for a player. Essentially a code block of actions, variables, and labels.
- Players - A player that can take actions. Players are constructed from a template but can optionally rename parts of the template. This makes it easy to create players with similar behaviour. All players must have at least one action, but can also have variables and labels.
- Actions - These define what players can do and when.
- Labels - These are propositions that can be referenced in ATL formulas.
Each declaration defines a part of the CGS.
A constant is simply what the name suggests: A constant value, that will not change.
const MAX_ROUNDS = 4;
If constants refer to other constants, the other constant must be declared above it.
// const baz = foo + bar // Not okay since foo and bar appears below it
const foo = 2;
const bar = foo * 3
Do not be afraid to use constants. All expressions are evaluted as much that as possible before the state exploration starts. This means that even a complex expressions like x > y ? x * y / z + 20 : max(y, z) is reduced to a single number as long as both x, y, and z are constants.
In LCGS a CGS state consists of the values of state variables. State variables are declared in a variable declaration.
power : [0..100] init 100;
power' = max(0, power - 1);
Variable declaration consists of two statements, which much follow each other (no declarations in between). The first statement declares the name, the range, and the initial value. The second statement declares how the variable is updated during transitions.
Variables must have a range as LCGS uses this to compress states to a single value. However, LCGS does not prevent you from using a CGS where the update expression can go out of range. You will instead get a runtime error, when it happens. LCGS can only handle up to 2^32 different states. So the product of all the sizes of the ranges of all variables, cannot exceed 2^32.
The upper bound, lower bound, and initial value must be constant expressions. That is, an expression that be evaluated at load-time. Both upper and lower bound is inclusive.
The update statement (the second half of the declaration) define how the state variable updates during transitions. The left-hand side of the = must be the variables name (again yes) followed by a '. The right-hand side is an expression for the new value. In this expression you can refer to constants, state variables, and even player actions. When referring to a state variable, its value is the variable's value in the previous state. You can also use the name of the declaration, that you are declaring to use the variables previous value. In the example below, flipflop to go back and forth between 0 and 1 regardless of which actions are taken.
flipflop : [0..1] init 1;
flipflop' = !flipflop;
Below is a very similar behaviour, but flip and flop are now two different variables, where the update expressions refer to the other.
flip : [0..1] init 1;
flip' = flop;
flop : [0..1] init 0;
flop' = flip;
In many cases, you want the variable to update based on players' actions. When referring to a player's action in an update expression, the action will have a value of 1 (true) if the player took that action or a value of 0 (false) if the player took another action.
// When Bob goes to work he earns 100 bucks
money : [0..1000] init 200;
money' = max(0, min(1000, money + bob.work * 100 - RENT));
A template declaration is essentially a block of code that models a process, and a player declaration is an instance of the process. Using relabeling, templates allow us to create similar process without having to write duplicate code. In the snippet below two players are defined both using the robot template.
player robotA = robot;
player robotB = robot;
label touching = robotA.x == robotB.x && robotA.y == robotB.y;
template robot
x : [0..10] init 5;
x' = x + moveRight - moveLeft;
y : [0..10] init 5;
y' = y + moveUp - moveDown;
[moveUp] y < 10;
[moveDown] y > 0;
[moveLeft] x > 0;
[moveRight] x < 10;
endtemplate
Each robot has a unqiue (x, y) position and is able to move up, down, left, and right.
The most important part of templates are actions. In concurrent game structures, the combination of all players' actions dictates the transitions. The actions available to a player is defined in their template using action declarations. All players must always have one action available to them.
As seen above, templates can contain other declarations. They can contain actions, state variables, and labels.
For each instance (player) of the template a unique instance of the action, state variable, or label is created.
These can be referred to using the player's names and dot notation.
As seen in the snippet above, the label touching is present, when robotA.x == robotB.x and robotA.y == robotB.y.
Inside a template the player can be omitted when refering to a declaration owned by the same instance.
For instance, in the declaration of the action moveUp above, we do not specify the player of y.
However, declarations inside a template can refer to a specific player.
This can be desired when one player's action affects the updating of state variables of other players.
Relabeling allows you to modify parts of a template for a player. This allows you to create more generic templates.
player alice = human [INCOME=150, RENT=70, relax=draw];
player bob = human [INCOME=150, RENT=60, relax=playGames];
template human
money : [0..1000] init 200;
money' = max(0, min(1000, money + work * INCOME - RENT));
[work] 1;
[relax] 1;
endtemplate
In the snippet above, two humans are defined: alice and bob.
However, using relabeling, the [...] in the player declaration, we have created to different humans.
Alice earns 150 whenever she works, her rent is 70, and she likes to draw to relax.
Bob also earns 150 whenever he works, but his rent is 60, and he relaxes by playing games.
Relabeling allows you to change any identifier to a different identifier or a constant expression.
The target identifier is given on the left of =, and the new expression is given on the right.
It is also possible to relabel first or second half of a dot notation.
For instance, relabeling bob.money with [money=euro] becomes bob.euro.
There are a few obvious constraints to relabeling. For instance, the name of a declaration nor parts of a dot notation can be relabeled to an expression. It must be a new identifier:
// Illegal. An action cannot be called "0"
player charlie = human [INCOME=150, RENT=70, relax=0];
// Illegal. A declaration cannot be called "week.1 + 2"
player david = human [INCOME=150, RENT=70, day=1 + 2];
template human
money : [0..1000] init 200;
money' = max(0, min(1000, money + work * INCOME - RENT));
[work] week.day != SUNDAY;
[relax] 1;
endtemplate
Transitions between states in the CGS are defined by actions taken by players, and all players must take exactly one available action. The actions taken and the previous state is then used to find the new state as discussed in the section on variables. The actions that are taken will have a value of 1, and other actions have a value of 0.
All action declarations must appear in templates. They consist of a name in square brackets and a condition describing whether the action is available. Players must always have at least one action available, otherwise a run-time error occurs.
player robotA = robot;
player robotB = robot;
template robot
x : [0..10] init 5;
x' = x + moveRight - moveLeft;
y : [0..10] init 5;
y' = y + moveUp - moveDown;
[moveUp] y < 10;
[moveDown] y > 0;
[moveLeft] x > 0;
[moveRight] x < 10;
endtemplate
In the example above, the robots can move up, down, left, and right, but not if it would them outside a 10x10 grid.
Labels are named expressions which can be queried in the ATL properties. They simply consists of the label keyword, a name, and an expression.
label touching = robotA.x == robotB.x && robotA.y == robotB.y;
The following property asserts that there exists a strategy, such that robotA and robotN is always touching.
<<robotA, robotB>> G touching