Bidirectional Runtime Enforcement of First-Order Branching-Time Properties

DOI10.46298/LMCS-19(1:14)2023MaRDI QIDQ5883741zbMATH OpenOpenAlexFDO

Authors Luca Aceto, Ian Cassar, Adrian Francalanza

Publication date 22 March 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2201.03108v4

zbMATH Keywords

modal \(\mu\)-calculusmonitor synthesisproperty enforcementfirst-order safety propertiesruntime monitors

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• On bidirectional runtime enforcement
• On first-order runtime enforcement of branching-time properties
• On runtime enforcement via suppressions
• Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
• Compositional runtime enforcement revisited

Cites work

• scientific article; zbMATH DE number 1330129 (Why is no real title available?)
• scientific article; zbMATH DE number 1088043 (Why is no real title available?)
• A calculus of mobile processes. I
• A framework for parameterized monitorability
• A modal logic for message passing processes
• A theory of monitors
• Compositional reasoning for explicit resource management in channel-based concurrency
• Computer says no: verdict explainability for runtime monitors using a local proof system
• Consistently-detecting monitors
• Determinizing monitors for HML with recursion
• Elements of automata theory. Translated from the French by Reuben Thomas
• Enforcing non-safety security policies with program monitors
• Introduction to bisimulation and coinduction
• Maximally permissive controlled system synthesis for non-determinism and modal logic
• Monitorability for the Hennessy-Milner logic with recursion
• Monitoring for silent actions
• Monitoring networks through multiparty session types
• Monitors and blame assignment for higher-order session types
• On bidirectional runtime enforcement
• On runtime enforcement via suppressions
• Proof systems for message-passing process algebras
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Reactive Systems
• Results on the propositional \(\mu\)-calculus
• Shield synthesis
• Streaming transducers for algorithmic verification of single-pass list-processing programs
• Survey on JavaScript security policies and their enforcement mechanisms in a web browser
• Synthesising correct concurrent runtime monitors
• Which security policies are enforceable by runtime monitors? A survey

Cited in

(2)

• On first-order runtime enforcement of branching-time properties
• Real-time policy enforcement with metric first-order temporal logic

This page was built for publication: Bidirectional Runtime Enforcement of First-Order Branching-Time Properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5883741)