Runtime verification : lecture notes in computer science

We study μHML (a branching-time logic with least and greatest fixpoints) from a runtime verification perspective. We establish which subset of the logic can be verified at runtime and define correct monitor-synthesis algorithms for this subset. We also prove completeness results wrt. these logical subsets that show that no other properties apart from those identified can be verified at runtime.peer-reviewe