Efficient controller synthesis for a fragment of MTL₀,
From MaRDI portal
Publication:2249659
DOI10.1007/S00236-013-0189-ZzbMATH Open1360.68578OpenAlexW1739620681MaRDI QIDQ2249659FDOQ2249659
Authors: Alexandre David, Guangyuan Li, P. E. Bulychev, Kim G. Larsen 
Publication date: 3 July 2014
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00236-013-0189-z
Recommendations
- Controller Synthesis for MTL Specifications
- On Synthesizing Controllers from Bounded-Response Properties
- Template-based controller synthesis for timed systems
- A method for the synthesis of controllers to handle safety, liveness, and real-time constraints
- Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Formal Methods for the Design of Real-Time Systems
- A theory of timed automata
- The benefits of relaxing punctuality
- Supervisory Control of a Class of Discrete Event Processes
- Using branching time temporal logic to synthesize synchronization skeletons
- Title not available (Why is that?)
- Synthesis of Reactive(1) designs
- Title not available (Why is that?)
- LTL to Büchi Automata Translation: Fast and More Deterministic
- On the synthesis of discrete controllers for timed systems
- CONCUR 2005 – Concurrency Theory
- Bounded Synthesis
- Synthesis of Communicating Processes from Temporal Logic Specifications
- On Synthesizing Controllers from Bounded-Response Properties
- Verification, Model Checking, and Abstract Interpretation
- Solving Sequential Conditions by Finite-State Strategies
- An Antichain Algorithm for LTL Realizability
- Safraless Compositional Synthesis
- Efficient Detection of Zeno Runs in Timed Automata
- Formal Modeling and Analysis of Timed Systems
- Safraless Procedures for Timed Specifications
- Title not available (Why is that?)
- Realizability of real-time logics
- Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic
- Controller Synthesis for MTL Specifications
Cited In (6)
- Controller Synthesis for MDPs and Frequency LTL $$_{\setminus \mathbf{G}\mathbf U}$$
- Further reduction of minimal first-met bad markings for the computationally efficient synthesis of a maximally permissive controller
- A method for the synthesis of controllers to handle safety, liveness, and real-time constraints
- Real-time policy enforcement with metric first-order temporal logic
- Taming large bounds in synthesis from bounded-liveness specifications
- Controller Synthesis for MTL Specifications
Uses Software
This page was built for publication: Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2249659)
