On Verifying Hennessy-Milner Logic with Recursion at Runtime

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.

• Type: Journal
• Year: 2015
• Where: RV
• Authors: Adrian Francalanza, Luca Aceto, Anna Ingólfsdóttir
• Keywords: Hardware, RV 2015