Formal verification and analysis has made few inroads into knowledge
sharing because, at the level of shared knowledge, the computation used
to perform sharing normally is too complex, unpredictable and/or
obscure to allow practical methods to be developed. Recently,
however,
computational methods have been developed that apply directly for
knowledge sharing some of the methods that have traditionally been used
in formal verification. The area to which these methods is
applied,
however, is very different in nature to those of traditional formal
verification. This leads us to apply formal analytical methods in
novel ways. I will summarise four of these (from work done by
Paolo
Besana, Phil Graham, Dave Lambert, and Nardine Osman) within a common
framework.