| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
SMCDEL.Symbolic.K
Description
The implementation in SMCDEL.Symbolic.S5 only works for models where the
epistemic accessibility relation is an equivalence relation.
This is because only those can be described by sets of observational variables.
In fact, not even every S5 relation on distinctly valuated worlds can be modeled with observational variables --- this is why our translation procedure S5 has to add additional atomic propositions.
To overcome this limitation, here we generalize the definition of knowledge structures. Using well-known methods from temporal model checking, arbitrary relations can also be represented as BDDs. See for example~cite{GoroRyan02:BelRevBDD}. Remember that in a knowledge structure we can identify states with boolean assignments and those are just sets of propositions. Hence a relation on states with unique valuations can be seen as a relation between sets of propositions. We can therefore represent it with the BDD of a characteristic function on a double vocabulary, as described in~cite[Section 5.2]{ClarkeGrumbergPeled1999:MC}. Intuitively, we construct (the BDD of) a formula which is true exactly for the pairs of boolean assignments that are connected by the relation.
Our symbolic model checker can then also be used for non-S5 models.
For further explanations, see~cite[Section 8]{BEGS17:SMCDELbeyond}.
Synopsis
- mvP :: Prp -> Prp
- cpP :: Prp -> Prp
- unmvcpP :: Prp -> Prp
- mv :: [Prp] -> [Prp]
- cp :: [Prp] -> [Prp]
- unmv :: [Prp] -> [Prp]
- uncp :: [Prp] -> [Prp]
- data Dubbel
- type RelBDD = Tagged Dubbel Bdd
- totalRelBdd :: RelBDD
- emptyRelBdd :: RelBDD
- allsamebdd :: [Prp] -> RelBDD
- class TagBdd a where
- tagBddEval :: [Prp] -> Tagged a Bdd -> Bool
- cpBdd :: Bdd -> RelBDD
- mvBdd :: Bdd -> RelBDD
- unmvBdd :: RelBDD -> Bdd
- propRel2bdd :: [Prp] -> Map State [State] -> RelBDD
- samplerel :: Map State [State]
- relBddOfIn :: Agent -> KripkeModel -> RelBDD
- data BelStruct = BlS [Prp] Bdd (Map Agent RelBDD)
- type BelScene = (BelStruct, State)
- type MultipointedBelScene = (BelStruct, Bdd)
- bddOf :: BelStruct -> Form -> Bdd
- validViaBdd :: BelStruct -> Form -> Bool
- evalViaBdd :: BelScene -> Form -> Bool
- announce :: BelStruct -> [Agent] -> Form -> BelStruct
- statesOf :: BelStruct -> [State]
- texRelBDD :: RelBDD -> String
- bddprefix :: String
- bddsuffix :: String
- cleanupObsLaw :: BelScene -> BelScene
- determinedVocabOf :: BelStruct -> [Prp]
- nonobsVocabOf :: BelStruct -> [Prp]
- withoutProps :: [Prp] -> BelStruct -> BelStruct
- equivExtraVocabOf :: [Prp] -> BelStruct -> [(Prp, Prp)]
- replaceWithIn :: (Prp, Prp) -> BelStruct -> BelStruct
- replaceEquivExtra :: [Prp] -> BelStruct -> (BelStruct, [(Prp, Prp)])
- data Transformer = Trf [Prp] Form (Map Prp Bdd) (Map Agent RelBDD)
- noChange :: ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer) -> [Prp] -> Form -> Map Agent RelBDD -> Transformer
- type Event = (Transformer, State)
- type MultipointedEvent = (Transformer, Bdd)
- shiftPrepare :: BelStruct -> Transformer -> (Transformer, [(Prp, Prp)])
- trfPost :: Event -> Prp -> Bdd
- reduce :: Event -> Form -> Maybe Form
- bddReduce :: BelScene -> Event -> Form -> Bdd
- evalViaBddReduce :: BelScene -> Event -> Form -> Bool
Translating relations to type-safe BDDs
totalRelBdd :: RelBDD Source #
emptyRelBdd :: RelBDD Source #
allsamebdd :: [Prp] -> RelBDD Source #
Minimal complete definition
Nothing
Describing Kripke Models with BDDs
We now want to use BDDs to represent the relations of multiple agents in a general Kripke Model. Suppose we have a model for the vocabulary $V$ in which the valuation function assigns to every state a distinct set of true propositions. To simplify the notation we also write $s$ for the set of propositions true at $s$.
relBddOfIn :: Agent -> KripkeModel -> RelBDD Source #
Translate an agent's relation of worlds to a relation of sets of propositions. The given model must have distinct valuations.
Belief Structures
Instances
type MultipointedBelScene = (BelStruct, Bdd) Source #
bddOf :: BelStruct -> Form -> Bdd Source #
Given a formula, compute a BDD that is equivalent to that formula, on a given belief structure.
Visualizing Belief Structures
cleanupObsLaw :: BelScene -> BelScene Source #
determinedVocabOf :: BelStruct -> [Prp] Source #
nonobsVocabOf :: BelStruct -> [Prp] Source #
data Transformer Source #
Instances
noChange :: ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer) -> [Prp] -> Form -> Map Agent RelBDD -> Transformer Source #
type Event = (Transformer, State) Source #
type MultipointedEvent = (Transformer, Bdd) Source #
shiftPrepare :: BelStruct -> Transformer -> (Transformer, [(Prp, Prp)]) Source #
shift addprops to ensure that props and newprops are disjoint: