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.
CITATION STYLE
Francalanza, A., Aceto, L., & Ingolfsdottir, A. (2015). On verifying hennessy-milner logic with recursion at runtime. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9333, pp. 71–86). Springer Verlag. https://doi.org/10.1007/978-3-319-23820-3_5
Mendeley helps you to discover research relevant for your work.