Reactive synthesis with maximum realizability of linear temporal logic specifications
From MaRDI portal
Publication:2303876
DOI10.1007/s00236-019-00348-4zbMath1435.68193arXiv1910.02561OpenAlexW2987958996MaRDI QIDQ2303876
Rayna Dimitrova, Ufuk Topcu, Mahsa Ghasemi
Publication date: 6 March 2020
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1910.02561
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Artificial intelligence for robotics (68T40) Computational aspects of satisfiability (68R07)
Related Items
A weakness measure for GR(1) formulae, Reactive synthesis with maximum realizability of linear temporal logic specifications
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Safraless LTL synthesis considering maximal realizability
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Least-violating control strategy synthesis with safety rules
- Formally Reasoning About Quality
- Open-WBO: A Modular MaxSAT Solver,
- Encodings of Bounded Synthesis
- Bounded Synthesis
- Ranking Automata and Games for Prioritized Requirements
- Better Quality in Synthesis through Quantitative Objectives
- Robust Linear Temporal Logic
- Boolean Abstraction for Temporal Logic Satisfiability
- Diagnostic Information for Realizability
- Model checking of safety properties
