Axiomatizing recursion-free, regular monitors

Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al. has specified monitors using a variation on the regular fra...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logical and algebraic methods in programming 2022-06, Vol.127, p.100778, Article 100778
Main Authors: Aceto, Luca, Achilleos, Antonis, Anastasiadi, Elli, Ingolfsdottir, Anna
Format: Article
Language:English
Subjects:
Axiomatization
Equational logic
Formal verification
Monitors
Process algebra
Verdict equivalence
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c303t-97330d41db10e00eac0037a74f87a545bfa20a0b08ea006d8c2350640fb3c0823
cites cdi_FETCH-LOGICAL-c303t-97330d41db10e00eac0037a74f87a545bfa20a0b08ea006d8c2350640fb3c0823
container_end_page
container_issue
container_start_page 100778
container_title Journal of logical and algebraic methods in programming
container_volume 127
creator Aceto, Luca
Achilleos, Antonis
Anastasiadi, Elli
Ingolfsdottir, Anna
description Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al. has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and ω-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and ω-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.
doi_str_mv 10.1016/j.jlamp.2022.100778
format article
fullrecord <record><control><sourceid>elsevier_cross</sourceid><recordid>TN_cdi_crossref_primary_10_1016_j_jlamp_2022_100778</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><els_id>S2352220822000311</els_id><sourcerecordid>S2352220822000311</sourcerecordid><originalsourceid>FETCH-LOGICAL-c303t-97330d41db10e00eac0037a74f87a545bfa20a0b08ea006d8c2350640fb3c0823</originalsourceid><addsrcrecordid>eNp9j8tOwzAQRb0Aiar0C9j0A3AY20lsFiyqikelSmxgbTnOuHKUxJWdIuDrcQlrVqMZ3TO6h5AbBgUDVt91Rdeb4Vhw4DxfQEp1QRZcVJxyDuqKrFLqAHJUSSXYgtDNpw-Dmfy3Hw_riPYUkw8jdRHxNu-HU2_iegijn0JM1-TSmT7h6m8uyfvT49v2he5fn3fbzZ5aAWKi91IIaEvWNgwQAI0FENLI0ilpqrJqnOFgoAGFBqBulc0NoS7BNcKC4mJJxPzXxpBSRKeP0Q8mfmkG-iyqO_0rqs-iehbN1MNMYa724THqZD2OFlufxSbdBv8v_wOi_V4K</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>Axiomatizing recursion-free, regular monitors</title><source>ScienceDirect Freedom Collection 2022-2024</source><creator>Aceto, Luca ; Achilleos, Antonis ; Anastasiadi, Elli ; Ingolfsdottir, Anna</creator><creatorcontrib>Aceto, Luca ; Achilleos, Antonis ; Anastasiadi, Elli ; Ingolfsdottir, Anna</creatorcontrib><description>Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al. has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and ω-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and ω-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.</description><identifier>ISSN: 2352-2208</identifier><identifier>DOI: 10.1016/j.jlamp.2022.100778</identifier><language>eng</language><publisher>Elsevier Inc</publisher><subject>Axiomatization ; Equational logic ; Formal verification ; Monitors ; Process algebra ; Verdict equivalence</subject><ispartof>Journal of logical and algebraic methods in programming, 2022-06, Vol.127, p.100778, Article 100778</ispartof><rights>2022 Elsevier Inc.</rights><lds50>peer_reviewed</lds50><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c303t-97330d41db10e00eac0037a74f87a545bfa20a0b08ea006d8c2350640fb3c0823</citedby><cites>FETCH-LOGICAL-c303t-97330d41db10e00eac0037a74f87a545bfa20a0b08ea006d8c2350640fb3c0823</cites><orcidid>0000-0001-7526-9256</orcidid></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Aceto, Luca</creatorcontrib><creatorcontrib>Achilleos, Antonis</creatorcontrib><creatorcontrib>Anastasiadi, Elli</creatorcontrib><creatorcontrib>Ingolfsdottir, Anna</creatorcontrib><title>Axiomatizing recursion-free, regular monitors</title><title>Journal of logical and algebraic methods in programming</title><description>Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al. has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and ω-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and ω-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.</description><subject>Axiomatization</subject><subject>Equational logic</subject><subject>Formal verification</subject><subject>Monitors</subject><subject>Process algebra</subject><subject>Verdict equivalence</subject><issn>2352-2208</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2022</creationdate><recordtype>article</recordtype><recordid>eNp9j8tOwzAQRb0Aiar0C9j0A3AY20lsFiyqikelSmxgbTnOuHKUxJWdIuDrcQlrVqMZ3TO6h5AbBgUDVt91Rdeb4Vhw4DxfQEp1QRZcVJxyDuqKrFLqAHJUSSXYgtDNpw-Dmfy3Hw_riPYUkw8jdRHxNu-HU2_iegijn0JM1-TSmT7h6m8uyfvT49v2he5fn3fbzZ5aAWKi91IIaEvWNgwQAI0FENLI0ilpqrJqnOFgoAGFBqBulc0NoS7BNcKC4mJJxPzXxpBSRKeP0Q8mfmkG-iyqO_0rqs-iehbN1MNMYa724THqZD2OFlufxSbdBv8v_wOi_V4K</recordid><startdate>202206</startdate><enddate>202206</enddate><creator>Aceto, Luca</creator><creator>Achilleos, Antonis</creator><creator>Anastasiadi, Elli</creator><creator>Ingolfsdottir, Anna</creator><general>Elsevier Inc</general><scope>AAYXX</scope><scope>CITATION</scope><orcidid>https://orcid.org/0000-0001-7526-9256</orcidid></search><sort><creationdate>202206</creationdate><title>Axiomatizing recursion-free, regular monitors</title><author>Aceto, Luca ; Achilleos, Antonis ; Anastasiadi, Elli ; Ingolfsdottir, Anna</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c303t-97330d41db10e00eac0037a74f87a545bfa20a0b08ea006d8c2350640fb3c0823</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2022</creationdate><topic>Axiomatization</topic><topic>Equational logic</topic><topic>Formal verification</topic><topic>Monitors</topic><topic>Process algebra</topic><topic>Verdict equivalence</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Aceto, Luca</creatorcontrib><creatorcontrib>Achilleos, Antonis</creatorcontrib><creatorcontrib>Anastasiadi, Elli</creatorcontrib><creatorcontrib>Ingolfsdottir, Anna</creatorcontrib><collection>CrossRef</collection><jtitle>Journal of logical and algebraic methods in programming</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Aceto, Luca</au><au>Achilleos, Antonis</au><au>Anastasiadi, Elli</au><au>Ingolfsdottir, Anna</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Axiomatizing recursion-free, regular monitors</atitle><jtitle>Journal of logical and algebraic methods in programming</jtitle><date>2022-06</date><risdate>2022</risdate><volume>127</volume><spage>100778</spage><pages>100778-</pages><artnum>100778</artnum><issn>2352-2208</issn><abstract>Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al. has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and ω-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and ω-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.</abstract><pub>Elsevier Inc</pub><doi>10.1016/j.jlamp.2022.100778</doi><orcidid>https://orcid.org/0000-0001-7526-9256</orcidid></addata></record>
fulltext fulltext
identifier ISSN: 2352-2208
ispartof Journal of logical and algebraic methods in programming, 2022-06, Vol.127, p.100778, Article 100778
issn 2352-2208
language eng
recordid cdi_crossref_primary_10_1016_j_jlamp_2022_100778
source ScienceDirect Freedom Collection 2022-2024
subjects Axiomatization
Equational logic
Formal verification
Monitors
Process algebra
Verdict equivalence
title Axiomatizing recursion-free, regular monitors
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-29T10%3A32%3A36IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-elsevier_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Axiomatizing%20recursion-free,%20regular%20monitors&rft.jtitle=Journal%20of%20logical%20and%20algebraic%20methods%20in%20programming&rft.au=Aceto,%20Luca&rft.date=2022-06&rft.volume=127&rft.spage=100778&rft.pages=100778-&rft.artnum=100778&rft.issn=2352-2208&rft_id=info:doi/10.1016/j.jlamp.2022.100778&rft_dat=%3Celsevier_cross%3ES2352220822000311%3C/elsevier_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c303t-97330d41db10e00eac0037a74f87a545bfa20a0b08ea006d8c2350640fb3c0823%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true