[{"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-030-29662-9_8","citation":{"apa":"Kong, H., Bartocci, E., Jiang, Y., &#38; Henzinger, T. A. (2019). Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>","ama":"Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:123-141. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>","short":"H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.","mla":"Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">10.1007/978-3-030-29662-9_8</a>.","ieee":"H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 123–141.","ista":"Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11750, 123–141.","chicago":"Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:123–41. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_8\">https://doi.org/10.1007/978-3-030-29662-9_8</a>."},"title":"Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems","end_date":"2019-08-29","start_date":"2019-08-27","location":"Amsterdam, The Netherlands"},"day":"13","type":"conference","author":[{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong"},{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"full_name":"Jiang, Yu","first_name":"Yu","last_name":"Jiang"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"alternative_title":["LNCS"],"publisher":"Springer Nature","isi":1,"publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","department":[{"_id":"ToHe"}],"quality_controlled":"1","intvolume":"     11750","status":"public","page":"123-141","month":"08","date_created":"2020-01-05T23:00:47Z","scopus_import":"1","external_id":{"arxiv":["1907.11514"],"isi":["000611677700008"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2023-09-06T14:55:15Z","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-0302-9661-2"],"eissn":["1611-3349"]},"year":"2019","oa_version":"Preprint","publication_status":"published","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1907.11514"}],"oa":1,"volume":11750,"arxiv":1,"article_processing_charge":"No","abstract":[{"lang":"eng","text":"Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature."}],"_id":"7231","date_published":"2019-08-13T00:00:00Z"},{"publication_identifier":{"isbn":["978-3-0302-9661-2"],"issn":["0302-9743"],"eissn":["1611-3349"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2023-09-06T14:57:17Z","external_id":{"isi":["000611677700004"]},"scopus_import":"1","oa_version":"None","year":"2019","publication_status":"published","volume":11750,"article_processing_charge":"No","abstract":[{"text":"We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. ","lang":"eng"}],"_id":"7232","date_published":"2019-08-13T00:00:00Z","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"doi":"10.1007/978-3-030-29662-9_4","language":[{"iso":"eng"}],"conference":{"name":"FORMATS: Formal Modeling and Anaysis of Timed Systems","start_date":"2019-08-27","end_date":"2019-08-29","location":"Amsterdam, The Netherlands"},"title":"Mixed-time signal temporal logic","citation":{"mla":"Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 59–75, doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>.","chicago":"Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal Logic.” In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, 11750:59–75. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>.","ieee":"T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,” in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.","ista":"Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.","ama":"Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature; 2019:59-75. doi:<a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">10.1007/978-3-030-29662-9_4</a>","apa":"Ferrere, T., Maler, O., &#38; Nickovic, D. (2019). Mixed-time signal temporal logic. In <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i> (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-29662-9_4\">https://doi.org/10.1007/978-3-030-29662-9_4</a>","short":"T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75."},"alternative_title":["LNCS"],"author":[{"last_name":"Ferrere","full_name":"Ferrere, Thomas","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143"},{"full_name":"Maler, Oded","first_name":"Oded","last_name":"Maler"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","day":"13","isi":1,"publisher":"Springer Nature","intvolume":"     11750","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"}],"publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","page":"59-75","date_created":"2020-01-05T23:00:48Z","month":"08"}]