Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/86107
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Aceto, Luca | - |
dc.contributor.author | Achilleos, Antonis | - |
dc.contributor.author | Francalanza, Adrian | - |
dc.contributor.author | Ingólfsdóttir, Anna | - |
dc.contributor.author | Lehtinen, Karoliina | - |
dc.date.accessioned | 2021-12-28T06:17:27Z | - |
dc.date.available | 2021-12-28T06:17:27Z | - |
dc.date.issued | 2019-01 | - |
dc.identifier.citation | Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., & Lehtinen, K. (2019). Adventures in monitorability : from branching to linear time and back again. Proceedings of the ACM on Programming Languages, 3(POPL), 1-29. | en_GB |
dc.identifier.uri | https://www.um.edu.mt/library/oar/handle/123456789/86107 | - |
dc.description.abstract | This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal µ-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties. | en_GB |
dc.language.iso | en | en_GB |
dc.publisher | Association for Computing Machinery | en_GB |
dc.rights | info:eu-repo/semantics/openAccess | en_GB |
dc.subject | Computer logic | en_GB |
dc.subject | Computer software -- Verification | en_GB |
dc.subject | Object monitors (Computer software) | en_GB |
dc.subject | Recursive functions -- Data processing | en_GB |
dc.title | Adventures in monitorability : from branching to linear time and back again | en_GB |
dc.type | article | en_GB |
dc.rights.holder | The copyright of this work belongs to the author(s)/publisher. The rights of this work are as defined by the appropriate Copyright Legislation or as modified by any successive legislation. Users may access this work and can make use of the information contained in accordance with the Copyright Legislation provided that the author must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the prior permission of the copyright holder. | en_GB |
dc.description.reviewed | peer-reviewed | en_GB |
dc.identifier.doi | 10.1145/3290365 | - |
dc.publication.title | Proceedings of the ACM on Programming Languages | en_GB |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Adventures in Monitorability.pdf | 503.22 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.