Incorporating monitors in reactive synthesis without paying the price

DOI10.1007/978-3-030-88885-5_22zbMath1497.68284arXiv2107.00929OpenAlexW3208661613MaRDI QIDQ2147214

Gerardo Schneider, Shaun Azzopardi, Nir Piterman

Publication date: 22 June 2022

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

zbMATH Keywords

synthesistemporal logicmonitoringsymbolic automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Uses Software

• contractLarva
• Strix

Cites Work

• Unnamed Item
• Unnamed Item
• Parametric linear dynamic logic
• Practical synthesis of reactive systems from LTL specifications via parity games
• Synthesis of Trigger Properties
• Temporal Logic and Fair Discrete Systems
• Temporal logic can be more expressive
• Comparing LTL Semantics for Runtime Verification
• Synthesis from Component Libraries
• LTL Model Checking of Interval Markov Chains
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• A counting semantics for monitoring LTL specifications over finite traces

This page was built for publication: Incorporating monitors in reactive synthesis without paying the price