It has been suggested by many people that formal notions of knowledge can usefully be applied to the design of distributed systems. My PhD project explored the possibility of algorithmically finding implementations of knowledge-based programs, which are essentially a notation for concurrent systems extended with explicit knowledge conditionals. These allow a designer to specify their distributed protocols directly in terms of what an agent (a component in the system) knows.
To make it feasible to automatically construct automata that implement these conditionals, we restrict our scope to synchronous systems, i.e., those that proceed in rounds, and moreover to those with a finite set of states. This allows us to use state-traversal techniques familiar from model checking.
The thesis (pdf, 1.5MB) contains further motivation for this formalism and what it might be good for.
The project involved developing a pair of domain-specific languages (DSLs) for describing synchronous systems that contain knowledge conditionals. Both are embedded in Haskell and are structured using Arrows.
The foundational language is called ADHOC (Arrows for Describing Higher-Order Circuits). In some ways it is similar to Mary Sheeran's pioneering μFP system, and the early monadic versions of Lava; it is purely functional in ways that more recent Lavas (Lava 2000, Kansas Lava, etc.) tend not to be. (York Lava is another pure Lava that adopts a distinct approach to the sharing issue.)
ADHOC's chief novelties are the use of Arrows, which allows for the capture of information flow between components, support for circuits with combinational cycles, and, of course, knowledge conditionals.
ADHOC underpins an implementation of Gérard Berry's circuit translation for the Esterel imperative synchronous language as an Arrow transformer. The result is Kesterel: Esterel extended with knowledge conditionals.
Several examples are included with the code, which is available from github:
git clone git://github.com/peteg/ADHOC.git
or perhaps:
git clone https://github.com/peteg/ADHOC.git
The system depends on these libraries that are available from Hackage:
See my publications page.