Title: Monitoring For Safe-HML with recursion

Abstract:  
In earlier work by Fredlund, the modal mu-calculus was used as a vehicle to specify the behaviour of Erlang processes, and a corresponding tool called McErlang was constructed to model check the satisfiability of Erlang programs with respect to mu-calculus formula.  Although remarkable, the inherent concurrent nature of erlang programs severly affect the scalability of the tool. 

In this work, we study the systhesis of monitors from (a subset of) mu-calculus formulas so as to check satisfiability of erlang programs at runtime, thus side-stepping state explosion issues associated with model checking systems with multiple  execution paths. We draw inspirations from testability results on this subset of the calculus, carried out by Aceto and Ingolfsdottir, but explain in what ways our work differs from theirs.  We also discuss how compositional properties of the LTS semantics of our language can be used to minimise the amount of monitoring that we need to carry out.