STV Demo Documentation
User interface #
1
2
3
4
5
6
7
8
9
The STV Demo interface consists of two main panels - the sidebar 1 and the graph container 3. The sidebar contains three tabs that can be used to generate a model, verify it and view node details. Mode selector 2 can be used to switch between verification, partial order reduction and bisimulation. After selecting the desired mode and specifying model parameters, a graph can be generated. Then it becomes possible to verify the model.
Graph display options can be changed in area 4. Graph can be zoomed in, zoomed out and zoomed to fit the viewport in area 5. Zooming in and out is also possible by using mouse wheel. Graph viewport can be resized using handle 6, whereas handle 7 can be used to resize panels in the sidebar. Nodes 9 can be dragged around. When clicked, node details can be viewed in the sidebar details tab. Starting nodes are marked with blue color as shown in 8.
When model is sourced from a file in verification and partial reduction modes, the main panel 3 contains tabs with the main model and agent models.
Partial order reduction #
1
2
3
4
Partial order reduction can be performed by selecting a model file using input 1. Then global and reduced models can be generated using buttons 2 and 3. Once model is generated, tabs containing graphs of the model and agents appear in 4.
1
2
3
4
5
6
When global and reduced models are generated, verification can be performed in sidebar tab 1. The global model can be verified using various algorithms: lower approximation 2, upper approximation 3 and Domino DFS 5. Heuristic for Domino DFS can be chosen using 4. Analogous verification interface is available for the reduced model as shown in 6.
Bisimulation #
1
2
3
4
5
6
Left and right model graphs can be generated by selecting files containing models 1 and 2 and pressing the "Generate" button 3. Bisimulation can be performed by selecting the mapping file 4 and pressing the "Check" button 5. The coalition is shown in area 6.
1
2
3
4
5
6
7
When both models are generated, verification can be performed in sidebar tab 1. The formula for verification is shown in 2. The left model can be verified using various algorithms: lower approximation 3, upper approximation 4 and Domino DFS 6. Heuristic for Domino DFS can be chosen using 5. Analogous verification interface is available for the right model as shown in 7.
Verification #
1
Verification can be performed by selecting the desired model using 1. The model can be read from a file or it can be generated from a parameterized model template. These templates are described in the Parameterized models section.
1
2
3
4
5
6
When model is generated, verification can be performed in sidebar tab 1. The formula for verification is shown in 2. The left model can be verified using various algorithms: lower approximation 3, upper approximation 4 and Domino DFS 6. Heuristic for Domino DFS can be chosen using 5.
Parameterized models #
Verification can be performed using a model file or one of available parameterized models:
Tian Ji #
N
This model verifies existence of a winning strategy in the ancient story of Tian Ji. Tian Ji races N horses against King's N horses in N rounds. Each horse is raced exactly one time. Horses are characterized by their speed. In each round the person with the faster horse wins. In case of a draw, the King wins the round. The goal is to ensure that Tian Ji has a winning strategy.
This model has one paramter N - the number of horses.
More information about this model is available here: A. Lomuscio, H. Qu, and F. Raimondi. 2015. MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems. International Journal on Software Tools for Technology ransfer (2015). https://doi.org/10.1007/s10009-015-0378-x
Castles #
C1
C2
C3
HP
The model verifies existence of a winning strategy in the Castles problem. There are three castles with C1, C2 and C3 workers respectively. Each castle has HP health points. In each round workers can execute one of three actions: attack another castle, defend their castle or do nothing. Doing nothing is the only available action to a worker of a defeated castle. No agent can defend it's castle twice in a row. A castle gets damaged if the number of attackers is greater than the number of defenders. The damage is equal to the difference between the number of attackers nad defenders. A castle is defeated once it reaches 0 HP. Every worker knows actions they can perform in each round and they know which castles have been defeated.
This model has four parameters: C1, C2, C3 - the number of workers in each castle and HP - the number of health points that each castle starts with. The STV demo checks whether there is a strategy to defeat the third castle.
More information about this model is available here: J. Pilecki, M.A. Bednarczyk, and W. Jamroga. 2017. SMC: Synthesis of Uniform Strategies and Verification of Strategic Ability for Multi-Agent Systems. Journal of Logic and Computation 27, 7 (2017), 1871–1895. https://doi.org/10.1093/logcom/exw032
Bridge Endplay #
D
C
The model verifies of existence of a winning strategy in the Bridge Endplay problem. The goal is to find a winning strategy for the declarer.
This model has two parameters: D - the number of cards per player and C - the number of cards in hand.
More information about this model is available here: W. Jamroga, M. Knapik, and D. Kurpiewski. 2017. Fixpoint Approximation of Strategic Abilities under Imperfect Information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS). IFAAMAS, 1241–1249.
Drones #
N
E
The model verifies existence of a winning strategy in the Drones problem. There is a map that is represented by a graph. There are N drones in the starting node of the graph (location). Each drone starts with E energy points. In each round each drone can perform one of five actions: go North, go South, go East, go West or wait. Every move consumes one energy point. When drone has no energy left it can only wait. Each drone knows it's current location, current reading from it's sensor, readings from adjacent drones, readings from all ground sensors, battery charge level and set of visited locations. The goal is to check existence ofa strategy that guarantees that at least two locations have been visited.
This model has two parameters: N - the number of drones and E - the number of energy points each drone starts with.
More information about this model is available here: W. Jamroga, B. Konikowska, W. Penczek, and D. Kurpiewski. 2019. Multi-Valued Verification of Strategic Ability. (2019)
Simple Voting #
V
C
There are V voters, 1 coercer and C candidates. Voters can wait or cast a vote. After voting, they can give the coercer a proof of how they voted or refuse to do that. Then the coercer can either punish or decide not to punish the voter. The STV Demo checks existence of a strategy for voter 1 to cast a vote on candidate other than candidate 1 and avoid punishment.
The model has two parameters: V - the number of voters and C - the number of candidates.
More information about this model is available here: W. Jamroga, M. Knapik, and D. Kurpiewski. 2017. Fixpoint Approximation of Strategic Abilities under Imperfect Information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS). IFAAMAS, 1241–1249.
Model file #
Model files contain agent definitions and property definitions. Empty lines and Lines starting with % (comments) are be ignored.
COALITION property definition
This definition starts with uppercase property name (COALITION), followed by a colon :, followed by an Array of agent identifiers.
Array of agent identifiers:
Starts with [, followed by comma-separated agent identifiers, followed by ]. Example: [Voter1, Voter2].
PERSISTENT, REDUCTION and GOAL property definitions
These definitions start with uppercase property name (PERSISTENT, REDUCTION, GOAL), followed by a colon :, followed by an Array of variable identifiers.
Array of variable identifiers:
Starts with [, followed by comma-separated variable identifiers, followed by ]. Example: [win1, win2].
FORMULA property definition
This definition starts with uppercase property name (FORMULA), followed by a colon :, followed by a formula. Example: FORMULA: <<Controller1>>F(Train1_in=True | Train2_in=True).
SHOW_EPISTEMIC property definition
This definition starts with uppercase property name (SHOW_EPISTEMIC), followed by a colon :, followed by true or false. Example: SHOW_EPISTEMIC: true.
Agent definition
Agent definition consists of a set of non-empty lines.
First line:
The first line should specify agent name and the number of agents of this type in following format: Agent AgentName[count]: for example Agent Voter[3]:. In this example agents with names Voter1, Voter2 and Voter3 will be created.
Second line:
The second line should specify the initial state in following format: init: stateName for example init: wait.
Next lines:
Next lines should contain transition definitions in following format: name: state1 -> state2. Optionally, the transition can be prefixed with shared keyword. It's also possible to set vars by appending variable setters to the line: [var1=true,var2=false,var3=123,...]. Variables can be integers, true or false. To set a condition for the transition, replace -> with -[varName==varValue]> or -[varName!=varValue]>.
To create dynamic var/state/transition names, use string aID. It will be replaced with the name of the agent.
Model file example:
Agent Voter[1]:
init: start
vote1: start -> voted1
vote2: start -> voted2
shared flip1: voted1 -> fin2
shared pass1: voted1 -> fin1
shared flip2: voted2 -> fin1
shared pass2: voted2 -> fin2
shared pub: fin1 -> pub [win1=true]
shared pub: fin2 -> pub [win2=true]
shared loop: pub -> pub
Agent Official[1]:
init: start
shared flip1: start -> pub
shared pass1: start -> pub
shared flip2: start -> pub
shared pass2: start -> pub
np: pub -> pub
shared pub: pub -> fin
shared loop: fin -> fin
REDUCTION: []
COALITION: [Official1]
PERSISTENT: [win1, win2]
FORMULA: <<Official1>>F(win1=true)
Mapping file #
Mapping files are used when checking bisimulation. Every line should contain either a mapping or a coalition definition.
Mapping definition
Mapping consists of comma-separated state identifiers from the first model, followed by ->, followed by comma-separated state identifiers from the second model. In the following example mappings are specified in lines 1-6.
Coalition definition
Coalition definition starts with coalition: followed by comma-separated agent identifiers. There should be only one coalition definition per file. In the following example a coalition definition is in line 7.
Mapping file example:
0 -> 0
1, 2 -> 1
3 -> 3
4 -> 2
5 -> 5
6 -> 4
coalition:1
Example specifications #