BOCoSy: small but powerful symbolic output-feedback control. (English) Zbl 07807732
Proceedings of the 25th ACM international conference on hybrid systems: computation and control, HSCC 2022, part of CPS-IoT week, Milan, Italy and virtual, May 4–6, 2022. New York, NY: Association for Computing Machinery (ACM). Paper No. 24, 11 p. (2022).
MSC:
| 68Q45 | Formal languages and automata |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |
References:
| [1] | WA Apaza-Perez, Antoine Girard, Christophe Combastel, and Ali Zolghadri. 2020. Symbolic observer-based controller for uncertain nonlinear systems. IEEE Control Systems Letters 5, 4 (2020), 1297-1302. |
| [2] | Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checkit. MIT Press. · Zbl 1179.68076 |
| [3] | Armin Biere. 2007. The AIGER And-Inverter Graph (AIG) Format Version 20071012. Technical Report 07/1. Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria. |
| [4] | Armin Biere, Keijo Heljanko, and Siert Wieringa. 2011. AIGER 1.9 And Beyond. Technical Report 11/2. Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria. |
| [5] | Armin Biere, Florian Lonsing, and Martina Seidl. 2011. Blocked Clause Elimination for QBF. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings(Lecture Notes in Computer Science, Vol. 6803), Nikolaj Björner and Viorica Sofronie-Stokkermans (Eds.). Springer, 101-115. https://doi.org/10.1007/978-3-642-22438-6_10 · Zbl 1341.68181 |
| [6] | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. 2007. Algorithms for Omega-Regular Games with Imperfect Information. Logical Methods in Computer Science 3, 3 (2007). · Zbl 1125.91028 |
| [7] | Rayna Dimitrova and Bernd Finkbeiner. 2008. Abstraction Refinement for Games with Incomplete Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 2008(LIPIcs, Vol. 2), Ramesh Hariharan, Madhavan Mukund, and V. Vinay (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 175-186. https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1751 · Zbl 1248.68327 |
| [8] | Rayna Dimitrova and Bernd Finkbeiner. 2012. Counterexample-Guided Synthesis of Observation Predicates. In FORMATS 2012(Lecture Notes in Computer Science, Vol. 7595), Marcin Jurdzinski and Dejan Nickovic (Eds.). Springer, 107-122. https://doi.org/10.1007/978-3-642-33365-1_9 · Zbl 1374.68083 |
| [9] | Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. 2016. Spot 2.0 - A Framework for LTL and \omega -Automata Manipulation. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings(Lecture Notes in Computer Science, Vol. 9938), Cyrille Artho, Axel Legay, and Doron Peled (Eds.). 122-129. https://doi.org/10.1007/978-3-319-46520-3_8 |
| [10] | Rüdiger Ehlers and Ufuk Topcu. 2015. Estimator-based reactive synthesis under incomplete information. In HSCC’15. ACM, 249-258. · Zbl 1366.68167 |
| [11] | Donglei Fan and Danielle C Tarraf. 2018. Output Observability of Systems Over Finite Alphabets With Linear Internal Dynamics. IEEE TAC 63, 10 (2018), 3404-3417. · Zbl 1423.93064 |
| [12] | Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup. 2017. Encodings of Bounded Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I(Lecture Notes in Computer Science, Vol. 10205), Axel Legay and Tiziana Margaria (Eds.). 354-370. https://doi.org/10.1007/978-3-662-54577-5_20 · Zbl 1452.68118 |
| [13] | Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup. 2017. BoSy: An experimentation framework for bounded synthesis. In International Conference on Computer Aided Verification. Springer, 325-332. · Zbl 1452.68118 |
| [14] | Jesko Hecking-Harbusch and Leander Tentrup. 2018. Solving QBF by Abstraction. In Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018(EPTCS, Vol. 277), Andrea Orlandini and Martin Zimmermann (Eds.). 88-102. https://doi.org/10.4204/EPTCS.277.7 · Zbl 1528.68223 |
| [15] | Thomas A. Henzinger, Rupak Majumdar, Freddy Y. C. Mang, and Jean-François Raskin. 2000. Abstract Interpretation of Game Properties. In SAS. 220-239. · Zbl 0966.68150 |
| [16] | Kyle Hsu, Rupak Majumdar, Kaushik Mallik, and Anne-Kathrin Schmuck. 2018. Lazy Abstraction-Based Control for Safety Specifications. In 2018 IEEE Conference on Decision and Control (CDC). IEEE, 4902-4907. · Zbl 1417.93061 |
| [17] | Omar Hussien and Paulo Tabuada. 2018. Lazy controller synthesis using three-valued abstractions for safety and reachability specifications. In 2018 IEEE Conference on Decision and Control (CDC). IEEE, 3567-3572. |
| [18] | Elena Ivanova and Antoine Girard. 2020. Lazy safety controller synthesis with multi-scale adaptive-sampling abstractions of nonlinear systems. IFAC-PapersOnLine 53, 2 (2020), 1837-1843. |
| [19] | Swen Jacobs, Felix Klein, and Sebastian Schirmer. 2016. A High-Level LTL Synthesis Format: TLSF v1.1. In Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016(EPTCS, Vol. 229), Ruzica Piskac and Rayna Dimitrova (Eds.). 112-132. https://doi.org/10.4204/EPTCS.229.10 |
| [20] | Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. 2016. Solving QBF with counterexample guided refinement. Artif. Intell. 234(2016), 1-25. https://doi.org/10.1016/j.artint.2016.01.004 · Zbl 1351.68254 |
| [21] | Gabriel Kalyon, Tristan Le Gall, Hervé Marchand, and Thierry Massart. 2009. Control of infinite Symbolic Transition Systems under partial observation. In 2009 European Control Conference (ECC). 1456-1462. https://doi.org/10.23919/ECC.2009.7074611 · Zbl 1242.93074 |
| [22] | Orna Kupferman and Moshe Y. Vardi. 2000. Synthesis with Incomplete Informatio. Springer Netherlands, Dordrecht, 109-127. https://doi.org/10.1007/978-94-015-9586-5_6 · Zbl 0953.68090 |
| [23] | O. Kupferman and M. Y. Vardi. 2005. Safraless decision procedures. In 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS’05). 531-540. |
| [24] | Rupak Majumdar, Necmiye Ozay, and Anne-Kathrin Schmuck. 2020. On abstraction-based controller design with output feedback. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control. 1-11. · Zbl 07300856 |
| [25] | Masashi Mizoguchi and Toshimitsu Ushio. 2018. Deadlock-free output feedback controller design based on approximately abstracted observers. Nonlinear Analysis: Hybrid Systems 30 (2018), 58-71. · Zbl 1408.93062 |
| [26] | Thomas Moor, Jörg Raisch, and Siu O’young. 2002. Discrete supervisory control of hybrid systems based on l-complete approximations. Discrete Event Dynamic Systems 12, 1 (2002), 83-107. · Zbl 1002.93016 |
| [27] | Giordano Pola, Maria Domenica Di Benedetto, and Alessandro Borri. 2019. Symbolic control design of nonlinear systems with outputs. Automatica 109(2019), 108511. · Zbl 1429.93151 |
| [28] | J.H. Reif. 1984. The complexity of two-player games of incomplete information. J. Computer and System Sciences 29 (1984), 274-301. · Zbl 0551.90100 |
| [29] | G. Reissig, A. Weber, and M. Rungger. 2017. Feedback Refinement Relations for the Synthesis of Symbolic Controllers. TAC 62, 4 (2017), 1781-1796. · Zbl 1366.93363 |
| [30] | M. Rungger and M. Zamani. 2016. SCOTS: A Tool for the Synthesis of Symbolic Controllers. In HSCC. ACM, 99-104. · Zbl 1364.93267 |
| [31] | Sven Schewe and Bernd Finkbeiner. 2007. Bounded synthesis. In International Symposium on Automated Technology for Verification and Analysis. Springer, 474-488. · Zbl 1141.68491 |
| [32] | Leander Tentrup. 2019. CAQE and QuAbS: Abstraction Based QBF Solvers. J. Satisf. Boolean Model. Comput. 11, 1 (2019), 155-210. https://doi.org/10.3233/SAT190121 · Zbl 1484.68224 |
| [33] | W. Thomas. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, J. van Leeuwen (Ed.). Vol. B. Elsevier, 133-191. · Zbl 0900.68316 |
| [34] | W. Thomas. 1995. On the Synthesis of Strategies in Infinite Games. In STACS’95(Lecture Notes in Computer Science, Vol. 900). Springer-Verlag, 1-13. · Zbl 1379.68233 |
| [35] | Clifford Wolf. 2013. Yosys Open Synthesis Suite. Retrieved March 14, 2022 from https://yosyshq.net/yosys/ |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
