An Antichain Algorithm for LTL Realizability

  • Emmanuel Filiot
  • Naiyong Jin
  • Jean-François Raskin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


In this paper, we study the structure of underlying automata based constructions for solving the LTL realizability and synthesis problem. We show how to reduce the LTL realizability problem to a game with an observer that checks that the game visits a bounded number of times accepting states of a universal co-Büchi word automaton. We show that such an observer can be made deterministic and that this deterministic observer has a nice structure which can be exploited by an incremental algorithm that manipulates antichains of game positions. We have implemented this new algorithm and our first results are very encouraging.


Linear Temporal Logic Winning Strategy Acceptance Condition Incremental Algorithm Tree Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, G., Dezani-Ciancaglini, M., Ronchi Della Rocca, S. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  2. 2.
    Acacia (2009),
  3. 3.
    Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Bouajjani, A., Habermehl, P., Holík, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: CIAA, pp. 57–67 (2008)Google Scholar
  5. 5.
    De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Doyen, L., Raskin, J.-F.: Improved algorithms for the automata-based approach to model-checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 451–465. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Fogarty, S., Vardi, M.: Buechi complementation and size-change termination. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 16–30. Springer, Heidelberg (2008)Google Scholar
  8. 8.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  9. 9.
    Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117–124. IEEE Computer Society, Los Alamitos (2006)Google Scholar
  10. 10.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS: IEEE Symposium on Foundations of Computer Science (FOCS) (2005)Google Scholar
  11. 11.
    Martin, D.: Borel determinacy. Annals of Mathematics 102, 363–371 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Piterman, N.: From nondeterministic büchi and streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3) (2007)Google Scholar
  13. 13.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symposium on Principles of Programming Languages (POPL). ACM, New York (1989)Google Scholar
  14. 14.
    Raskin, J.-F., Chatterjee, K., Doyen, L., Henzinger, T.A.: Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science 3(3) (2007)Google Scholar
  15. 15.
    Rosner, R.: Modular synthesis of reactive systems. Ph.d. dissertation, Weizmann Institute of Science (1992)Google Scholar
  16. 16.
    Ruys, T.C., Holzmann, G.J.: Advanced SPIN Tutorial. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 304–305. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Miyano, S., Hayashi, T.: Alternating automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Safra, S.: On the complexity of ω automata. In: FOCS, pp. 319–327 (1988)Google Scholar
  19. 19.
    Somenzi, F., Bloem, R.: Efficient büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  20. 20.
    Thomas, W.: Church’s problem and a tour through automata theory. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 635–655. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    De Wulf, M., Doyen, L., Maquet, N., Raskin, J.-F.: Antichains: Alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 63–77. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Emmanuel Filiot
    • 1
  • Naiyong Jin
    • 1
  • Jean-François Raskin
    • 1
  1. 1.CS, Faculty of SciencesUniversité Libre de Bruxelles (U.L.B.)Belgium

Personalised recommendations