Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/23273| Title: | On verifying Hennessy-Milner logic with recursion at runtime |
| Other Titles: | Runtime verification : lecture notes in computer science |
| Authors: | Francalanza, Adrian Aceto, Luca Ingólfsdóttir, Anna |
| Keywords: | Aspect-oriented programming Computer software -- Development Real-time data processing Computer security Computer programs -- Verification Discrete-time systems Calculus -- Computer programs Computer programs -- Correctness |
| Issue Date: | 2015 |
| Publisher: | Springer, Cham |
| Citation: | Francalanza A., Aceto L., & Ingolfsdottir A. (2015). On verifying Hennessy-Milner logic with recursion at runtime. In E. Bartocci, R. Majumdar (Eds.), Runtime Verification. Lecture Notes in Computer Science (pp.1-15). Cham: Springer. |
| Abstract: | 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. |
| URI: | https://www.um.edu.mt/library/oar//handle/123456789/23273 |
| Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| rv15rechml.pdf | 428.87 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.