Exploiting structure in LTL synthesis

  • Emmanuel Filiot
  • Naiyong Jin
  • Jean-François Raskin
Synthesis

DOI: 10.1007/s10009-012-0222-5

Cite this article as:
Filiot, E., Jin, N. & Raskin, JF. Int J Softw Tools Technol Transfer (2013) 15: 541. doi:10.1007/s10009-012-0222-5

Abstract

In this paper, we show how to exploit the structure of some automata-based construction to efficiently solve the LTL synthesis problem. We focus on a construction proposed in Schewe and Finkbeiner that reduces the synthesis problem to a safety game, which can then be solved by computing the solution of the classical fixpoint equation νX.SafeCPre(X), where CPre(X) are the controllable predecessors of X. We have shown in previous works that the sets computed during the fixpoint algorithm can be equipped with a partial order that allows one to represent them very compactly, by the antichain of their maximal elements. However the computation of CPre(X) cannot be done in polynomial time when X is represented by an antichain (unless P = NP). This motivates the use of SAT solvers to compute CPre(X). Also, we show that the CPre operator can be replaced by a weaker operator CPrecrit where the adversary is restricted to play a subset of critical signals. We show that the fixpoints of the two operators coincide, and so, instead of applying iteratively CPre, we can apply iteratively CPrecrit. In practice, this leads to important improvements on previous LTL synthesis methods. The reduction to SAT problems and the weakening of the CPre operator into CPrecrit and their performance evaluations are new.

Keywords

Synthesis Reactive systems Temporal logics Antichain algorithms 

Copyright information

© Springer-Verlag 2012

Authors and Affiliations

  • Emmanuel Filiot
    • 1
  • Naiyong Jin
    • 2
  • Jean-François Raskin
    • 1
  1. 1.CS, Université Libre de BruxellesBrusselsBelgium
  2. 2.Synopsys CompanyShanghaiPeople’s Republic of China

Personalised recommendations