Compositional Algorithms for LTL Synthesis

In this paper, we provide two compositional algorithms to solve safety games and apply them to provide compositional algorithms for the LTL synthesis problem. We have implemented those new compositional algorithms, and we demonstrate that they are able to handle full LTL specifications that are orders of magnitude larger than the specifications that can be treated by the current state of the art algorithms.

• Type: Conference
• Year: 2010
• Where: ATVA
• Authors: Emmanuel Filiot, Naiyong Jin, Jean-François Raskin
• Keywords: ATVA 2010, Compositional Algorithms, Hardware, LTL Specifications, LTL Synthesis Problem