A Synthesis Tool for Optimal Monitors in a Branching-Time Setting

Antonis Achilleos; Léo Exibard; Adrian Francalanza; Karoliina Lehtinen; Jasmine Xuereb

doi:10.1007/978-3-031-08143-9_11

A Synthesis Tool for Optimal Monitors in a Branching-Time Setting

Antonis Achilleos, Léo Exibard, Adrian Francalanza, Karoliina Lehtinen, Jasmine Xuereb^*

^*Corresponding author for this work

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set of monitorable properties to a small logical fragment. A recent study has enlarged the set of monitorable branching-time properties by weakening the requirements expected of the monitors effecting the verification: it defines a novel notion of optimal monitor that carries out the maximum number of detections that can be effected for any property, thereby turning a branching-time property into a monitorable one. The study also outlines a method for obtaining a unique optimal monitor from any branching-time property but falls short of providing an automation for this procedure. In this paper, we present a prototype tool that generates monitorable properties for branching-time properties expressed in a variant of the modal μ -calculus, based on this procedure. We also assess the performance of the prototype tool by evaluating its performance against several specifications.

Original language	English
Title of host publication	Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings
Editors	Maurice H. ter Beek, Marjan Sirjani
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	181-199
Number of pages	19
ISBN (Print)	9783031081453
DOIs	https://doi.org/10.1007/978-3-031-08143-9_11
Publication status	Published - 2022
Event	24th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022 - Lucca, Italy Duration: 13 Jun 2022 → 17 Jun 2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13271 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022
Country/Territory	Italy
City	Lucca
Period	13/06/22 → 17/06/22

Bibliographical note

Funding Information:
This research was supported by the project‘Mode(l)s of Verification and Monitorability (MoVeMnt)’ (no. 217987-051) of the Icelandic Research Fund.

Publisher Copyright:
© 2022, IFIP International Federation for Information Processing.

Other keywords

Branching-time specifications
Monitor Synthesis
Runtime Verification

Access to Document

10.1007/978-3-031-08143-9_11

Cite this

Achilleos, A., Exibard, L., Francalanza, A., Lehtinen, K., & Xuereb, J. (2022). A Synthesis Tool for Optimal Monitors in a Branching-Time Setting. In M. H. ter Beek, & M. Sirjani (Eds.), Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings (pp. 181-199). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13271 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-08143-9_11

Achilleos, Antonis ; Exibard, Léo ; Francalanza, Adrian et al. / A Synthesis Tool for Optimal Monitors in a Branching-Time Setting. Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings. editor / Maurice H. ter Beek ; Marjan Sirjani. Springer Science and Business Media Deutschland GmbH, 2022. pp. 181-199 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{eac89f05133c4e9983bb6d66f7e27d72,

title = "A Synthesis Tool for Optimal Monitors in a Branching-Time Setting",

abstract = "Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set of monitorable properties to a small logical fragment. A recent study has enlarged the set of monitorable branching-time properties by weakening the requirements expected of the monitors effecting the verification: it defines a novel notion of optimal monitor that carries out the maximum number of detections that can be effected for any property, thereby turning a branching-time property into a monitorable one. The study also outlines a method for obtaining a unique optimal monitor from any branching-time property but falls short of providing an automation for this procedure. In this paper, we present a prototype tool that generates monitorable properties for branching-time properties expressed in a variant of the modal μ -calculus, based on this procedure. We also assess the performance of the prototype tool by evaluating its performance against several specifications.",

keywords = "Branching-time specifications, Monitor Synthesis, Runtime Verification",

author = "Antonis Achilleos and L{\'e}o Exibard and Adrian Francalanza and Karoliina Lehtinen and Jasmine Xuereb",

note = "Funding Information: This research was supported by the project{\textquoteleft}Mode(l)s of Verification and Monitorability (MoVeMnt){\textquoteright} (no. 217987-051) of the Icelandic Research Fund. Publisher Copyright: {\textcopyright} 2022, IFIP International Federation for Information Processing.; 24th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022 ; Conference date: 13-06-2022 Through 17-06-2022",

year = "2022",

doi = "10.1007/978-3-031-08143-9_11",

language = "English",

isbn = "9783031081453",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "181--199",

editor = "{ter Beek}, {Maurice H.} and Marjan Sirjani",

booktitle = "Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings",

address = "Germany",

}

Achilleos, A, Exibard, L, Francalanza, A, Lehtinen, K & Xuereb, J 2022, A Synthesis Tool for Optimal Monitors in a Branching-Time Setting. in MH ter Beek & M Sirjani (eds), Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13271 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 181-199, 24th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, 13/06/22. https://doi.org/10.1007/978-3-031-08143-9_11

A Synthesis Tool for Optimal Monitors in a Branching-Time Setting. / Achilleos, Antonis; Exibard, Léo; Francalanza, Adrian et al.
Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings. ed. / Maurice H. ter Beek; Marjan Sirjani. Springer Science and Business Media Deutschland GmbH, 2022. p. 181-199 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13271 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A Synthesis Tool for Optimal Monitors in a Branching-Time Setting

AU - Achilleos, Antonis

AU - Exibard, Léo

AU - Francalanza, Adrian

AU - Lehtinen, Karoliina

AU - Xuereb, Jasmine

N1 - Funding Information: This research was supported by the project‘Mode(l)s of Verification and Monitorability (MoVeMnt)’ (no. 217987-051) of the Icelandic Research Fund. Publisher Copyright: © 2022, IFIP International Federation for Information Processing.

PY - 2022

Y1 - 2022

N2 - Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set of monitorable properties to a small logical fragment. A recent study has enlarged the set of monitorable branching-time properties by weakening the requirements expected of the monitors effecting the verification: it defines a novel notion of optimal monitor that carries out the maximum number of detections that can be effected for any property, thereby turning a branching-time property into a monitorable one. The study also outlines a method for obtaining a unique optimal monitor from any branching-time property but falls short of providing an automation for this procedure. In this paper, we present a prototype tool that generates monitorable properties for branching-time properties expressed in a variant of the modal μ -calculus, based on this procedure. We also assess the performance of the prototype tool by evaluating its performance against several specifications.

AB - Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set of monitorable properties to a small logical fragment. A recent study has enlarged the set of monitorable branching-time properties by weakening the requirements expected of the monitors effecting the verification: it defines a novel notion of optimal monitor that carries out the maximum number of detections that can be effected for any property, thereby turning a branching-time property into a monitorable one. The study also outlines a method for obtaining a unique optimal monitor from any branching-time property but falls short of providing an automation for this procedure. In this paper, we present a prototype tool that generates monitorable properties for branching-time properties expressed in a variant of the modal μ -calculus, based on this procedure. We also assess the performance of the prototype tool by evaluating its performance against several specifications.

KW - Branching-time specifications

KW - Monitor Synthesis

KW - Runtime Verification

UR - http://www.scopus.com/inward/record.url?scp=85132985586&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-08143-9_11

DO - 10.1007/978-3-031-08143-9_11

M3 - Conference contribution

AN - SCOPUS:85132985586

SN - 9783031081453

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 181

EP - 199

BT - Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings

A2 - ter Beek, Maurice H.

A2 - Sirjani, Marjan

PB - Springer Science and Business Media Deutschland GmbH

T2 - 24th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022

Y2 - 13 June 2022 through 17 June 2022

ER -

Achilleos A, Exibard L, Francalanza A, Lehtinen K, Xuereb J. A Synthesis Tool for Optimal Monitors in a Branching-Time Setting. In ter Beek MH, Sirjani M, editors, Coordination Models and Languages - 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Proceedings. Springer Science and Business Media Deutschland GmbH. 2022. p. 181-199. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-08143-9_11