This report documents the addition of new features to CAAL. Previous work on CAAL resulted in a web application used for teaching students about reactive systems. The tool supports description of processes in the process algebra Calculus of Communicating Systems. It is possible to verify the presence or absence of various preorders and equivalence between processes, and the tool offers to play against the user in bisimulation games to prove to the user the validity of a result. The tool also supports model checking of recursive Hennessy-Milner formulae. All computations are done by reducing problems to dependency graphs, and interpreting the computed fixed-point assignments, which are computed by an "on-the-fly" algorithm.

We extend CAAL with full syntax and semantics of HML formulae and offer reductions from HML formulae to dependency graphs. To complement the bisimulation games, we define the HML game and show that satisfiability is related to which player has a universal winning strategy. We also show that universal winning strategy corresponds to fixed-point assignments on the dependency graphs, and in doing so also shows the relationship between satisfiability and fixed-point assignments.

As an alternative to playing bisimulation games, we show it is possible to compute a distinguishing formula for two non-bisimilar processes. Finding the simplest possible distinguishing formula turns out difficult and we conjecture the decidability problem of whether a simple formula exists is NP-hard. Instead we present a greedy algorithm simplifies some formulae.

In CAAL it is possible to view a visual representation of processes. Processes can become quite complex and difficult to understand. Equivalence collapses may simplify the state system and allow the user to focus on particular aspects of a process. We present the theory and an algorithm to collapse processes based on merging equivalent processes into equivalence classes.

As an experiment we attempted to reuse the code in CAAL for a parallel algorithm. We document our design, pseudocode, and test result. The results were unsatisfactorily, but we identify possible reasons for this.