References

  1. Henrik Reif Andersen (1997): An introduction to binary decision diagrams. Technical Report. Course Notes on the WWW.
  2. Krzysztof R. Apt & Erich Grädel (2011): Lectures in game theory for computer scientists. Cambridge University Press, doi:10.1017/CBO9780511973468.
  3. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Yaniv Sa'ar (2012): Synthesis of Reactive(1) designs. Journal of Computer and System Sciences 78(3), pp. 911 – 938, doi:10.1016/j.jcss.2011.08.007. Available at http://www.sciencedirect.com/science/article/pii/S0022000011000869. In Commemoration of Amir Pnueli.
  4. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2014): AbsSynthe: abstract synthesis from succinct safety specifications. In: Proceedings 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, July 23-24, 2014., pp. 100–116, doi:10.4204/EPTCS.157.11.
  5. Randal E. Bryant (1986): Graph-based algorithms for boolean function manipulation. Computers, IEEE Transactions on 100(8), pp. 677–691, doi:10.1109/TC.1986.1676819.
  6. Jerry Burch, Edmund M Clarke & David Long (1991): Symbolic model checking with partitioned transition relations. Computer Science Department, pp. 435.
  7. Edmund M. Clarke, Orna Grumberg & Doron Peled (2001): Model checking. MIT Press, doi:10.1016/B978-044450813-3/50026-6.
  8. E. Allen Emerson & Charanjit S. Jutla (1991): Tree automata, mu-calculus and determinacy. In: FOCS. IEEE, pp. 368–377, doi:10.1109/SFCS.1991.185392.
  9. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2010): Compositional Algorithms for LTL Synthesis. In: Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, Lecture Notes in Computer Science 6252. Springer, pp. 112–127, doi:10.1007/978-3-642-15643-410.
  10. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2011): Antichains and compositional algorithms for LTL synthesis. Formal Methods in System Design 39(3), pp. 261–296, doi:10.1007/s10703-011-0115-3.
  11. Guillermo A. Pérez: LTL2AIG. https://github.com/gaperez64/acacia_ltl2aig.
  12. Thomas R. Shiple, Ramin Hojati, Alberto L. Sangiovanni-Vincentelli & Robert K. Brayton (1994): Heuristic minimization of BDDs using don't cares. In: Proceedings of the 31st annual Design Automation Conference. ACM, pp. 225–231, doi:10.1145/196244.196360.
  13. Fabio Somenzi (1999): Binary Decision Diagrams. In: Calculational system design 173. IOS Press, pp. 303.
  14. Alfred Tarski (1955): A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics 5(2), pp. 285–309, doi:10.2140/pjm.1955.5.285.
  15. H.J. Touti, H. Savoj, B. Lin, R.K. Brayton & A. Sangiovanni-Vincentelli (1990): Implicit enumeration of finite state machines using bdd's. In: IEEE Int. Conference on CAD, doi:10.1109/ICCAD.1990.129860.
  16. Chao Wang, Gary D Hachtel & Fabio Somenzi (2003): The compositional far side of image computation. In: Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design. IEEE Computer Society, pp. 334, doi:10.1109/ICCAD.2003.159708.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org