This is a follow-up to my previous post Finding Cheryl’s Birthday with DEMO in which I solved the famous puzzle about Cheryl’s Birthday using DEMO, an explicit model checker for Dynamic Epistemic Logic (DEL).
Since this commit the famous puzzle is also one of the examples included in SMCDEL, a symbolic model checker for DEL. Here I will explain the basics usage of SMCDEL and highlight the differences between explicit and symbolic model checking.
Like DEMO, also SMCDEL is meant to be used as a Haskell module. There is also a command-line and a web interface which are easier to use, but as of now they provide less functionality. It would be a hassle to encode Cheryl’s Birthday in the format needed by those interfaces, so here we will use Haskell directly.
We start by importing a Haskell library for lists and two modules from SMCDEL: the language and the symbolic methods for S5. The latter choice makes sense because the puzzle is only about knowledge, not belief.
module SMCDEL.Examples.Cheryl where import Data.List import SMCDEL.Language import SMCDEL.Symbolic.S5
Before doing anything with SMCDEL we define the set of all possibilities, i.e. all birthdays. This is exactly the same as in the DEMO version, but for readability we also introduce a type alias.
type Possibility = (Int, String) possibilities :: [Possibility] = possibilities 15,"May"), (16,"May"), (19,"May") [ (17,"June"), (18,"June") , (14,"July"), (16,"July") , (14,"August"), (15,"August"), (17,"August") ] , (
Recall that DEMO offers many different atomic propositions like
R Int and
Info a propositions are a very convenient and powerful tool.
Unfortunately, such nominal propositions are not available in SMCDEL.
The language in SMCDEL provides only one set of atomic propositions given by
This restriction is due to the encoding with
Binary Decision Diagrams.
Still, also without
Info a propositions we can make our life easy:
we define abbreviations in Haskell so that we can write formulas more easily.
For example, we fix that
P 17 means “The day of Cheryl’s birthday is 17.”
P 8 means “The month of Cheryl’s birthday is August.”
dayIs :: Int -> Prp = P dayIs monthIs :: String -> Prp "May" = P 5 monthIs "June" = P 6 monthIs "July" = P 7 monthIs "August" = P 8 monthIs = undefinedmonthIs _
We then combine our atomic propositions to form more complex formulas.
For example, the command
thisPos (15,"August") will give us the conjunction
Conj [PrpF (P 15), PrpF (P 8)] saying that Cheryl’s birthday is the 15th of August.
The second formula
knWhich i says that agent i knows Cheryl’s birthday.
This the same as
knowsBday in the
DEMO version and also here we define it as a big disjunction.
This is not optimal, but given the small model size in this puzzle, it does not hurt.
thisPos :: Possibility -> Form = Conj $ thisPos (d,m) PrpF (dayIs d) : [ Neg (PrpF $ dayIs d') | d' <- nub (map fst possibilities) \\ [d] ]) ++ (PrpF (monthIs m) : [ Neg (PrpF $ monthIs m') | m' <- nub (map snd possibilities) \\ [m] ]) ( knWhich :: Agent -> Form = Disj [ K i (thisPos pos) | pos <- possibilities ]knWhich i
Now, instead of an initial Kripke model, for SMCDEL we need a knowledge structure modelling the start of the puzzle. A knowledge structure is the symbolic analogue of a Kripke model. Recall that a Kripke model contains a set of worlds w1, w2, etc. and valuations like p1 : true, p2 : false, etc. for each world. Instead of listing all this information explicitly, a knowledge structure contains a summary of the whole set of worlds.
The main trick of symbolic model checking is to replace the explicit list of worlds with a boolean formula and then say: My worlds are all boolean assignments satisfying this formula.
Well, and there are some more ingredients. First, there are many tricks to find and modify this boolean formula. Second, instead of a formula we only need the boolean function it represents and this can be represented as a Binary Decision Diagram.
A knowledge structure now consists of three parts:
- a list of propositions called the vocabulary:
- the aforementioned boolean formula:
- for each agent a list which propositions that agent observes:
Let us compare this again to a Kripke model. The vocabulary and state law together replace the set of worlds and the valuation function. The observational variables replace the accessibility relation.
(Maybe you are now wondering whether a knowledge structure is just a different way to write down a Kripke model. The answer is yes. Think of knowledge structures as a data structure to store Kripke models.)
Enough theory, here is the initial knowledge structure for Cheryl’s Birthday puzzle:
start :: KnowStruct = KnS allprops statelaw obs where start = sort $ nub $ map (dayIs . fst) possibilities ++ allprops map (monthIs . snd) possibilities = boolBddOf $ Conj statelaw Disj (map thisPos possibilities) [ Conj [ Neg $ Conj [thisPos p1, thisPos p2] , | p1 <- possibilities, p2 <- possibilities, p1 /= p2 ] ] = [ ("Albert" , nub $ map (monthIs . snd) possibilities) obs "Bernard", nub $ map (dayIs . fst) possibilities) ] , (
It is easy to check that
allprobs is the list
map P [5,6,7,8,14,15,16,17,18,19].
statelaw essentially says “The birthday must be one of the
possibilities, but it cannot be two different ones at the same time.”
To encode the knowledge of the agents, we let Albert observe all atomic propositions about the day and Bernard those about the month.
An equivalent and sometimes more intuitive way to read observational variables is this: an agent observes a variable iff the agent knows whether that variable is true.
Now we will update the
model structure with public announcements, given by the dialogue in the puzzle.
The announced formulas are exactly the same as in the DEMO implementation, with small syntax adaptations.
Instead of the
upd_pa function in DEMO we now use the
update function in SMCDEL.
update is polymorphic such that it also accepts action models or transformers, but here it is given a formula and will thus execute a public announcement.
First Albert says: “I don’t know when Cheryl’s birthday is and I know that Bernard does not know.” To model this we update with the following conjunction:
= update start (Conj [ Neg $ knWhich "Albert" round1 K "Albert" $ Neg (knWhich "Bernard")]) ,
Then Bernard says: “Now I know when Cheryl’s birthday is.”
= update round1 (knWhich "Bernard")round2
Finally, Albert says: “Now I also know when Cheryl’s birthday is.”
= update round2 (knWhich "Albert")round3
We can now get the solution by asking for the remaining states:
$ stack ghci src/SMCDEL/Examples/Cheryl.hs λ> statesOf round3 [[P 7,P 16]]
To get the solution in a more readable form, we can write a little helper function:
cherylsBirthday :: String = m ++ " " ++ show d ++ "th" where cherylsBirthday = filter [(d,m)] -> [monthIs m', dayIs d'] `elem` statesOf round3) (\(d',m') possibilities
λ> cherylsBirthday "July 16th"
If you want to learn more about the internals of SMCDEL, please have a look at the source code and documentation or my PhD thesis. The first chapter also describes the basics of Dynamic Epistemic Logic.