Luca Aceto ; Ian Cassar ; Adrian Francalanza ; Anna Ingolfsdottir - Bidirectional Runtime Enforcement of First-Order Branching-Time Properties

lmcs:8944 - Logical Methods in Computer Science, February 28, 2023, Volume 19, Issue 1 - https://doi.org/10.46298/lmcs-19(1:14)2023
Bidirectional Runtime Enforcement of First-Order Branching-Time PropertiesArticle

Authors: Luca Aceto ; Ian Cassar ; Adrian Francalanza ; Anna Ingolfsdottir

    Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.


    Volume: Volume 19, Issue 1
    Published on: February 28, 2023
    Accepted on: January 19, 2023
    Submitted on: January 11, 2022
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Computer Science - Software Engineering,F.3.1,F.3.2,D.2.4
    Funding:
      Source : OpenAIRE Graph
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233

    Consultation statistics

    This page has been seen 4989 times.
    This article's PDF has been downloaded 350 times.