On Synthesizing Controllers from Bounded-Response Properties

In this paper we propose a complete chain for synthesizing controllers from high-level specifications. From real-time properties expressed in the logic MTL we generate, under bounded-variability assumptions, deterministic timed automata to which we apply safety synthesis algorithms to derive a controller that satisfies the properties by construction. Some preliminary experimental results are reported.

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Oded Maler, Dejan Nickovic, Amir Pnueli
• Keywords: CAV 2007, Deterministic Timed Automata, Formal Methods, Real-time Properties, Safety Synthesis Algorithms