References

  1. Luca de Alfaro & Pritam Roy (2010): Solving games via three-valued abstraction refinement. Information and Computation 208(6), pp. 666–676, doi:10.1016/j.ic.2009.05.007.
  2. Roderick Bloem, Robert Könighofer & Martina Seidl (2014): SAT-Based Synthesis Methods for Safety Specs. In: VMCAI, LNCS 8318. Springer, pp. 1–20, doi:10.1007/978-3-642-54013-4_1.
  3. 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.
  4. Jerry R. Burch, Edmund M. Clarke & David E. Long (1991): Symbolic Model Checking with Partitioned Transistion Relations. In: VLSI, pp. 49–58.
  5. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu & Helmut Veith (2000): Counterexample-guided abstraction refinement. In: CAV, LNCS 1855. Springer, pp. 154–169, doi:10.1007/10722167_15.
  6. Edmund Clarke, Orna Grumberg, Muralidhar Talupur & Dong Wang (2003): High level verification of control intensive systems using predicate abstraction. In: MEMOCODE. IEEE, pp. 55–64, doi:10.1109/MEMCOD.2003.1210089.
  7. Olivier Coudert, Christian Berthet & Jean Christophe Madre (1990): Verification of synchronous sequential machines based on symbolic execution. In: Automatic verification methods for finite state systems, LNCS 407. Springer, pp. 365–373, doi:10.1007/3-540-52148-8_30.
  8. Olivier Coudert & Jean Christophe Madre (1990): A Unified Framework for the Formal Verification of Sequential Circuits. In: ICCAD, pp. 126–129.
  9. Olivier Coudert, Jean Christophe Madre & Christian Berthet (1991): Verifying temporal properties of sequential machines without building their state diagrams. In: CAV, LNCS 531. Springer, pp. 23–32, doi:10.1007/BFb0023716.
  10. Patrick Cousot & Radhia Cousot (1977): Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. ACM, pp. 238–252, doi:10.1145/512950.512973.
  11. Rüdiger Ehlers (2010): Symbolic Bounded Synthesis. In: CAV, LNCS 6174. Springer, pp. 365–379, doi:10.1007/s10703-011-0137-x.
  12. 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.
  13. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2009): An Antichain Algorithm for LTL Realizability. In: CAV, LNCS 5643. Springer, pp. 263–277, doi:10.1007/978-3-642-02658-4_22.
  14. Erich Grädel (2004): Positional Determinacy of Infinite Games. In: STACS, LNCS 2996. Springer, pp. 4–18, doi:10.1007/978-3-540-24749-4_2.
  15. Susanne Graf & Hassen Saïdi (1997): Construction of abstract state graphs with PVS. In: CAV, LNCS 1254. Springer, pp. 72–83, doi:10.1007/3-540-63166-6_10.
  16. Thomas A. Henzinger, Ranjit Jhala & Rupak Majumdar (2003): Counterexample-guided control. In: ICALP, LNCS 2719. Springer, pp. 886–902, doi:10.1007/3-540-45061-0_69.
  17. Thomas A. Henzinger, Rupak Majumdar, Freddy Y. C. Mang & Jean-François Raskin (2000): Abstract Interpretation of Game Properties. In: SAS, pp. 220–239, doi:10.1007/978-3-540-45099-3_12.
  18. Youpyo Hong, Peter A Beerel, Jerry R Burch & Kenneth L McMillan (1997): Safe BDD minimization using don't cares. In: Proceedings of the 34th annual Design Automation Conference. ACM, pp. 208–213, doi:10.1145/266021.266068.
  19. Robert P. Kurshan (1994): Automata-theoretic verification of coordinating processes. In: 11th International Conference on Analysis and Optimization of Systems Discrete Event Systems. Springer, pp. 16–28, doi:10.1007/BFb0033528.
  20. Edward J. McCluskey (1956): Minimization of Boolean Functions*. Bell system technical Journal 35(6), pp. 1417–1444, doi:10.1002/j.1538-7305.1956.tb03835.x.
  21. Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk & Adam Walker (2014): Solving Games without Controllable Predecessor. In: CAV. Springer.
  22. Christos H. Papadimitriou & Mihalis Yannakakis (1986): A note on succinct representations of graphs. Information and Control 71(3), pp. 181 – 185, doi:10.1016/S0019-9958(86)80009-2.
  23. Martin Sauerhoff & Ingo Wegener (1996): On the complexity of minimizing the OBDD size for incompletely specified functions. IEEE Trans. on CAD of Integrated Circuits and Systems 15(11), pp. 1435–1437, doi:10.1109/43.543775.
  24. Saqib Sohail & Fabio Somenzi (2009): Safety first: A two-stage algorithm for LTL games. FMCAD, pp. 77–84, doi:10.1007/s10009-012-0224-3.
  25. Fabio Somenzi (1999): Binary Decision Diagrams. In: Calculational system design 173. IOS Press, pp. 303.
  26. 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.
  27. Wolfgang Thomas (1995): On the synthesis of strategies in infinite games. In: STACS. Springer, pp. 1–13, doi:10.1007/3-540-59042-0_57.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org