Mechanising a Modal Logic for Value-Passing Agents in HOL
Monica Nesi · Electronic Notes in Theoretical Computer Science · 1997
An extension of Hennessy-Milner logic to value-passing CCS is embedded in the HOL system. The resulting proof environment allows one to formally verify modal properties of communicating agents, which are defined over an infinite value domain.