Synthesis of Reactive(1) designs

Piterman, 2006, Synthesis of reactive(1) designs, vol. 3855, 364 Bloem, 2007, Automatic hardware synthesis from specifications: A case study, 1188 Bloem, 2007, Specify, compile, run: Hardware from PSL, vol. 190, 3 Jobstmann, 2007, Anzu: A tool for property synthesis, vol. 4590, 258 A. Church, Logic, arithmetic and automata, in: Proc. 1962 Int. Congr. Math. Upsala, 1963, pp. 23–25. Büchi, 1969, Solving sequential conditions by finite-state strategies, Trans. Amer. Math. Soc., 138, 295, 10.1090/S0002-9947-1969-0280205-0 Rabin, 1972, Automata on Infinite Objects and Churcʼs Problem, vol. 13 Pnueli, 1989, On the synthesis of an asynchronous reactive module, vol. 372, 652 Clarke, 1981, Design and synthesis of synchronization skeletons using branching time temporal logic, vol. 131, 52 Manna, 1984, Synthesis of communicating processes from temporal logic specifications, ACM Trans. Prog. Lang. Syst., 6, 68, 10.1145/357233.357237 R. Rosner, Modular synthesis of reactive systems, PhD thesis, Weizmann Institute of, Science, 1992. Wallmeier, 2003, Symbolic synthesis of finite-state controllers for request-response specifications, vol. 2759, 11 Alur, 2004, Deterministic generators and games for LTL fragments, ACM Trans. Comput. Log., 5, 1, 10.1145/963927.963928 Harding, 2005, A new algorithm for strategy synthesis in LTL games, vol. 3440, 477 Jobstmann, 2005, Program repair as a game, vol. 3576, 226 Asarin, 1998, Controller synthesis for timed automata, 469 Z. Manna, A. Pnueli, A hierarchy of temporal properties, in: Proc. 9th ACM Symp. Princ. of Dist. Comp., 1990, pp. 377–408. Kesten, 2005, Bridging the gap between fair simulation and trace inclusion, Inform. and Comput., 200, 36, 10.1016/j.ic.2005.01.006 Bloem, 2006, An algorithm for strongly connected component analysis in nlogn symbolic steps, Formal Methods Syst. Des., 28, 37, 10.1007/s10703-006-4341-z Pnueli, 1985, In transition from global to modular temporal reasoning about programs, Logics Models Concurrent Syst., 13, 123, 10.1007/978-3-642-82453-1_5 A. Ltd., AMBA specification (rev. 2), available from www.arm.com, 1999. B. Jobstmann, R. Bloem, Optimizations for LTL synthesis, in: Proc. of the 6th Int. Conf. on Formal Methods in Computer-Aided Design, IEEE, 2006, pp. 117–124. Sohail, 2008, A hybrid algorithm for LTL games, vol. 4905, 309 S. Sohail, F. Somenzi, Safety first: A two-stage algorithm for LTL games, in: Proc. of the 9th Int. Conf. on Formal Methods in Computer-Aided Design, IEEE, 2009, pp. 77–84. Henzinger, 2006, Solving games without determinization, vol. 4207, 394 A. Morgenstern, Symbolic controller synthesis for LTL specifications, PhD thesis, Universität Kaiserslautern, 2010. O. Kupferman, M. Vardi, Safraless decision procedures, in: Proc. of the 46th IEEE Symp. on Foundations of Computer Science, 2005, pp. 531–542. Kupferman, 2006, Safraless compositional synthesis, vol. 4144, 31 S. Schewe, Bounded synthesis, in: Automated Technology for Verification and Analysis, 2007, pp. 474–488. Filiot, 2009, An antichain algorithm for ltl realizability, vol. 5643, 263 Eisner, 2006 Kesten, 2000, Verification by augmented finitary abstraction, Inform. and Comput., 163, 203, 10.1006/inco.2000.3000 A. Pnueli, R. Rosner, Distributed reactive systems are hard to synthesize, in: Proc. of the 31st IEEE Symp. Found. of Comp. Sci., 1990, pp. 746–757. Kozen, 1983, Results on the propositional μ-calculus, Theoret. Comput. Sci., 27, 333, 10.1016/0304-3975(82)90125-6 E.A. Emerson, C.L. Lei, Efficient model-checking in fragments of the propositional modal μ-calculus, in: Proc. of the 1st IEEE Symp. Logic in Comp. Sci., 1986, pp. 267–278. Long, 1994, An improved algorithm for the evaluation of fixpoint expressions, vol. 818, 338 Jurdziński, 2000, Small progress measures for solving parity games, vol. 1770, 290 Emerson, 1997, Model checking and the μ-calculus, 185 O. Lichtenstein, Decidability, completeness, and extensions of linear time temporal logic, PhD thesis, Weizmann Institute of Science, 1991. Pnueli, 2010, JTLV: A framework for developing verification algorithms, vol. 6174, 171 Juvekar, 2006, Minimizing generalized Büchi automata, vol. 4144, 45 Bloem, 2010, Robustness in the presence of liveness, vol. 6174, 410 R. Koenighofer, G. Hofferek, R. Bloem, Debugging formal specifications using simple counterstrategies, in: Proc. of the 9th Int. Conf. on Formal Methods in Computer-Aided Design, IEEE, 2009, pp. 152–159. Kukula, 2000, Building circuits from relations, vol. 1855, 113 Somenzi A.J. Hu, D. Dill, Reducing BDD size by exploiting functional dependencies, in: Proc. of the Design Automation Conference, Dallas, TX, 1993, pp. 266–271. Prosyd – Property-Based System Design, http://www.prosyd.org/, EU grant 507219, 2004–2007. Abadi, 1991, The existence of refinement mappings, Theoret. Comput. Sci., 82, 253, 10.1016/0304-3975(91)90224-P Dederichs, 1990, Safety and liveness from a methodological point of view, Inform. Process. Lett., 36, 25, 10.1016/0020-0190(90)90181-V Abadi, 1991, Preserving liveness: Comments on “safety and liveness from a methodological point of view”, Inform. Process. Lett., 40, 141, 10.1016/0020-0190(91)90168-H Kesten, 1998, Algorithmic verification of linear temporal logic specifications, vol. 1443, 1 Pnueli, 2008, On the merits of temporal testers, vol. 5000, 172 A. Pnueli, R. Rosner, On the synthesis of a reactive module, in: Proc. of the 16th ACM Symp. Princ. of Prog. Lang., 1989, pp. 179–190. Synthesis Y. Godhal, K. Chatterjee, T.A. Henzinger, Synthesis of AMBA AHB from formal specification, Tech. Rep. abs/1001.2811, CORR, 2010. Hachtel, 1996 I. Pill, S. Semprini, R. Cavada, M. Roveri, R. Bloem, A. Cimatti, Formal analysis of hardware requirements, in: Proc. of the Design Automation Conference, 2006, pp. 821–826. Cimatti, 2008, Diagnostic information for realizability, vol. 4905, 52 Chatterjee, 2008, Environment assumptions for synthesis, vol. 5201, 147 Bloem, 2009, Better quality in synthesis through quantitative objectives, vol. 5643, 140 R. Bloem, K. Greimel, T. Henzinger, B. Jobstmann, Synthesizing robust systems, in: Proc. of the 9th Int. Conf. on Formal Methods in Computer-Aided Design, IEEE, 2009, pp. 85–92. A. Pnueli, U. Klein, Synthesis of programs from temporal property specifications, in: Proc. Formal Methods and Models for Co-Design (MEMOCODE), IEEE, 2009, pp. 1–7. Abadi, 1989, Realizable and unrealizable specifications of reactive systems, vol. 372, 1 Pnueli, 1996, A platform for combining deductive with algorithmic verification, vol. 1102, 184 Bloem, 2007, Rat: A tool for the formal analysis of requirements, vol. 4590, 263 Bloem, 2010, RATSY — a new requirements analysis tool with synthesis, vol. 6174, 425 H. Kress-Gazit, G.E. Fainekos, G.J. Pappas, Whereʼs waldo? sensor-based temporal logic motion planning, in: Conf. on Robotics and Automation, IEEE, 2007, pp. 3116–3121. D.C. Conner, H. Kress-Gazit, H. Choset, A.A. Rizzi, G.J. Pappas, Valet parking without a valet, in: Conf. on Intelligent Robots and Systems, IEEE, 2007, pp. 572–577. H. Kress-Gazit, G. Fainekos, G. Pappas, From structured English to robot motion, in: Proc. IEEE/RSJ Int. Conf. on Intelligent Robots and Systems, IEEE, 2007, pp. 2717–2722. T. Wongpiromsarn, U. Topcu, R.M. Murray, Receding horizon temporal logic planning for dynamical systems, in: Proc. of the 48th IEEE Conf. on Decision and Control, IEEE, 2009, pp. 5997–6004. T. Wongpiromsarn, U. Topcu, R.M. Murray, Receding horizon control for temporal logic specifications, in: Proc. of the 13th ACM Int. Conf. on Hybrid Systems: Computation and Control, ACM, 2010, pp. 101–110. T. Wongpiromsarn, U. Topcu, R.M. Murray, Automatic synthesis of robust embedded control software, in: In AAAI Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010, pp. 104–110. Kugler, 2009, Controller synthesis from LSC requirements, vol. 5503, 79 Kugler, 2009, Compositional synthesis of reactive systems from live sequence chart specifications, vol. 5505, 77 S. Maoz, Y. Saʼar, Aspectltl: an aspect language for ltl specifications, in: Proc. of the 10th Int. Conf. on Aspect-Oriented Software Development, ACM, 2011, pp. 19–30.