Davide Grossi edited untitled.tex  about 8 years ago

Commit id: bc23b66893bb6fd1994d706874da08cc2b3fbf11

deletions | additions      

       

\box{p} \phi \limp \dia{p} \phi & & \mbox{(seriality)} \\  \dia{p} \phi \limp \box{p} \phi & & \mbox{(functionality)}  \end{align}  More precisely, for any influence graph $G = \tuple{\N, R}$, formula $\lbox $\box{p}  \phi \limp \dia{p} \phi$ (respectively, $\dia{p} \phi \limp \box{p} \phi$) is valid in such graph---that is, true in any pointed influence model built on such graph---if and only if $R$ is serial (respectively, functional).\footnote{These are known results from modal correspondence theory (cf. \cite{Blackburn_2001}).} \subsection{Expressing Convergence} 

Let the influence $\Model = \tuple{\N, \G, \Val}$ be given. Each $G_p$ in $\G$ converges if and only if:  \begin{align}  \true{\mu x.p \vee [ p] \box{p}  x }_\Model = \N \end{align}  \paragraph{Structural equivalence of BDPs}