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
Ingolfsdottir, 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 SizeFormat 
rv15rechml.pdf428.87 kBAdobe PDFView/Open


Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.