Reactive synthesis with maximum realizability of linear temporal logic specifications

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

Mathematics Subject Classification ID

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 (2)

A weakness measure for GR(1) formulae ⋮ Reactive synthesis with maximum realizability of linear temporal logic specifications

Uses Software

• SPOT
• Open-WBO
• PackUp

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

This page was built for publication: Reactive synthesis with maximum realizability of linear temporal logic specifications