Please use this identifier to cite or link to this item:
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.
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.