Real-time policy enforcement with metric first-order temporal logic

DOI10.1007/978-3-031-17146-8_11zbMath1524.68193MaRDI QIDQ6109435

David A. Basin, François Hublet, Srđan Krstić

Publication date: 28 July 2023

Published in: Computer Security – ESORICS 2022 (Search for Journal in Brave)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Unnamed Item
• Antichains and compositional algorithms for LTL synthesis
• Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
• A formally verified, optimized monitor for metric first-order dynamic logic
• On bidirectional runtime enforcement
• \textsc{MightyL}: a compositional translation from MITL to timed automata
• First-order temporal logic monitoring with BDDs
• Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\)
• Monitoring Metric First-Order Temporal Properties
• Enforceable Security Policies Revisited
• Reactive synthesis from signal temporal logic specifications
• Unbeast: Symbolic Bounded Synthesis
• Bounded Synthesis
• From MITL to Timed Automata
• The benefits of relaxing punctuality
• Controller Synthesis for MTL Specifications
• Enforcing Non-safety Security Policies with Program Monitors