Exploiting structure in LTL synthesis

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

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 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
  2. 2.
    Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: International Conference on Automata, Languages and Programming (ICALP) (1989)Google Scholar
  3. 3.
    Bloem R., Galler S., Jobstmann B., Piterman N., Pnueli A., Weiglhofer M.: Specify, compile, run: hardware from psl. Electr. Notes Theor. Comput. Sci. 190(4), 3–16 (2007)CrossRefGoogle Scholar
  4. 4.
    Ehlers, R.: Symbolic bounded synthesis. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, vol 6174, pp. 365–379. Springer, Berlin (2010)Google Scholar
  5. 5.
    Eén, N., Sörensson, N.: MiniSat. http://minisat.se/ (2010)
  6. 6.
    Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, vol 5643, pp. 263–277. Springer, Berlin (2009)Google Scholar
  7. 7.
    Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 112–127 (2010)Google Scholar
  8. 8.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, pp. 53–65. Springer, Berlin (2001)Google Scholar
  9. 9.
    Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 117–124. IEEE Computer Society (2006)Google Scholar
  10. 10.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: IEEE Symposium on Foundations of Computer Science (FOCS) (2005)Google Scholar
  11. 11.
  12. 12.
  13. 13.
    Martin, D.: Borel determinacy. In: Annals of Mathematics, vol. 102, pp. 363–371 (1975)Google Scholar
  14. 14.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symposium on Principles of Programming Languages (POPL). ACM, New York 1989Google Scholar
  15. 15.
    Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Proceedings of 16th ICALP, 1989Google Scholar
  16. 16.
    Safra, S.: On the complexity of ω automata. In: IEEE Symposium on Foundations of Computer Science (FOCS), pp. 319–327 (1988)Google Scholar
  17. 17.
    Schewe, S., Finkbeiner, B.: Bounded synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). LNCS, vol 4762, pp. 474–488. Springer, Berlin (2007)Google Scholar
  18. 18.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Proceedings of the International Conference on Computer Aided Verification (CAV) (2000)Google Scholar
  19. 19.
    Thomas, W.: Church’s problem and a tour through automata theory. In: Pillars of Computer Science. LNCS, vol 4800, pp 635–655. Springer, Berlin (2008)Google Scholar
  20. 20.
  21. 21.

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