| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
SMCDEL.Symbolic.S5
Description
In this module we define a symbolic represenation of Kripke models, called knoweldge structures.
To represent Boolean functions we use the CacBDD library via the Haskell bindings HasCacBDD.
An alternative to this module here is S5_CUDD which uses CUDD instead of CacBDD.
Synopsis
- boolBddOf :: Form -> Bdd
- boolEvalViaBdd :: [Prp] -> Form -> Bool
- bddEval :: [Prp] -> Bdd -> Bool
- size :: Bdd -> Int
- relabelWith :: [(Prp, Prp)] -> Bdd -> Bdd
- data KnowStruct = KnS [Prp] Bdd [(Agent, [Prp])]
- type State = [Prp]
- type KnowScene = (KnowStruct, State)
- type MultipointedKnowScene = (KnowStruct, Bdd)
- statesOf :: KnowStruct -> [State]
- numberOfStates :: KnowStruct -> Int
- eval :: KnowScene -> Form -> Bool
- shareknow :: KnowStruct -> [[Prp]] -> [(State, State)]
- comknow :: KnowStruct -> [Agent] -> [(State, State)]
- announce :: KnowStruct -> [Agent] -> Form -> KnowStruct
- announceOnScn :: KnowScene -> [Agent] -> Form -> KnowScene
- bddOf :: KnowStruct -> Form -> Bdd
- evalViaBdd :: KnowScene -> Form -> Bool
- validViaBdd :: KnowStruct -> Form -> Bool
- whereViaBdd :: KnowStruct -> Form -> [State]
- determinedVocabOf :: KnowStruct -> [Prp]
- nonobsVocabOf :: KnowStruct -> [Prp]
- equivExtraVocabOf :: [Prp] -> KnowStruct -> [(Prp, Prp)]
- replaceWithIn :: (Prp, Prp) -> KnowStruct -> KnowStruct
- replaceEquivExtra :: [Prp] -> KnowStruct -> (KnowStruct, [(Prp, Prp)])
- withoutProps :: [Prp] -> KnowStruct -> KnowStruct
- generatedSubstructure :: MultipointedKnowScene -> MultipointedKnowScene
- type Propulation = Tagged Quadrupel Bdd
- ($$) :: Monad m => ([a] -> b) -> [m a] -> m b
- checkPropu :: Propulation -> KnowStruct -> KnowStruct -> [Prp] -> Bool
- data KnowTransformer = KnTrf [Prp] Form [(Prp, Bdd)] [(Agent, [Prp])]
- noChange :: ([Prp] -> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer) -> [Prp] -> Form -> [(Agent, [Prp])] -> KnowTransformer
- type Event = (KnowTransformer, State)
- type MultipointedEvent = (KnowTransformer, Bdd)
- publicAnnounce :: [Agent] -> Form -> Event
- shiftPrepare :: KnowStruct -> KnowTransformer -> (KnowTransformer, [(Prp, Prp)])
- texBddWith :: (Int -> String) -> Bdd -> String
- texBDD :: Bdd -> String
- newtype WrapBdd = Wrap Bdd
- reduce :: Event -> Form -> Maybe Form
Boolean Reasoning
boolBddOf :: Form -> Bdd Source #
Translate a Boolean formula to a BDD. The function will raise an error if it is given an epistemic or dynamic formula.
boolEvalViaBdd :: [Prp] -> Form -> Bool Source #
Given a set of true atomic propositions, evaluate a Boolean formula.
relabelWith :: [(Prp, Prp)] -> Bdd -> Bdd Source #
Given a mapping between atomic propositions, relabel them inside a BDD.
Knowledge Structures
data KnowStruct Source #
Knowledge structures are a compact representation of S5 Kripke models. Their set of states is defined by a Boolean formula. Instead of accessibility relations we use observational variables. Formal proofs that knowledge structures are indeed equivalent to S5 Kripke models can be found in the references from the Readme.
A knowledge structure is a tuple \(\mathcal{F} = (V,\theta,O_1,\dots,O_n)\) where \(V\) is the vocabulary, a finite set of propositional variables, \(\theta\) is the state law, a Boolean formula over $V$ (represented as its BDD) and for each agent \(i\), we have observational variables \(O_i \subseteq V\).
Instances
A state of \(\mathcal{F}\) is a list of true atomic propositions. It should satisfy \(\theta\).
type KnowScene = (KnowStruct, State) Source #
A pair $(mathcal{F},s)$ where $s$ is a state of $mathcal{F}$, is a scene.
type MultipointedKnowScene = (KnowStruct, Bdd) Source #
statesOf :: KnowStruct -> [State] Source #
Given a knowledge structure, generate the finite list of its states.
numberOfStates :: KnowStruct -> Int Source #
Semantics
Semantics on KnowScenes are defined inductively as follows.
- \( (\mathcal{F},s)\vDash p\) iff \(s \vDash p\)
- \( (\mathcal{F},s)\vDash \neg \varphi\) iff not \((\mathcal{F},s)\vDash \varphi\)
- \( (\mathcal{F},s)\vDash \varphi \land \psi\) iff \((\mathcal{F},s)\vDash \varphi\) and \((\mathcal{F},s)\vDash \psi\)
- \( (\mathcal{F},s)\vDash { K}_i \varphi\) iff for all \(t\) of \(\mathcal{F}\), if \(s\cap O_i=t\cap O_i\), then \((\mathcal{F},t)\vDash \varphi\)
- \((\mathcal{F},s)\vDash {C}_\Delta \varphi\) iff for all \(t\) of \(\mathcal{F}\), if \((s,t)\in {\cal E}_\Delta^\ast\), then \(({\cal F},t)\vDash \varphi\)
- \((\mathcal{F},s)\vDash [\psi] \varphi\) iff \((\mathcal{F},s)\vDash \psi\) implies \((\mathcal{F}^\psi, s) \vDash \varphi\)
where
\(\| \psi \|_\mathcal{F}\) is given by
bddOfand \[\mathcal{F}^\psi:=(V,\theta \land \| \psi \|_\mathcal{F}, O_1, \dots, O_n)\] - \((\mathcal{F},s)\vDash [\psi]_\Delta \varphi\) iff \((\mathcal{F},s)\vDash \psi\) implies \((\mathcal{F}^\Delta_\psi, s\cup \{ p_\psi \} ) \vDash \varphi\) where \(p_\psi\) is a new propositional variable, \(\| \psi \|_\mathcal{F}\) is a boolean formula given by Definition~ref{def-boolEquiv} and \[\mathcal{F}^\Delta_\psi:= (V\cup \{ p_\psi \},\theta \land (p_\psi \leftrightarrow \| \psi \|_\mathcal{F}), O^\ast_1, \dots, O^\ast_n) \] where (O^ast_i := left{ begin{array}{ll} O_i cup { p_psi } & text{if } i in Delta \ O_i & text{otherwise} end{array} right. )
If we have \(({\cal F},s) \vDash \phi\) for all states \(s\) of \(\cal F\), then we say that \(\phi\) is valid on \(\cal F\) and write \(\cal F \vDash \phi\).
eval :: KnowScene -> Form -> Bool Source #
The function eval implements the semantics.
An important warning: This function is not a symbolic algorithm!
It is a direct translation of the Definition above.
In particular it calls statesOf which means that the set of stats is explicitly generated.
The symbolic (and much faster) counterpart of eval is evalViaBdd below.
Common Knowledge
To interpret common knowledge we use the following definitions. Given a knowledge structure \((V,\theta,O_1,\dots,O_n)\) and a set of agents \(\Delta\), let \(\mathcal{E}_\Delta\) be the relation on states of \(\mathcal{F}\) defined by \((s,t) \in {\cal E}_\Delta\) iff there exists an \(i\in {\Delta}\) with \(s \cap O_i = t \cap O_i\). and let \({\cal E}_{\cal V}^\ast\) to denote the transitive closure of \({\cal E}_{\cal V}\).
In our data type for knowledge structures we represent the state law \(\theta\) not as a formula but as a Binary Decision Diagram.
Announcements
We also have to define how knowledge structures are changed by public and group announcements. The following functions correspond to the last two points of the semantics Definition above.
announce :: KnowStruct -> [Agent] -> Form -> KnowStruct Source #
Symbolic Evaluation
validViaBdd :: KnowStruct -> Form -> Bool Source #
whereViaBdd :: KnowStruct -> Form -> [State] Source #
Minimization and Optimization
determinedVocabOf :: KnowStruct -> [Prp] Source #
Knowledge structures can contain unnecessary vocabulary, i.e. atomic propositions that are determined by the state law and not used as observational propositions.
nonobsVocabOf :: KnowStruct -> [Prp] Source #
equivExtraVocabOf :: [Prp] -> KnowStruct -> [(Prp, Prp)] Source #
replaceWithIn :: (Prp, Prp) -> KnowStruct -> KnowStruct Source #
replaceEquivExtra :: [Prp] -> KnowStruct -> (KnowStruct, [(Prp, Prp)]) Source #
withoutProps :: [Prp] -> KnowStruct -> KnowStruct Source #
Remove determined and unused atomic propositions from a structure to make the state law smaller.
Symbolic Bisimulations f
type Propulation = Tagged Quadrupel Bdd Source #
See Section 2.11 from https://malv.in/phdthesis for details.
To distinguish explicit and symbolic bisimulations in the implementation we call symbolic bisimulations propulations.
checkPropu :: Propulation -> KnowStruct -> KnowStruct -> [Prp] -> Bool Source #
Knowledge Transformers
data KnowTransformer Source #
Instances
noChange :: ([Prp] -> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer) -> [Prp] -> Form -> [(Agent, [Prp])] -> KnowTransformer Source #
type Event = (KnowTransformer, State) Source #
type MultipointedEvent = (KnowTransformer, Bdd) Source #
publicAnnounce :: [Agent] -> Form -> Event Source #
A public announcement, the easiest example of a knowledge transformer.
shiftPrepare :: KnowStruct -> KnowTransformer -> (KnowTransformer, [(Prp, Prp)]) Source #
shift addprops to ensure that props and newprops are disjoint:
LaTeX functions
Reduction axioms for knowledge transformers
reduce :: Event -> Form -> Maybe Form Source #
Adding knowledge transformers does not increase expressivity because we have the following reductions.
For now we do not implement a separate type of formulas with dynamic operators but instead implement the reduction axioms directly as a function which takes an event and ``pushes it through'' a formula.
The following takes an event $mathcal{X},x$ and a formula $phi$ and then
`pushes' $[mathcal{X},x]$ through all boolean and epistemic operators in
$phi$ until it disappears in front of atomic propositons.
This translation is global, i.e. if there is a reduced formula, then it is
equivalent to the original on all structures.