Safraless LTL synthesis considering maximal realizability

DOI10.1007/s00236-016-0280-3zbMath1380.68285OpenAlexW2528851098WikidataQ59607128 ScholiaQ59607128MaRDI QIDQ1674867

Atsushi Ueno, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki, Takashi Tomita

Publication date: 26 October 2017

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-016-0280-3

Mathematics Subject Classification ID

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

Related Items

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

Uses Software

• SPOT
• LTL2BA
• Acacia+

Cites Work

• Symbolic bounded synthesis
• Faster algorithms for mean-payoff games
• Positional strategies for mean payoff games
• Reasoning about infinite computations
• The complexity of mean payoff games on graphs
• Strategy synthesis for multi-dimensional quantitative objectives
• Synthesizing robust systems
• From LTL to deterministic automata. A safraless compositional approach
• LTL to Büchi Automata Translation: Fast and More Deterministic
• Bounded Synthesis
• Environment Assumptions for Synthesis
• Tighter Bounds for the Determinisation of Büchi Automata
• Better Quality in Synthesis through Quantitative Objectives
• Tight Bounds for the Determinisation and Complementation of Generalised Büchi Automata
• LTL Model Checking of Interval Markov Chains
• Synthesis from LTL Specifications with Mean-Payoff Objectives
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item