A game approach to the parametric control of real-time systems

References

• Alfaro, L. D. , , Henzinger, T. A. , & Majumdar, R. (2001). Symbolic algorithms for infinite-state games. In Proceedings of the 12th international conference on concurrency theory (CONCUR ′01) (pp. 536–550). Berlin, Germany: Springer.
   Google Scholar
• Alur, R. , Courcoubetis, C. , Halbwachs, N. , Henzinger, T. , Ho, P.-H. , Nicollin, X. ,…  Yovine, S. (1995). The algorithmic analysis of hybrid systems. Theoretical Computer Science , 138 (1), 3–34.
   Web of Science ®Google Scholar
• Alur, R. , & Dill, D. (1994). A theory of timed automata. Theoretical Computer Science , 126 (2), 183–235.
   Web of Science ®Google Scholar
• Alur, R. , Henzinger, T. A. , & Vardi, M. Y. (1993). Parametric real-time reasoning. In ACM symposium on theory of computing (pp. 592–601).New York: ACM.
   Google Scholar
• André, É. , Chatain, T. , Encrenaz, E. , & Fribourg, L. (2009). An inverse method for parametric timed automata. International Journal of Foundations of Computer Science , 20 (5), 819–836.
   Web of Science ®Google Scholar
• Asarin, E. , Maler, O. , Pnueli, A. , & Sifakis, J. (1998). Controller synthesis for timed automata. In Proceeding of the IFAC symposium on system structure and control . Amsterdam, The Netherlands: Elsevier.
   Google Scholar
• Bandur, V. , Kahl, W. , & Wassyng, A. (2012). Microcontroller assembly synthesis from timed automaton task specifications. In Formal methods for industrial critical systems – 17th international workshop, FMICS 2012 , (pp. 63–77). Paris, France: Springer.
   Google Scholar
• Behrmann, G. , Cougnard, A. , David, A. , Fleury, E. , Larsen, K. G. , & Lime, D. (2007). Uppaal-tiga: Time for playing games! In Conference on computer aided verification (CAV 2007) (pp. 121–125).
   Google Scholar
• Berthomieu, B. , Lime, D. , Roux, O. H. , & Vernadat, F. (2007). Reachability problems and abstract state spaces for time Petri nets with stopwatches. Journal of Discrete Event Dynamic Systems (jDEDS) , 17 (2), 133–158.
   Web of Science ®Google Scholar
• Bozzelli, L. , & La Torre, S. (2009). Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design , 35 (2), 121–151.
   Web of Science ®Google Scholar
• Bruyère, V. , & Raskin, J.-F. (2007). Real-time model-checking: Parameters everywhere. Logical Methods in Computer Science , 3 (1), 1–30.
   Web of Science ®Google Scholar
• Cassez, F. , David, A. , Fleury, E. , Larsen, K. , & Lime, D. (2005). Efficient on-the-fly algorithms for the analysis of timed games. In CONCUR′05 , LNCS 3653. Berlin, Germany: Springer.
   Google Scholar
• Cassez, F. , Jessen, J. J. , Larsen, K. G. , Raskin, J.-F. , & Reynier, P.-A. (2009). Automatic synthesis of robust and optimal controllers – an industrial case study. In HSCC (pp. 90–104). Berlin, Germany: Springer.
   Google Scholar
• Devillers, R. R. , Didier, J. , & Klaudel, H. (2013, July 8–10). Implementing timed automata specifications: The “sandwich” approach. In 13th International conference on application of concurrency to system design, ACSD 2013 , (pp. 226–235). Washington: IEEE.
   Google Scholar
• Fleming, S. T. , & Thomas, D. B. (2013, September 2–4). FPGA based control for real time systems. In 23rd International conference on field programmable logic and applications, FPL 2013 , (pp. 1–2). Washington: IEEE.
   Google Scholar
• Henzinger, T. A. , Ho, P.-H. , & Wong-toi, H. (1997). Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer , 1 , 460–463.
   Google Scholar
• Henzinger, T. A. , Nicollin, X. , Sifakis, J. , & Yovine, S. (1994). Symbolic model checking for real-time systems. Information and Computation , 111 (2), 193–244.
   Web of Science ®Google Scholar
• Hune, T. , Romijn, J. , Stoelinga, M. , & Vaandrager, F. (2002). Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming , 52–53 , 183–220.
   Google Scholar
• Jessen, J. J. , Rasmussen, J. I. , Larsen, K. G. , & David, A. (2007, October 3–5). Guided controller synthesis for climate controller using Uppaal Tiga. In Formal modeling and analysis of timed systems, 5th international conference, FORMATS 2007 , LNCS 4763 (pp. 227–240). Berlin, Germany: Springer.
   Google Scholar
• Jovanović, A. , Lime, D. , & Roux, O. H. (2013). Synthesis of bounded integer parameters for parametric timed reachability games. In 11th International symposium on automated technology for verification and analysis (ATVA 2013) (Vol. 8172, pp. 87–101). Hanoi: Springer.
   Google Scholar
• Jovanović, A. , Lime, D. , & Roux, O. H. (2015). Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engineering (TSE) , 41 (5), 445–461.
   Web of Science ®Google Scholar
• Larsen, K. G. , Pettersson, P. , & Yi, W. (1995). Model-checking for real-time systems. In Fundamentals of computation theory , LNCS 965 (pp. 62–88). Berlin, Germany: Springer.
   Google Scholar
• Lime, D. , & Roux, O. H. (2009). Formal verification of real-time systems with preemptive scheduling. Journal of Real-Time Systems , 41 (2), 118–151.
   Web of Science ®Google Scholar
• Maler, O. , Pnueli, A. , & Sifakis, J. (1995). On the synthesis of discrete controllers for timed systems. In Proceedings STACS’95 , LNCS 900 (pp. (229–242). Berlin, Germany: Springer.
   Google Scholar
• Parquier, B. , Rioux, L. , Henia, R. , Soulat, R. , Roux, O. H. , Lime, D. , & André, E. (2016). Applying parametric model-checking techniques for reusing real-time critical systems. In 5th International workshop on formal techniques for safety-critical systems (FTSCS 2016), Vol. 694 of CCIS . Tokyo: Springer.
   Google Scholar
• Wulf, M. D. , Doyen, L. , & Raskin, J. (2005, July 18–22). Systematic implementation of real-time models. In FM 2005: Formal methods. International symposium of formal methods , (pp. (139–156). Berlin, Germany: Springer.
   Google Scholar