ISPL Language Reference

ISPL is a programming language used to describe multi-agent systems for verification with MCMAS. An ISPL program models a system of agents that can interact, communicate, and evolve over time.

Program Structure

An ISPL program consists of several main sections:

1. Semantics (optional)
2. Environment Agent (optional)
3. Standard Agents (one or more)
4. Evaluation
5. InitStates
6. Groups (optional)
7. Fairness (optional)
8. Formulae

Semantics

Overview: Defines how variable assignments are handled during evolution.

The semantics section appears at the beginning of the file and specifies how the evolution functions should be interpreted:

Semantics = MultiAssignment | SingleAssignment

• MultiAssignment (MA): Evolution items are mutually exclusive - only one item executes per step, updating its variables while keeping others unchanged
• SingleAssignment (SA): Evolution items are partitioned by variable - items updating the same variable are mutually exclusive, but items updating different variables can execute simultaneously

If omitted, MultiAssignment is used by default.

Environment Agent

Overview: Models the shared infrastructure and boundary conditions that all standard agents can observe.

The Environment is a special agent that represents the system's external conditions, communication channels, or shared resources. Unlike standard agents, the Environment can have observable variables that other agents can read (but not modify).

Agent Environment
  Obsvars:
    // Observable variables - can be seen by other agents
  end Obsvars
  
  Vars:
    // Private variables - only the Environment can access
  end Vars
  
  RedStates:
    // Definition of "bad" states for correctness properties
  end RedStates
  
  Actions = {...};
  
  Protocol:
    // Rules for when actions can be performed
  end Protocol
  
  Evolution:
    // How variables change based on actions
  end Evolution
end Agent

Key Features:

• Can have both observable and private variables
• Observable variables can be referenced by other agents as Environment.variableName
• Represents non-deterministic external conditions
• Optional - not all models require an environment

Standard Agents

Overview: Represents individual entities in the multi-agent system with private state and behavior.

Standard agents are the main actors in the system. Each agent has private local state, can perform actions, and evolves according to protocols and evolution functions.

Agent AgentName
  Lobsvars = {...};  // Local observable variables from Environment
  
  Vars:
    // Private local variables
  end Vars
  
  RedStates:
    // Definition of incorrect/bad states
  end RedStates
  
  Actions = {...};
  
  Protocol:
    // Action selection rules
  end Protocol
  
  Evolution:
    // State transition rules
  end Evolution
end Agent

Key Features:

• Have private local state (variables)
• Can observe specific Environment variables (Lobsvars)
• Cannot directly access other agents' private variables
• Can reference other agents' actions in evolution functions

Variable Types

Overview: ISPL supports three types of variables for modeling agent state.

Boolean Variables

variableName : boolean;

• Values: true or false
• Supports bit operations: ~ (not), & (and), | (or), ^ (xor)
• Comparisons: =, !=

Enumeration Variables

variableName : {value1, value2, value3};

• Values: Any of the specified enumeration constants
• Comparisons: =, !=
• Two enumeration types are comparable if one is a subset of the other

Bounded Integer Variables

variableName : lowerBound .. upperBound;

• Values: Integers within the specified range
• Supports arithmetic operations: +, -, *, /
• Comparisons: =, !=, <, <=, >, >=

Actions

Overview: Defines the set of actions an agent can perform, which are visible to all other agents.

Actions = {action1, action2, action3};

Key Features:

• Actions are "public" - all agents can observe what actions others perform
• Used in protocols to determine when actions can be taken
• Used in evolution functions to trigger state changes
• Referenced in other agents' conditions as AgentName.Action = actionName

Protocol

Overview: Defines the rules for when an agent can perform specific actions based on its current state.

Protocol:
  condition1 : {action1, action2};
  condition2 : {action3};
  Other : {defaultAction};
end Protocol

Key Features:

• Maps boolean conditions over local state to sets of enabled actions
• Conditions can overlap (enabling non-deterministic choice)
• Other keyword handles all states not covered by explicit conditions
• Conditions can reference local variables and Environment observable variables
• Non-deterministic when multiple actions are enabled

Example:

Protocol:
  state=ready and Environment.channel=open : {send, wait};
  state=busy : {process};
  Other : {idle};
end Protocol

Evolution

Overview: Defines how an agent's local variables change in response to the actions performed by all agents.

MultiAssignment Semantics

Evolution:
  var1=newValue1 and var2=newValue2 if condition1;
  var3=newValue3 if condition2;
end Evolution

SingleAssignment Semantics

Evolution:
  var1=newValue1 if condition1;
  var2=newValue2 if condition2;
end Evolution

Key Features:

• Conditions can reference local variables, Environment observables, and all agents' actions
• Actions referenced as AgentName.Action = actionName
• Right-hand side can be expressions involving variables and constants
• If no condition matches, variables retain their current values
• In MultiAssignment: evolution rules are mutually exclusive
• In SingleAssignment: rules for different variables can execute simultaneously

Red States

Overview: Defines "incorrect" or "bad" states for an agent, used in correctness verification.

RedStates:
  booleanCondition;
end RedStates

Key Features:

• Boolean formula over local variables and Environment observables
• States satisfying the condition are "red" (incorrect)
• All other states are "green" (correct)
• Used with deontic operator O (ought) in formulae
• Can be omitted if all states are considered correct

Evaluation

Overview: Defines atomic propositions (boolean predicates) over global system state for use in verification formulae.

Evaluation
  propositionName if booleanCondition;
  anotherProp if Agent1.var1 = value and Agent2.var2 > threshold;
end Evaluation

Key Features:

• Creates named boolean propositions for use in formulae
• Conditions can reference any agent's variables using AgentName.variableName syntax
• Environment variables referenced as Environment.variableName
• Used to make formulae more readable and reusable

InitStates

Overview: Specifies the initial global states of the system when verification begins.

InitStates
  Agent1.var1 = value1 and Agent2.var2 = value2 and Environment.var3 = value3;
end InitStates

Key Features:

• Boolean formula over all agents' variables
• Can specify exact values or relationships between variables
• Multiple initial states possible if formula is satisfied by multiple variable assignments
• Can use equality between variables: Agent1.var = Agent2.var
• Must specify initial values for all relevant variables

Groups

Overview: Defines collections of agents for use in group-based verification formulae.

Groups
  groupName = {Agent1, Agent2, Environment};
  anotherGroup = {Agent3, Agent4};
end Groups

Key Features:

• Used with group epistemic operators: GK (group knowledge), GCK (common knowledge), DK (distributed knowledge)
• Used with ATL strategy operators: <groupName>X, <groupName>F, etc.
• Can include the Environment agent
• Groups can overlap or be disjoint

Fairness

Overview: Specifies conditions that must hold infinitely often along all execution paths, used to rule out unrealistic behaviors.

Fairness
  proposition1;
  proposition2 -> proposition3;
  AG someCondition;
end Fairness

Key Features:

• List of formulae that must be true infinitely often
• Can use atomic propositions defined in Evaluation section
• Can use boolean combinations and temporal operators
• Prevents models where certain conditions are avoided forever
• Example: ensuring a communication channel works infinitely often

Formulae

Overview: Contains the properties to be verified against the model, written in temporal and epistemic logic.

Formulae
  AG(proposition1 -> AF proposition2);
  K(Agent1, proposition3);
  <group1>F proposition4;
end Formulae

Supported Logics:

• CTL: AG, EG, AX, EX, AF, EF, AU, EU
• LTL: G, F, X, U (with LTL prefix)
• CTL*: Combined state and path formulae (with CTL* prefix)
• Epistemic: K(agent, φ) (knowledge), GK(group, φ) (group knowledge), GCK(group, φ) (common knowledge), DK(group, φ) (distributed knowledge)
• ATL: <group>X φ, <group>F φ, <group>G φ, <group>(φ U ψ) (strategic operators)
• Deontic: O(agent, φ) (correctness - agent ought to satisfy φ)

Key Features:

• Each formula is checked and results are reported as TRUE or FALSE
• Can generate counterexamples for false universal formulae
• Can generate witnesses for true existential formulae
• Supports boolean combinations of formulae
• Built-in propositions: AgentName.GreenStates, AgentName.RedStates