Usable Object Oriented Prover for S5n
OOPS
The Object Oriented Prover for S5n (OOPS) is a command line tool that can be used to model and derive knowledge of agents. To model the world that an agent inhabits, the user has to explicitly specify all knowledge in this world. For example, the next OOPS formula models a world in which three agents wear either a red or a blue hat, there are two blue hats in total and an agent has exactly one hat:
(r0 = ~b0) & (r0 | b0) & (r1 = ~b1) & (r1 | b1) & (r2 = ~b2) & (r2 | b2) & ((b0 & b1) > (~b2)) & ((b0 & b2) > (~b1)) & ((b1 & b2) > (~b0))
(where | is or, & is and, ~ is negation, > is material conditional, = is biconditional, rX means agent X has a red hat, bX means agent X has a blue hat.).
Although the explicit and precise way of defining formulas in OOPS make OOPS very generally applicable (i.e. OOPS can be used to model almost any kind of world), it is not very user-friendly. The complexity of the OOPS formulas increases dramatically when more agents and attributes are added. For example, the OOPS formula shown above is already quite complex for the simple world it models, but imagine creating this formula for five agents and three different hat colors. The goal of this project is to build a GUI that lets users create a world graphically and automatically generates OOPS formulas based on this world. In this way, the user can intuitively solve multi-agent problems, without having to specify all knowledge manually. Because of the limited time span of this project, we will base our implementation on one well-known multi-agent problem: the Queen’s Wise Men.
The Queen’s Wise Men
The Queen’s Wise Men problem (QWM, also known as the King’s Wise Men) is defined as follows: There once was a wise queen, who was a perfect logician. For advice, she relied on three wise men, who were likewise perfect logicians. This was common knowledge among the four of them, as was the fact that none of them would ever lie or cheat. One day, the queen wanted to demonstrate to her people just how wise her wise men were. She announced that she would place a hat on each of their heads, and that each of the wise men would be able to see the hats of the other two, but not his own. The queen then announced that she had three red hats and two blue hats total, and that each wise man was to determine the color of his own hat. The queen then placed the hats, and said: “Each man who knows the color of his hat, must now step forward.”
QWM in OOPS
To determine the hat color of a particular agent in OOPS, you need to take the following steps:
1. Specify all common knowledge:
(r0 = ~b0) & (r0 | b0) & (r1 = ~b1) & (r1 | b1) & (r2 = ~b2) & (r2 | b2) & ((b0 & b1) > (~b2)) & ((b0 & b2) > (~b1)) & ((b1 & b2) > (~b0))
2. Agent 0 knows all common knowledge:
#_0((r0 = ~b0) & (r0 | b0) & (r1 = ~b1) & (r1 | b1) & (r2 = ~b2) & (r2 | b2) & ((b0 & b1) > (~b2)) & ((b0 & b2) > (~b1)) & ((b1 & b2) > (~b0)))
(where #_0 means agent 0 knows).
3. Does agent 0’s knowledge imply that, given the observed color of the hats of the other agents, he knows the color of his own hat?
For red:
#_0((r0 = ~b0) & (r0 | b0) & (r1 = ~b1) & (r1 | b1) & (r2 = ~b2) & (r2 | b2) & ((b0 & b1) > (~b2)) & ((b0 & b2) > (~b1)) & ((b1 & b2) > (~b0))) > ((b1 & b2) > r0)
For blue:
#_0((r0 = ~b0) & (r0 | b0) & (r1 = ~b1) & (r1 | b1) & (r2 = ~b2) & (r2 | b2) & ((b0 & b1) > (~b2)) & ((b0 & b2) > (~b1)) & ((b1 & b2) > (~b0))) > ((b1 & b2) > b0)
Usable OOPS
Our implementation, called Usable Object Oriented Prover for S5n (UOOPS), consists of a panel containing the world (i.e. the agents and their properties) and a toolbar. A screenshot of our program is shown in Figure 1. With the buttons in the toolbar, users can add and remove agents to the world and specify the total number of hats for each color. The toolbar also contains a text area that shows the output of the problem solving process and a text area that shows the generated OOPS formulas. Underneath each agent are two buttons, the change hat button changes the hat color of the agent and the determine hat button initiates the problem solving process.
Figure 1: Screenshot of UOOPS. In this screenshot, the determine hat button of agent 0 has been clicked. When this button is clicked, a message appears in the upper text area indicating whether the agent can derive the color of his hat. The OOPS formulas used to arrive at this conclusion are shown in the bottom text area.
To solve the same problem as above in UOOPS, the user needs to take the following steps:
1. Add three agents
2. Set number of blue hats to two, set number of red hats to three.
3. Change the hats of agent 1 and 2 to blue.
4. Click on agent 0's determine hat button.
UOOPS automatically generates the correct OOPS formulas, runs them through OOPS and presents the knowledge of the agent regarding its own hat (the hat is blue, red, or unknown) to the user in the output text area.
Higher level knowledge
In the problem presented above, agent 0 can determine his hat color after the queen’s first announcement (i.e. ‘each man who knows the color of his hat, must now step forward’). However, it is also possible that an agent can not determine his hat color after one announcement, but by using knowledge about the knowledge of the other agents, can determine his hat color after multiple announcements. The following example illustrates this situation.
There are three agents in the world, agents 0 and 1 wear a red hat and agent 2 wears a blue hat. There are three red hats and two blue hats in total. After the queen’s first announcement, none of the agents knows his hat color and therefore none of the agents step forward. All agents know that the other agents do not know their hat color. When the queen makes a second announcement, an agent can use the fact that the other agents did not know their hat color after the first announcement to determine his own hat color. Agents 0 can now derive that he has a red hat, because he sees that agent 1 has a red hat, agent 2 has a blue hat and he knows that if he had a blue hat, agent 1 would have known his hat color after the first announcement (because then agent 1 would have seen that the other agents had blue hats and therefore he has a red hat). Therefore agent 0 knows that he must have a red hat. Agent 1 can determine his hat color in the same way. After two announcements, agent 2 still can not know his hat color. After three announcements, agent 2 knows that the other agents know their hat color. Therefore he knows that he must have the opposite hat color as them, because if he has the same hat color as them, they would not have known their hat color after the previous announcement. Therefore agent 2 knows he has a blue hat.
In UOOPS, users can model situations like this by using the Queen announcement button. This button determines the hat color for all agents. The button can be clicked multiple times to invoke the use of higher level knowledge (i.e. knowledge of the knowledge of other agents after the previous announcement) to determine the hat color. The Reset announcements button allows the user to start again at the first announcement. A UOOPS representation of the multiple announcement example discussed above is shown in Figure 2.
Figure 2: UOOPS screenshot where the world is defined according to the problem definition outlined above.
Discussion
UOOPS is able to parse a graphical representation of a world into OOPS formulas and thereby provides an intuitive and user-friendly way to solve the QWM problem. UOOPS allows the user to easily create and evaluate different versions of the QWM problem. The user can change the amount of agents, the hats the agents wear and the total number of red and blue hats with just a single mouse click. In standard OOPS, changing these properties would require the user to define the appropriate OOPS formula over and over again, which would be a very tedious and time-consuming process.
Because UOOPS incorporates higher level knowledge (i.e. it can evaluate situations in which multiple announcements of the queen are necessary), it can be used to study the interaction between the number of agents and hats and the number of announcements necessary before an agent can know its hat color. UOOPS forms an interesting and useful GUI for OOPS. Although it is currently limited to the QWM problem, it could be extended to include a wider range of problems. In its current form, UOOPS is very suitable for educational purposes and for evaluation of complex versions of the QWM problem.
Java Demo
UOOPS was written in Java. In runs on any system with Java (possibly, Java 1.6 is required).
To download and start UOOPS, click te button below:
If that doesn't work, try the direct link: Download
If that doesn't work, you might still try and download the source. You can build it yourself or look in the dist folder to find a executable jar.
Source Code
A zipped source package with Netbeans (ver. 7.1 required) project configuration is available here. It also includes an executable uoops.jar in the distfolder.