CCS+HML model checker

By applying informed search methods such as A* on the state space generated by a CCS expression and the operational semantics of CCS, one can build a rudimentary reachability checker. This project consists of writing such a checker in Haskell. This involves parsing CCS and HML expressions, animating the semantics of CCS and searching a process tree for a process that satisfies a given HML formula.

Here is a PDF describing the implementation and here is the source on GitHub.