[{"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","file_date_updated":"2020-07-14T12:47:43Z","publication_status":"published","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2019-09-18T08:06:58Z","alternative_title":["LIPIcs"],"title":"Determinacy in discrete-bidding infinite-duration games","intvolume":"       140","_id":"6886","scopus_import":"1","author":[{"last_name":"Aghajohari","first_name":"Milad","full_name":"Aghajohari, Milad"},{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"volume":140,"ddc":["000"],"doi":"10.4230/LIPICS.CONCUR.2019.20","arxiv":1,"day":"01","abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets. ","lang":"eng"}],"date_updated":"2022-01-26T08:27:10Z","year":"2019","citation":{"mla":"Aghajohari, Milad, et al. <i>Determinacy in Discrete-Bidding Infinite-Duration Games</i>. Vol. 140, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">10.4230/LIPICS.CONCUR.2019.20</a>.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","ista":"Aghajohari M, Avni G, Henzinger TA. 2019. Determinacy in discrete-bidding infinite-duration games. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 20.","ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">10.4230/LIPICS.CONCUR.2019.20</a>","apa":"Aghajohari, M., Avni, G., &#38; Henzinger, T. A. (2019). Determinacy in discrete-bidding infinite-duration games (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">https://doi.org/10.4230/LIPICS.CONCUR.2019.20</a>","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">https://doi.org/10.4230/LIPICS.CONCUR.2019.20</a>."},"external_id":{"arxiv":["1905.03588"]},"conference":{"location":"Amsterdam, Netherlands","end_date":"2019-08-30","start_date":"2019-08-27","name":"CONCUR: International Conference on Concurrency Theory"},"language":[{"iso":"eng"}],"oa_version":"Published Version","project":[{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory"}],"month":"08","article_number":"20","has_accepted_license":"1","file":[{"file_id":"6915","creator":"kschuh","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:47:43Z","file_name":"2019_LIPIcs_Aghajohari.pdf","content_type":"application/pdf","date_created":"2019-09-27T12:21:38Z","checksum":"4df6d3575c506edb17215adada03cc8e","file_size":741425}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","oa":1,"tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","short":"CC BY (3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"date_published":"2019-08-01T00:00:00Z","type":"conference"},{"quality_controlled":"1","file_date_updated":"2020-10-08T17:30:38Z","publisher":"IEEE","scopus_import":"1","_id":"6888","author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"first_name":"Ramin","last_name":"Hasani","full_name":"Hasani, Ramin"},{"last_name":"Zimmer","first_name":"Manuel","full_name":"Zimmer, Manuel"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"}],"date_created":"2019-09-18T08:09:51Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","alternative_title":["ICRA"],"title":"Designing worm-inspired neural networks for interpretable robotic control","volume":"2019-May","ddc":["000"],"citation":{"apa":"Lechner, M., Hasani, R., Zimmer, M., Henzinger, T. A., &#38; Grosu, R. (2019). Designing worm-inspired neural networks for interpretable robotic control. In <i>Proceedings - IEEE International Conference on Robotics and Automation</i> (Vol. 2019–May). Montreal, QC, Canada: IEEE. <a href=\"https://doi.org/10.1109/icra.2019.8793840\">https://doi.org/10.1109/icra.2019.8793840</a>","ama":"Lechner M, Hasani R, Zimmer M, Henzinger TA, Grosu R. Designing worm-inspired neural networks for interpretable robotic control. In: <i>Proceedings - IEEE International Conference on Robotics and Automation</i>. Vol 2019-May. IEEE; 2019. doi:<a href=\"https://doi.org/10.1109/icra.2019.8793840\">10.1109/icra.2019.8793840</a>","chicago":"Lechner, Mathias, Ramin Hasani, Manuel Zimmer, Thomas A Henzinger, and Radu Grosu. “Designing Worm-Inspired Neural Networks for Interpretable Robotic Control.” In <i>Proceedings - IEEE International Conference on Robotics and Automation</i>, Vol. 2019–May. IEEE, 2019. <a href=\"https://doi.org/10.1109/icra.2019.8793840\">https://doi.org/10.1109/icra.2019.8793840</a>.","ieee":"M. Lechner, R. Hasani, M. Zimmer, T. A. Henzinger, and R. Grosu, “Designing worm-inspired neural networks for interpretable robotic control,” in <i>Proceedings - IEEE International Conference on Robotics and Automation</i>, Montreal, QC, Canada, 2019, vol. 2019–May.","mla":"Lechner, Mathias, et al. “Designing Worm-Inspired Neural Networks for Interpretable Robotic Control.” <i>Proceedings - IEEE International Conference on Robotics and Automation</i>, vol. 2019–May, 8793840, IEEE, 2019, doi:<a href=\"https://doi.org/10.1109/icra.2019.8793840\">10.1109/icra.2019.8793840</a>.","short":"M. Lechner, R. Hasani, M. Zimmer, T.A. Henzinger, R. Grosu, in:, Proceedings - IEEE International Conference on Robotics and Automation, IEEE, 2019.","ista":"Lechner M, Hasani R, Zimmer M, Henzinger TA, Grosu R. 2019. Designing worm-inspired neural networks for interpretable robotic control. Proceedings - IEEE International Conference on Robotics and Automation. ICRA: International Conference on Robotics and Automation, ICRA, vol. 2019–May, 8793840."},"year":"2019","date_updated":"2021-01-12T08:09:28Z","day":"01","doi":"10.1109/icra.2019.8793840","abstract":[{"lang":"eng","text":"In this paper, we design novel liquid time-constant recurrent neural networks for robotic control, inspired by the brain of the nematode, C. elegans. In the worm's nervous system, neurons communicate through nonlinear time-varying synaptic links established amongst them by their particular wiring structure. This property enables neurons to express liquid time-constants dynamics and therefore allows the network to originate complex behaviors with a small number of neurons. We identify neuron-pair communication motifs as design operators and use them to configure compact neuronal network structures to govern sequential robotic tasks. The networks are systematically designed to map the environmental observations to motor actions, by their hierarchical topology from sensory neurons, through recurrently-wired interneurons, to motor neurons. The networks are then parametrized in a supervised-learning scheme by a search-based algorithm. We demonstrate that obtained networks realize interpretable dynamics. We evaluate their performance in controlling mobile and arm robots, and compare their attributes to other artificial neural network-based control agents. Finally, we experimentally show their superior resilience to environmental noise, compared to the existing machine learning-based methods."}],"language":[{"iso":"eng"}],"conference":{"name":"ICRA: International Conference on Robotics and Automation","start_date":"2019-05-20","end_date":"2019-05-24","location":"Montreal, QC, Canada"},"has_accepted_license":"1","publication":"Proceedings - IEEE International Conference on Robotics and Automation","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Submitted Version","article_number":"8793840","month":"05","file":[{"file_name":"2019_ICRA_Lechner.pdf","content_type":"application/pdf","date_updated":"2020-10-08T17:30:38Z","file_size":3265107,"checksum":"f5545a6b60c3ffd01feb3613f81d03b6","date_created":"2020-10-08T17:30:38Z","creator":"dernst","file_id":"8636","access_level":"open_access","success":1,"relation":"main_file"}],"status":"public","user_id":"D865714E-FA4E-11E9-B85B-F5C5E5697425","type":"conference","date_published":"2019-05-01T00:00:00Z","publication_identifier":{"isbn":["9781538660270"]},"oa":1},{"day":"30","degree_awarded":"PhD","doi":"10.15479/AT:ISTA:6894","abstract":[{"lang":"eng","text":"Hybrid automata combine finite automata and dynamical systems, and model the interaction of digital with physical systems. Formal analysis that can guarantee the safety of all behaviors or rigorously witness failures, while unsolvable in general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking, assisted theorem proving.\r\nNevertheless, very few methods have addressed the time-unbounded reachability analysis of hybrid automata and, for current sound and automatic tools, scalability remains critical. We develop methods for the polyhedral abstraction of hybrid automata, which construct coarse overapproximations and tightens them incrementally, in a CEGAR fashion. We use template polyhedra, i.e., polyhedra whose facets are normal to a given set of directions.\r\nWhile, previously, directions were given by the user, we introduce (1) the first method\r\nfor computing template directions from spurious counterexamples, so as to generalize and\r\neliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid\r\nautomata with (possibly non-linear) convex constraints on derivatives only, while for linear\r\nODE requires further abstraction. Specifically, we introduce (2) the conic abstractions,\r\nwhich, partitioning the state space into appropriate (possibly non-uniform) cones, divide\r\ncurvy trajectories into relatively straight sections, suitable for polyhedral abstractions.\r\nFinally, we introduce (3) space-time interpolation, which, combining interval arithmetic\r\nand template refinement, computes appropriate (possibly non-uniform) time partitioning\r\nand template directions along spurious trajectories, so as to eliminate them.\r\nWe obtain sound and automatic methods for the reachability analysis over dense\r\nand unbounded time of convex hybrid automata and hybrid automata with linear ODE.\r\nWe build prototype tools and compare—favorably—our methods against the respective\r\nstate-of-the-art tools, on several benchmarks."}],"citation":{"ieee":"M. Giacobbe, “Automatic time-unbounded reachability analysis of hybrid systems,” Institute of Science and Technology Austria, 2019.","chicago":"Giacobbe, Mirco. “Automatic Time-Unbounded Reachability Analysis of Hybrid Systems.” Institute of Science and Technology Austria, 2019. <a href=\"https://doi.org/10.15479/AT:ISTA:6894\">https://doi.org/10.15479/AT:ISTA:6894</a>.","ama":"Giacobbe M. Automatic time-unbounded reachability analysis of hybrid systems. 2019. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:6894\">10.15479/AT:ISTA:6894</a>","apa":"Giacobbe, M. (2019). <i>Automatic time-unbounded reachability analysis of hybrid systems</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:6894\">https://doi.org/10.15479/AT:ISTA:6894</a>","ista":"Giacobbe M. 2019. Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria.","short":"M. Giacobbe, Automatic Time-Unbounded Reachability Analysis of Hybrid Systems, Institute of Science and Technology Austria, 2019.","mla":"Giacobbe, Mirco. <i>Automatic Time-Unbounded Reachability Analysis of Hybrid Systems</i>. Institute of Science and Technology Austria, 2019, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:6894\">10.15479/AT:ISTA:6894</a>."},"year":"2019","date_updated":"2023-09-19T09:30:43Z","ddc":["000"],"date_created":"2019-09-22T14:08:44Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","title":"Automatic time-unbounded reachability analysis of hybrid systems","alternative_title":["ISTA Thesis"],"_id":"6894","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904"}],"publisher":"Institute of Science and Technology Austria","page":"132","file_date_updated":"2020-07-14T12:47:43Z","publication_identifier":{"eissn":["2663-337X"]},"oa":1,"supervisor":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"dissertation","date_published":"2019-09-30T00:00:00Z","file":[{"file_name":"giacobbe_thesis.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:43Z","checksum":"773beaf4a85dc2acc2c12b578fbe1965","file_size":4100685,"date_created":"2019-09-27T14:15:05Z","creator":"mgiacobbe","file_id":"6916","access_level":"open_access","relation":"main_file"},{"creator":"mgiacobbe","file_id":"6917","relation":"source_file","access_level":"closed","content_type":"application/gzip","file_name":"giacobbe_thesis_src.tar.gz","date_updated":"2020-07-14T12:47:43Z","checksum":"97f1c3da71feefd27e6e625d32b4c75b","file_size":7959732,"date_created":"2019-09-27T14:22:04Z"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"id":"631","relation":"part_of_dissertation","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"647"},{"status":"public","id":"140","relation":"part_of_dissertation"}]},"status":"public","oa_version":"Published Version","month":"09","has_accepted_license":"1","language":[{"iso":"eng"}]},{"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1809.03864"}],"abstract":[{"text":"In this paper, we introduce a novel method to interpret recurrent neural networks (RNNs), particularly long short-term memory networks (LSTMs) at the cellular level. We propose a systematic pipeline for interpreting individual hidden state dynamics within the network using response characterization methods. The ranked contribution of individual cells to the network's output is computed by analyzing a set of interpretable metrics of their decoupled step and sinusoidal responses. As a result, our method is able to uniquely identify neurons with insightful dynamics, quantify relationships between dynamical properties and test accuracy through ablation analysis, and interpret the impact of network capacity on a network's dynamical distribution. Finally, we demonstrate the generalizability and scalability of our method by evaluating a series of different benchmark sequential datasets.","lang":"eng"}],"oa":1,"arxiv":1,"doi":"10.1109/ijcnn.2019.8851954","publication_identifier":{"isbn":["9781728119854"]},"day":"30","date_published":"2019-09-30T00:00:00Z","type":"conference","external_id":{"arxiv":["1809.03864"]},"date_updated":"2021-01-12T08:11:19Z","year":"2019","citation":{"ista":"Hasani R, Amini A, Lechner M, Naser F, Grosu R, Rus D. 2019. Response characterization for auditing cell dynamics in long short-term memory networks. Proceedings of the International Joint Conference on Neural Networks. IJCNN: International Joint Conference on Neural Networks, 8851954.","short":"R. Hasani, A. Amini, M. Lechner, F. Naser, R. Grosu, D. Rus, in:, Proceedings of the International Joint Conference on Neural Networks, IEEE, 2019.","mla":"Hasani, Ramin, et al. “Response Characterization for Auditing Cell Dynamics in Long Short-Term Memory Networks.” <i>Proceedings of the International Joint Conference on Neural Networks</i>, 8851954, IEEE, 2019, doi:<a href=\"https://doi.org/10.1109/ijcnn.2019.8851954\">10.1109/ijcnn.2019.8851954</a>.","ieee":"R. Hasani, A. Amini, M. Lechner, F. Naser, R. Grosu, and D. Rus, “Response characterization for auditing cell dynamics in long short-term memory networks,” in <i>Proceedings of the International Joint Conference on Neural Networks</i>, Budapest, Hungary, 2019.","chicago":"Hasani, Ramin, Alexander Amini, Mathias Lechner, Felix Naser, Radu Grosu, and Daniela Rus. “Response Characterization for Auditing Cell Dynamics in Long Short-Term Memory Networks.” In <i>Proceedings of the International Joint Conference on Neural Networks</i>. IEEE, 2019. <a href=\"https://doi.org/10.1109/ijcnn.2019.8851954\">https://doi.org/10.1109/ijcnn.2019.8851954</a>.","ama":"Hasani R, Amini A, Lechner M, Naser F, Grosu R, Rus D. Response characterization for auditing cell dynamics in long short-term memory networks. In: <i>Proceedings of the International Joint Conference on Neural Networks</i>. IEEE; 2019. doi:<a href=\"https://doi.org/10.1109/ijcnn.2019.8851954\">10.1109/ijcnn.2019.8851954</a>","apa":"Hasani, R., Amini, A., Lechner, M., Naser, F., Grosu, R., &#38; Rus, D. (2019). Response characterization for auditing cell dynamics in long short-term memory networks. In <i>Proceedings of the International Joint Conference on Neural Networks</i>. Budapest, Hungary: IEEE. <a href=\"https://doi.org/10.1109/ijcnn.2019.8851954\">https://doi.org/10.1109/ijcnn.2019.8851954</a>"},"conference":{"end_date":"2019-07-19","location":"Budapest, Hungary","start_date":"2019-07-14","name":"IJCNN: International Joint Conference on Neural Networks"},"publisher":"IEEE","language":[{"iso":"eng"}],"quality_controlled":"1","title":"Response characterization for auditing cell dynamics in long short-term memory networks","month":"09","article_number":"8851954","oa_version":"Preprint","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2019-11-04T15:59:58Z","author":[{"last_name":"Hasani","first_name":"Ramin","full_name":"Hasani, Ramin"},{"first_name":"Alexander","last_name":"Amini","full_name":"Amini, Alexander"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","first_name":"Mathias","last_name":"Lechner"},{"last_name":"Naser","first_name":"Felix","full_name":"Naser, Felix"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"},{"full_name":"Rus, Daniela","last_name":"Rus","first_name":"Daniela"}],"_id":"6985","publication":"Proceedings of the International Joint Conference on Neural Networks","scopus_import":1},{"publication":"Journal of the ACM","article_number":"19","month":"05","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa_version":"None","language":[{"iso":"eng"}],"type":"journal_article","date_published":"2019-05-01T00:00:00Z","publication_identifier":{"issn":["0004-5411"]},"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","issue":"3","author":[{"last_name":"Ferrere","first_name":"Thomas","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"last_name":"Ničković","first_name":"Dejan","full_name":"Ničković, Dejan"},{"full_name":"Pnueli, Amir","first_name":"Amir","last_name":"Pnueli"}],"scopus_import":"1","_id":"7109","intvolume":"        66","title":"From real-time logic to timed automata","date_created":"2019-11-26T10:22:32Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","quality_controlled":"1","article_type":"original","publisher":"ACM","external_id":{"isi":["000495406300005"]},"isi":1,"citation":{"apa":"Ferrere, T., Maler, O., Ničković, D., &#38; Pnueli, A. (2019). From real-time logic to timed automata. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3286976\">https://doi.org/10.1145/3286976</a>","ama":"Ferrere T, Maler O, Ničković D, Pnueli A. From real-time logic to timed automata. <i>Journal of the ACM</i>. 2019;66(3). doi:<a href=\"https://doi.org/10.1145/3286976\">10.1145/3286976</a>","chicago":"Ferrere, Thomas, Oded Maler, Dejan Ničković, and Amir Pnueli. “From Real-Time Logic to Timed Automata.” <i>Journal of the ACM</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3286976\">https://doi.org/10.1145/3286976</a>.","ieee":"T. Ferrere, O. Maler, D. Ničković, and A. Pnueli, “From real-time logic to timed automata,” <i>Journal of the ACM</i>, vol. 66, no. 3. ACM, 2019.","short":"T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019).","mla":"Ferrere, Thomas, et al. “From Real-Time Logic to Timed Automata.” <i>Journal of the ACM</i>, vol. 66, no. 3, 19, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3286976\">10.1145/3286976</a>.","ista":"Ferrere T, Maler O, Ničković D, Pnueli A. 2019. From real-time logic to timed automata. Journal of the ACM. 66(3), 19."},"year":"2019","date_updated":"2023-09-06T11:11:56Z","abstract":[{"lang":"eng","text":"We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended."}],"day":"01","doi":"10.1145/3286976","volume":66},{"date_created":"2019-12-04T16:07:50Z","article_processing_charge":"No","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"publication_status":"published","intvolume":"     11773","alternative_title":["LNCS"],"title":"Transient memory in gene regulation","scopus_import":"1","_id":"7147","author":[{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","first_name":"Calin C","last_name":"Guet","orcid":"0000-0001-6220-2052","full_name":"Guet, Calin C"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"id":"46613666-F248-11E8-B48F-1D18A9856A87","full_name":"Igler, Claudia","first_name":"Claudia","last_name":"Igler"},{"full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","last_name":"Petrov","first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali","first_name":"Ali","last_name":"Sezgin"}],"publisher":"Springer Nature","quality_controlled":"1","page":"155-187","day":"17","doi":"10.1007/978-3-030-31304-3_9","abstract":[{"lang":"eng","text":"The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets.\r\n\r\nIn this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest.\r\n\r\nThe behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions."}],"year":"2019","citation":{"ista":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. 2019. Transient memory in gene regulation. 17th International Conference on Computational Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNCS, vol. 11773, 155–187.","mla":"Guet, Calin C., et al. “Transient Memory in Gene Regulation.” <i>17th International Conference on Computational Methods in Systems Biology</i>, vol. 11773, Springer Nature, 2019, pp. 155–87, doi:<a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">10.1007/978-3-030-31304-3_9</a>.","short":"C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International Conference on Computational Methods in Systems Biology, Springer Nature, 2019, pp. 155–187.","ieee":"C. C. Guet, T. A. Henzinger, C. Igler, T. Petrov, and A. Sezgin, “Transient memory in gene regulation,” in <i>17th International Conference on Computational Methods in Systems Biology</i>, Trieste, Italy, 2019, vol. 11773, pp. 155–187.","chicago":"Guet, Calin C, Thomas A Henzinger, Claudia Igler, Tatjana Petrov, and Ali Sezgin. “Transient Memory in Gene Regulation.” In <i>17th International Conference on Computational Methods in Systems Biology</i>, 11773:155–87. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">https://doi.org/10.1007/978-3-030-31304-3_9</a>.","ama":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. Transient memory in gene regulation. In: <i>17th International Conference on Computational Methods in Systems Biology</i>. Vol 11773. Springer Nature; 2019:155-187. doi:<a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">10.1007/978-3-030-31304-3_9</a>","apa":"Guet, C. C., Henzinger, T. A., Igler, C., Petrov, T., &#38; Sezgin, A. (2019). Transient memory in gene regulation. In <i>17th International Conference on Computational Methods in Systems Biology</i> (Vol. 11773, pp. 155–187). Trieste, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-31304-3_9\">https://doi.org/10.1007/978-3-030-31304-3_9</a>"},"date_updated":"2023-09-06T11:18:08Z","external_id":{"isi":["000557875100009"]},"isi":1,"volume":11773,"project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"251EE76E-B435-11E9-9278-68D0E5697425","grant_number":"24573","name":"Design principles underlying genetic switch architecture"}],"oa_version":"None","month":"09","publication":"17th International Conference on Computational Methods in Systems Biology","conference":{"end_date":"2019-09-20","location":"Trieste, Italy","name":"CMSB: Computational Methods in Systems Biology","start_date":"2019-09-18"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783030313036","9783030313043"],"issn":["0302-9743"],"eissn":["1611-3349"]},"type":"conference","date_published":"2019-09-17T00:00:00Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public"},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030320782","9783030320799"]},"type":"conference","date_published":"2019-10-01T00:00:00Z","conference":{"name":"RV: Runtime Verification","start_date":"2019-10-08","end_date":"2019-10-11","location":"Porto, Portugal"},"language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering"}],"oa_version":"None","month":"10","publication":"19th International Conference on Runtime Verification","volume":11757,"day":"01","doi":"10.1007/978-3-030-32079-9_17","abstract":[{"lang":"eng","text":"Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. "}],"year":"2019","citation":{"mla":"Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal Features.” <i>19th International Conference on Runtime Verification</i>, vol. 11757, Springer Nature, 2019, pp. 292–309, doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>.","short":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309.","ista":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. 2019. Shape expressions for specifying and extracting signal features. 19th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 11757, 292–309.","apa":"Ničković, D., Qin, X., Ferrere, T., Mateis, C., &#38; Deshmukh, J. (2019). Shape expressions for specifying and extracting signal features. In <i>19th International Conference on Runtime Verification</i> (Vol. 11757, pp. 292–309). Porto, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>","ama":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for specifying and extracting signal features. In: <i>19th International Conference on Runtime Verification</i>. Vol 11757. Springer Nature; 2019:292-309. doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>","ieee":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions for specifying and extracting signal features,” in <i>19th International Conference on Runtime Verification</i>, Porto, Portugal, 2019, vol. 11757, pp. 292–309.","chicago":"Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In <i>19th International Conference on Runtime Verification</i>, 11757:292–309. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>."},"date_updated":"2023-09-06T11:24:10Z","external_id":{"isi":["000570006300017"]},"isi":1,"publisher":"Springer Nature","quality_controlled":"1","page":"292-309","article_processing_charge":"No","date_created":"2019-12-09T08:47:55Z","department":[{"_id":"ToHe"}],"publication_status":"published","intvolume":"     11757","alternative_title":["LNCS"],"title":"Shape expressions for specifying and extracting signal features","scopus_import":"1","_id":"7159","author":[{"full_name":"Ničković, Dejan","first_name":"Dejan","last_name":"Ničković"},{"last_name":"Qin","first_name":"Xin","full_name":"Qin, Xin"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Ferrere","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas"},{"last_name":"Mateis","first_name":"Cristinel","full_name":"Mateis, Cristinel"},{"full_name":"Deshmukh, Jyotirmoy","first_name":"Jyotirmoy","last_name":"Deshmukh"}]},{"doi":"10.1007/978-3-030-29662-9_8","arxiv":1,"day":"13","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."}],"date_updated":"2023-09-06T14:55:15Z","year":"2019","citation":{"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>.","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.","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>","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>.","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."},"isi":1,"external_id":{"isi":["000611677700008"],"arxiv":["1907.11514"]},"volume":11750,"publication_status":"published","date_created":"2020-01-05T23:00:47Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","title":"Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty","alternative_title":["LNCS"],"intvolume":"     11750","_id":"7231","scopus_import":"1","author":[{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer Nature","page":"123-141","quality_controlled":"1","publication_identifier":{"isbn":["978-3-0302-9661-2"],"eissn":["1611-3349"],"issn":["0302-9743"]},"oa":1,"date_published":"2019-08-13T00:00:00Z","type":"conference","main_file_link":[{"url":"https://arxiv.org/abs/1907.11514","open_access":"1"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Preprint","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"month":"08","publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems","start_date":"2019-08-27","end_date":"2019-08-29","location":"Amsterdam, The Netherlands"},"language":[{"iso":"eng"}]},{"publisher":"Springer Nature","page":"59-75","quality_controlled":"1","title":"Mixed-time signal temporal logic","alternative_title":["LNCS"],"intvolume":"     11750","publication_status":"published","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2020-01-05T23:00:48Z","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Ferrere","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan"}],"_id":"7232","scopus_import":"1","volume":11750,"abstract":[{"lang":"eng","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. "}],"doi":"10.1007/978-3-030-29662-9_4","day":"13","isi":1,"external_id":{"isi":["000611677700004"]},"date_updated":"2023-09-06T14:57:17Z","year":"2019","citation":{"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.","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>.","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.","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>","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>","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."},"conference":{"start_date":"2019-08-27","name":"FORMATS: Formal Modeling and Anaysis of Timed Systems","end_date":"2019-08-29","location":"Amsterdam, The Netherlands"},"language":[{"iso":"eng"}],"month":"08","oa_version":"None","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"publication":"17th International Conference on Formal Modeling and Analysis of Timed Systems","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["978-3-0302-9661-2"]},"date_published":"2019-08-13T00:00:00Z","type":"conference"},{"author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Larsen, Kim G.","first_name":"Kim G.","last_name":"Larsen"},{"full_name":"Mikučionis, Marius","last_name":"Mikučionis","first_name":"Marius"}],"scopus_import":"1","_id":"7453","intvolume":"     10000","alternative_title":["Lecture Notes in Computer Science"],"title":"Continuous-time models for system design and analysis","article_processing_charge":"No","date_created":"2020-02-05T10:51:44Z","department":[{"_id":"ToHe"}],"publication_status":"published","quality_controlled":"1","series_title":"LNCS","page":"452-477","editor":[{"first_name":"Bernhard","last_name":"Steffen","full_name":"Steffen, Bernhard"},{"first_name":"Gerhard","last_name":"Woeginger","full_name":"Woeginger, Gerhard"}],"publisher":"Springer Nature","citation":{"ieee":"R. Alur, M. Giacobbe, T. A. Henzinger, K. G. Larsen, and M. Mikučionis, “Continuous-time models for system design and analysis,” in <i>Computing and Software Science</i>, vol. 10000, B. Steffen and G. Woeginger, Eds. Springer Nature, 2019, pp. 452–477.","chicago":"Alur, Rajeev, Mirco Giacobbe, Thomas A Henzinger, Kim G. Larsen, and Marius Mikučionis. “Continuous-Time Models for System Design and Analysis.” In <i>Computing and Software Science</i>, edited by Bernhard Steffen and Gerhard Woeginger, 10000:452–77. LNCS. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">https://doi.org/10.1007/978-3-319-91908-9_22</a>.","apa":"Alur, R., Giacobbe, M., Henzinger, T. A., Larsen, K. G., &#38; Mikučionis, M. (2019). Continuous-time models for system design and analysis. In B. Steffen &#38; G. Woeginger (Eds.), <i>Computing and Software Science</i> (Vol. 10000, pp. 452–477). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">https://doi.org/10.1007/978-3-319-91908-9_22</a>","ama":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. Continuous-time models for system design and analysis. In: Steffen B, Woeginger G, eds. <i>Computing and Software Science</i>. Vol 10000. LNCS. Springer Nature; 2019:452-477. doi:<a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">10.1007/978-3-319-91908-9_22</a>","ista":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. 2019.Continuous-time models for system design and analysis. In: Computing and Software Science. Lecture Notes in Computer Science, vol. 10000, 452–477.","mla":"Alur, Rajeev, et al. “Continuous-Time Models for System Design and Analysis.” <i>Computing and Software Science</i>, edited by Bernhard Steffen and Gerhard Woeginger, vol. 10000, Springer Nature, 2019, pp. 452–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">10.1007/978-3-319-91908-9_22</a>.","short":"R. Alur, M. Giacobbe, T.A. Henzinger, K.G. Larsen, M. Mikučionis, in:, B. Steffen, G. Woeginger (Eds.), Computing and Software Science, Springer Nature, 2019, pp. 452–477."},"year":"2019","date_updated":"2022-09-06T08:25:52Z","abstract":[{"lang":"eng","text":"We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement."}],"day":"05","doi":"10.1007/978-3-319-91908-9_22","volume":10000,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award). This research has received funding from the Sino-Danish Basic Research Centre, IDEA4CPS, funded by the Danish National Research Foundation and the National Science Foundation, China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant LASSO.","publication":"Computing and Software Science","month":"10","project":[{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"type":"book_chapter","date_published":"2019-10-05T00:00:00Z","oa":1,"publication_identifier":{"isbn":["9783319919072"],"issn":["1611-3349"],"eissn":["0302-9743"],"eisbn":["9783319919089"]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-319-91908-9_22"}]},{"file":[{"file_id":"7617","creator":"dernst","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:48:00Z","file_name":"2019_ARCH19_Immler.pdf","content_type":"application/pdf","date_created":"2020-03-24T07:36:36Z","file_size":1934830,"checksum":"9138977a06fcd6a95976eb4bca875f0c"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"eissn":["23987340"]},"oa":1,"type":"conference","date_published":"2019-05-25T00:00:00Z","conference":{"location":"Montreal, Canada","end_date":"2019-04-15","start_date":"2019-04-15","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems"},"language":[{"iso":"eng"}],"oa_version":"Published Version","month":"05","has_accepted_license":"1","publication":"EPiC Series in Computing","volume":61,"ddc":["000"],"day":"25","doi":"10.29007/m75b","abstract":[{"text":"We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In this year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. They are applied to solve reachability analysis problems on four benchmark problems, one of them with hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.","lang":"eng"}],"citation":{"short":"F. Immler, M. Althoff, L. Benet, A. Chapoutot, X. Chen, M. Forets, L. Geretti, N. Kochdumper, D.P. Sanders, C. Schilling, in:, EPiC Series in Computing, EasyChair Publications, 2019, pp. 41–61.","mla":"Immler, Fabian, et al. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” <i>EPiC Series in Computing</i>, vol. 61, EasyChair Publications, 2019, pp. 41–61, doi:<a href=\"https://doi.org/10.29007/m75b\">10.29007/m75b</a>.","ista":"Immler F, Althoff M, Benet L, Chapoutot A, Chen X, Forets M, Geretti L, Kochdumper N, Sanders DP, Schilling C. 2019. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 61, 41–61.","apa":"Immler, F., Althoff, M., Benet, L., Chapoutot, A., Chen, X., Forets, M., … Schilling, C. (2019). ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In <i>EPiC Series in Computing</i> (Vol. 61, pp. 41–61). Montreal, Canada: EasyChair Publications. <a href=\"https://doi.org/10.29007/m75b\">https://doi.org/10.29007/m75b</a>","ama":"Immler F, Althoff M, Benet L, et al. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In: <i>EPiC Series in Computing</i>. Vol 61. EasyChair Publications; 2019:41-61. doi:<a href=\"https://doi.org/10.29007/m75b\">10.29007/m75b</a>","ieee":"F. Immler <i>et al.</i>, “ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics,” in <i>EPiC Series in Computing</i>, Montreal, Canada, 2019, vol. 61, pp. 41–61.","chicago":"Immler, Fabian, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders, and Christian Schilling. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” In <i>EPiC Series in Computing</i>, 61:41–61. EasyChair Publications, 2019. <a href=\"https://doi.org/10.29007/m75b\">https://doi.org/10.29007/m75b</a>."},"year":"2019","date_updated":"2021-01-12T08:14:17Z","publisher":"EasyChair Publications","quality_controlled":"1","page":"41-61","file_date_updated":"2020-07-14T12:48:00Z","date_created":"2020-03-08T23:00:49Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","intvolume":"        61","title":"ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics","scopus_import":1,"_id":"7576","author":[{"first_name":"Fabian","last_name":"Immler","full_name":"Immler, Fabian"},{"first_name":"Matthias","last_name":"Althoff","full_name":"Althoff, Matthias"},{"full_name":"Benet, Luis","first_name":"Luis","last_name":"Benet"},{"first_name":"Alexandre","last_name":"Chapoutot","full_name":"Chapoutot, Alexandre"},{"last_name":"Chen","first_name":"Xin","full_name":"Chen, Xin"},{"full_name":"Forets, Marcelo","first_name":"Marcelo","last_name":"Forets"},{"full_name":"Geretti, Luca","first_name":"Luca","last_name":"Geretti"},{"full_name":"Kochdumper, Niklas","first_name":"Niklas","last_name":"Kochdumper"},{"full_name":"Sanders, David P.","last_name":"Sanders","first_name":"David P."},{"last_name":"Schilling","first_name":"Christian","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}]},{"ddc":["000"],"volume":22,"external_id":{"arxiv":["1901.10736"],"isi":["000516713900005"]},"isi":1,"year":"2019","citation":{"ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. JuliaReach: A toolbox for set-based reachability. In: <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>. Vol 22. ACM; 2019:39-44. doi:<a href=\"https://doi.org/10.1145/3302504.3311804\">10.1145/3302504.3311804</a>","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., &#38; Schilling, C. (2019). JuliaReach: A toolbox for set-based reachability. In <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i> (Vol. 22, pp. 39–44). Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/3302504.3311804\">https://doi.org/10.1145/3302504.3311804</a>","ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach: A toolbox for set-based reachability,” in <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>, Montreal, QC, Canada, 2019, vol. 22, pp. 39–44.","chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “JuliaReach: A Toolbox for Set-Based Reachability.” In <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>, 22:39–44. ACM, 2019. <a href=\"https://doi.org/10.1145/3302504.3311804\">https://doi.org/10.1145/3302504.3311804</a>.","mla":"Bogomolov, Sergiy, et al. “JuliaReach: A Toolbox for Set-Based Reachability.” <i>Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control</i>, vol. 22, ACM, 2019, pp. 39–44, doi:<a href=\"https://doi.org/10.1145/3302504.3311804\">10.1145/3302504.3311804</a>.","short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 39–44.","ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2019. JuliaReach: A toolbox for set-based reachability. Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and Control vol. 22, 39–44."},"date_updated":"2023-08-24T14:47:21Z","abstract":[{"lang":"eng","text":"We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems."}],"day":"16","doi":"10.1145/3302504.3311804","arxiv":1,"file_date_updated":"2020-07-14T12:47:17Z","ec_funded":1,"quality_controlled":"1","page":"39-44","publisher":"ACM","author":[{"last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Forets, Marcelo","first_name":"Marcelo","last_name":"Forets"},{"last_name":"Frehse","first_name":"Goran","full_name":"Frehse, Goran"},{"first_name":"Kostiantyn","last_name":"Potomkin","full_name":"Potomkin, Kostiantyn"},{"first_name":"Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","_id":"6035","intvolume":"        22","title":"JuliaReach: A toolbox for set-based reachability","date_created":"2019-02-18T14:43:28Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"creator":"cschilli","file_id":"6067","access_level":"open_access","relation":"main_file","file_name":"hscc19.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:17Z","checksum":"28ed56439aea5991c3122d4730fd828f","file_size":3784414,"date_created":"2019-03-05T09:27:18Z"}],"type":"conference","date_published":"2019-04-16T00:00:00Z","oa":1,"publication_identifier":{"isbn":["9781450362825"]},"keyword":["reachability analysis","hybrid systems","lazy computation"],"language":[{"iso":"eng"}],"conference":{"location":"Montreal, QC, Canada","end_date":"2019-04-18","start_date":"2019-04-16","name":"HSCC: Hybrid Systems Computation and Control"},"has_accepted_license":"1","publication":"Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control","month":"04","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"oa_version":"Submitted Version"},{"year":"2019","citation":{"chicago":"Christakis, Maria, Matthias Heizmann, Muhammad Numair Mansur, Christian Schilling, and Valentin Wüstholz. “Semantic Fault Localization and Suspiciousness Ranking.” In <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, 11427:226–43. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">https://doi.org/10.1007/978-3-030-17462-0_13</a>.","ieee":"M. Christakis, M. Heizmann, M. N. Mansur, C. Schilling, and V. Wüstholz, “Semantic fault localization and suspiciousness ranking,” in <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, Prague, Czech Republic, 2019, vol. 11427, pp. 226–243.","apa":"Christakis, M., Heizmann, M., Mansur, M. N., Schilling, C., &#38; Wüstholz, V. (2019). Semantic fault localization and suspiciousness ranking. In <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i> (Vol. 11427, pp. 226–243). Prague, Czech Republic: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">https://doi.org/10.1007/978-3-030-17462-0_13</a>","ama":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. Semantic fault localization and suspiciousness ranking. In: <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 11427. Springer Nature; 2019:226-243. doi:<a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">10.1007/978-3-030-17462-0_13</a>","ista":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. 2019. Semantic fault localization and suspiciousness ranking. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 11427, 226–243.","short":"M. Christakis, M. Heizmann, M.N. Mansur, C. Schilling, V. Wüstholz, in:, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2019, pp. 226–243.","mla":"Christakis, Maria, et al. “Semantic Fault Localization and Suspiciousness Ranking.” <i>25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems </i>, vol. 11427, Springer Nature, 2019, pp. 226–43, doi:<a href=\"https://doi.org/10.1007/978-3-030-17462-0_13\">10.1007/978-3-030-17462-0_13</a>."},"date_updated":"2023-08-24T14:47:45Z","external_id":{"isi":["000681166500013"]},"isi":1,"day":"04","doi":"10.1007/978-3-030-17462-0_13","abstract":[{"text":"Static program analyzers are increasingly effective in checking correctness properties of programs and reporting any errors found, often in the form of error traces. However, developers still spend a significant amount of time on debugging. This involves processing long error traces in an effort to localize a bug to a relatively small part of the program and to identify its cause. In this paper, we present a technique for automated fault localization that, given a program and an error trace, efficiently narrows down the cause of the error to a few statements. These statements are then ranked in terms of their suspiciousness. Our technique relies only on the semantics of the given program and does not require any test cases or user guidance. In experiments on a set of C benchmarks, we show that our technique is effective in quickly isolating the cause of error while out-performing other state-of-the-art fault-localization techniques.","lang":"eng"}],"volume":11427,"ddc":["000"],"scopus_import":"1","_id":"6042","author":[{"full_name":"Christakis, Maria","last_name":"Christakis","first_name":"Maria"},{"full_name":"Heizmann, Matthias","first_name":"Matthias","last_name":"Heizmann"},{"last_name":"Mansur","first_name":"Muhammad Numair","full_name":"Mansur, Muhammad Numair"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"},{"last_name":"Wüstholz","first_name":"Valentin","full_name":"Wüstholz, Valentin"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2019-02-18T16:44:06Z","publication_status":"published","intvolume":"     11427","alternative_title":["LNCS"],"title":"Semantic fault localization and suspiciousness ranking","ec_funded":1,"quality_controlled":"1","page":"226-243","file_date_updated":"2020-07-14T12:47:17Z","publisher":"Springer Nature","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2019-04-04T00:00:00Z","oa":1,"file":[{"date_updated":"2020-07-14T12:47:17Z","content_type":"application/pdf","file_name":"2019_LNCS_Christakis.pdf","date_created":"2019-05-10T14:16:05Z","file_size":773083,"checksum":"9998496f6fe202c0a19124b4209154c6","file_id":"6408","creator":"dernst","access_level":"open_access","relation":"main_file"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","has_accepted_license":"1","publication":"25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"oa_version":"Published Version","month":"04","language":[{"iso":"eng"}],"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2019-04-06","location":"Prague, Czech Republic","end_date":"2019-04-11"}},{"isi":1,"external_id":{"isi":["000516713900007"]},"date_updated":"2023-08-25T10:19:23Z","year":"2019","citation":{"chicago":"Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James Kapinski. “Interface-Aware Signal Temporal Logic.” In <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, 57–66. ACM, 2019. <a href=\"https://doi.org/10.1145/3302504.3311800\">https://doi.org/10.1145/3302504.3311800</a>.","ieee":"T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware signal temporal logic,” in <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, Montreal, Canada, 2019, pp. 57–66.","apa":"Ferrere, T., Nickovic, D., Donzé, A., Ito, H., &#38; Kapinski, J. (2019). Interface-aware signal temporal logic. In <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i> (pp. 57–66). Montreal, Canada: ACM. <a href=\"https://doi.org/10.1145/3302504.3311800\">https://doi.org/10.1145/3302504.3311800</a>","ama":"Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. Interface-aware signal temporal logic. In: <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2019:57-66. doi:<a href=\"https://doi.org/10.1145/3302504.3311800\">10.1145/3302504.3311800</a>","ista":"Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. 2019. Interface-aware signal temporal logic. Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and Control, 57–66.","mla":"Ferrere, Thomas, et al. “Interface-Aware Signal Temporal Logic.” <i>Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2019, pp. 57–66, doi:<a href=\"https://doi.org/10.1145/3302504.3311800\">10.1145/3302504.3311800</a>.","short":"T. Ferrere, D. Nickovic, A. Donzé, H. Ito, J. Kapinski, in:, Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 57–66."},"abstract":[{"text":"Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system.","lang":"eng"}],"doi":"10.1145/3302504.3311800","day":"16","ddc":["000"],"author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","first_name":"Thomas"},{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Donzé, Alexandre","first_name":"Alexandre","last_name":"Donzé"},{"full_name":"Ito, Hisahiro","last_name":"Ito","first_name":"Hisahiro"},{"full_name":"Kapinski, James","last_name":"Kapinski","first_name":"James"}],"_id":"6428","scopus_import":"1","title":"Interface-aware signal temporal logic","publication_status":"published","date_created":"2019-05-13T08:13:46Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","file_date_updated":"2020-10-08T17:25:45Z","page":"57-66","quality_controlled":"1","publisher":"ACM","date_published":"2019-04-16T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"isbn":["9781450362825"]},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"relation":"main_file","success":1,"access_level":"open_access","file_id":"8633","creator":"dernst","date_created":"2020-10-08T17:25:45Z","checksum":"b8e967081e051d1c55ca5d18fb187890","file_size":1055421,"date_updated":"2020-10-08T17:25:45Z","file_name":"2019_ACM_Ferrere.pdf","content_type":"application/pdf"}],"publication":"Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control","has_accepted_license":"1","month":"04","oa_version":"Submitted Version","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"language":[{"iso":"eng"}],"conference":{"start_date":"2019-04-16","name":"HSCC: Hybrid Systems Computation and Control","location":"Montreal, Canada","end_date":"2019-04-18"}},{"file":[{"access_level":"open_access","relation":"main_file","creator":"dernst","file_id":"6816","file_size":659766,"checksum":"c231579f2485c6fd4df17c9443a4d80b","date_created":"2019-08-14T09:35:24Z","file_name":"2019_CAV_Avni.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:31Z"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2019-07-12T00:00:00Z","conference":{"end_date":"2019-07-18","location":"New York, NY, United States","start_date":"2019-07-13","name":"CAV: Computer Aided Verification"},"language":[{"iso":"eng"}],"project":[{"_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"oa_version":"Published Version","month":"07","has_accepted_license":"1","publication":"31st International Conference on Computer-Aided Verification","volume":11561,"ddc":["000"],"day":"12","doi":"10.1007/978-3-030-25540-4_36","abstract":[{"lang":"eng","text":"A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive  synthesis.  First,  we  abstract  the  plant  by  building  a  stochastic  model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles."}],"year":"2019","citation":{"ieee":"G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger, “Run-time optimization for learned controllers through quantitative games,” in <i>31st International Conference on Computer-Aided Verification</i>, New York, NY, United States, 2019, vol. 11561, pp. 630–649.","chicago":"Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers through Quantitative Games.” In <i>31st International Conference on Computer-Aided Verification</i>, 11561:630–49. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">https://doi.org/10.1007/978-3-030-25540-4_36</a>.","ama":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time optimization for learned controllers through quantitative games. In: <i>31st International Conference on Computer-Aided Verification</i>. Vol 11561. Springer; 2019:630-649. doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">10.1007/978-3-030-25540-4_36</a>","apa":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., &#38; Pranger, S. (2019). Run-time optimization for learned controllers through quantitative games. In <i>31st International Conference on Computer-Aided Verification</i> (Vol. 11561, pp. 630–649). New York, NY, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">https://doi.org/10.1007/978-3-030-25540-4_36</a>","ista":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019. Run-time optimization for learned controllers through quantitative games. 31st International Conference on Computer-Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 11561, 630–649.","short":"G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 630–649.","mla":"Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative Games.” <i>31st International Conference on Computer-Aided Verification</i>, vol. 11561, Springer, 2019, pp. 630–49, doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">10.1007/978-3-030-25540-4_36</a>."},"date_updated":"2023-08-25T10:33:27Z","external_id":{"isi":["000491468000036"]},"isi":1,"publisher":"Springer","quality_controlled":"1","page":"630-649","file_date_updated":"2020-07-14T12:47:31Z","article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2019-05-16T11:22:30Z","publication_status":"published","intvolume":"     11561","title":"Run-time optimization for learned controllers through quantitative games","alternative_title":["LNCS"],"scopus_import":"1","_id":"6462","author":[{"orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Bloem, Roderick","last_name":"Bloem","first_name":"Roderick"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Konighofer","first_name":"Bettina","full_name":"Konighofer, Bettina"},{"full_name":"Pranger, Stefan","last_name":"Pranger","first_name":"Stefan"}]},{"ec_funded":1,"quality_controlled":"1","page":"297-314","file_date_updated":"2020-07-14T12:47:32Z","publisher":"Springer","scopus_import":"1","_id":"6493","author":[{"id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","first_name":"Miriam","full_name":"Garcia Soto, Miriam","orcid":"0000−0003−2936−5719"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","first_name":"Christian","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065"},{"id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87","full_name":"Zeleznik, Luka","first_name":"Luka","last_name":"Zeleznik"}],"article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2019-05-27T07:09:53Z","publication_status":"published","intvolume":"     11561","alternative_title":["LNCS"],"title":"Membership-based synthesis of linear hybrid automata","volume":11561,"ddc":["000"],"year":"2019","citation":{"ieee":"M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based synthesis of linear hybrid automata,” in <i>31st International Conference on Computer-Aided Verification</i>, New York City, NY, USA, 2019, vol. 11561, pp. 297–314.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In <i>31st International Conference on Computer-Aided Verification</i>, 11561:297–314. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">https://doi.org/10.1007/978-3-030-25540-4_16</a>.","ama":"Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis of linear hybrid automata. In: <i>31st International Conference on Computer-Aided Verification</i>. Vol 11561. Springer; 2019:297-314. doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">10.1007/978-3-030-25540-4_16</a>","apa":"Garcia Soto, M., Henzinger, T. A., Schilling, C., &#38; Zeleznik, L. (2019). Membership-based synthesis of linear hybrid automata. In <i>31st International Conference on Computer-Aided Verification</i> (Vol. 11561, pp. 297–314). New York City, NY, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">https://doi.org/10.1007/978-3-030-25540-4_16</a>","ista":"Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. 2019. Membership-based synthesis of linear hybrid automata. 31st International Conference on Computer-Aided Verification. CAV: Computer-Aided Verification, LNCS, vol. 11561, 297–314.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.","mla":"Garcia Soto, Miriam, et al. “Membership-Based Synthesis of Linear Hybrid Automata.” <i>31st International Conference on Computer-Aided Verification</i>, vol. 11561, Springer, 2019, pp. 297–314, doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">10.1007/978-3-030-25540-4_16</a>."},"date_updated":"2023-08-25T10:40:41Z","external_id":{"isi":["000491468000016"]},"isi":1,"day":"12","doi":"10.1007/978-3-030-25540-4_16","abstract":[{"text":"We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements.","lang":"eng"}],"keyword":["Synthesis","Linear hybrid automaton","Membership"],"language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer-Aided Verification","start_date":"2019-07-15","end_date":"2019-07-18","location":"New York City, NY, USA"},"has_accepted_license":"1","publication":"31st International Conference on Computer-Aided Verification","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","month":"07","file":[{"content_type":"application/pdf","file_name":"2019_CAV_GarciaSoto.pdf","date_updated":"2020-07-14T12:47:32Z","checksum":"1f1d61b83a151031745ef70a501da3d6","file_size":674795,"date_created":"2019-08-14T11:05:30Z","creator":"dernst","file_id":"6817","access_level":"open_access","relation":"main_file"}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2019-07-12T00:00:00Z","publication_identifier":{"isbn":["9783030255398"],"issn":["0302-9743"]},"oa":1},{"abstract":[{"text":"In this paper, we address the problem of synthesizing periodic switching controllers for stabilizing a family of linear systems. Our broad approach consists of constructing a finite game graph based on the family of linear systems such that every winning strategy on the game graph corresponds to a stabilizing switching controller for the family of linear systems. The construction of a (finite) game graph, the synthesis of a winning strategy and the extraction of a stabilizing controller are all computationally feasible. We illustrate our method on an example.","lang":"eng"}],"day":"16","doi":"10.1109/INDIANCC.2019.8715598","year":"2019","citation":{"mla":"Kundu, Atreyee, et al. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” <i>5th Indian Control Conference Proceedings</i>, 8715598, IEEE, 2019, doi:<a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">10.1109/INDIANCC.2019.8715598</a>.","short":"A. Kundu, M. Garcia Soto, P. Prabhakar, in:, 5th Indian Control Conference Proceedings, IEEE, 2019.","ista":"Kundu A, Garcia Soto M, Prabhakar P. 2019. Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. 5th Indian Control Conference Proceedings. ICC 2019 - Indian Control Conference, 8715598.","apa":"Kundu, A., Garcia Soto, M., &#38; Prabhakar, P. (2019). Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In <i>5th Indian Control Conference Proceedings</i>. Delhi, India: IEEE. <a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">https://doi.org/10.1109/INDIANCC.2019.8715598</a>","ama":"Kundu A, Garcia Soto M, Prabhakar P. Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In: <i>5th Indian Control Conference Proceedings</i>. IEEE; 2019. doi:<a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">10.1109/INDIANCC.2019.8715598</a>","chicago":"Kundu, Atreyee, Miriam Garcia Soto, and Pavithra Prabhakar. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” In <i>5th Indian Control Conference Proceedings</i>. IEEE, 2019. <a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">https://doi.org/10.1109/INDIANCC.2019.8715598</a>.","ieee":"A. Kundu, M. Garcia Soto, and P. Prabhakar, “Formal synthesis of stabilizing controllers for periodically controlled linear switched systems,” in <i>5th Indian Control Conference Proceedings</i>, Delhi, India, 2019."},"date_updated":"2021-01-12T08:08:01Z","ddc":["000"],"title":"Formal synthesis of stabilizing controllers for periodically controlled linear switched systems","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2019-06-17T06:57:33Z","publication_status":"published","author":[{"full_name":"Kundu, Atreyee","first_name":"Atreyee","last_name":"Kundu"},{"id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","first_name":"Miriam","full_name":"Garcia Soto, Miriam","orcid":"0000−0003−2936−5719"},{"first_name":"Pavithra","last_name":"Prabhakar","full_name":"Prabhakar, Pavithra"}],"scopus_import":"1","_id":"6565","publisher":"IEEE","file_date_updated":"2020-10-21T13:13:49Z","quality_controlled":"1","oa":1,"publication_identifier":{"isbn":["978-153866246-5"]},"type":"conference","date_published":"2019-05-16T00:00:00Z","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_updated":"2020-10-21T13:13:49Z","file_name":"2019_ICC_Kundu.pdf","content_type":"application/pdf","date_created":"2020-10-21T13:13:49Z","checksum":"d622a91af1e427f6b1e0ba8e18a2b767","file_size":396031,"file_id":"8687","creator":"dernst","success":1,"relation":"main_file","access_level":"open_access"}],"article_number":"8715598","month":"05","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Submitted Version","has_accepted_license":"1","publication":"5th Indian Control Conference Proceedings","conference":{"location":"Delhi, India","end_date":"2019-01-11","name":"ICC 2019 - Indian Control Conference","start_date":"2019-01-09"},"language":[{"iso":"eng"}]},{"author":[{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman","first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"scopus_import":"1","_id":"297","intvolume":"     10805","title":"Strategy representation by decision trees in reactive synthesis","alternative_title":["LNCS"],"date_created":"2018-12-11T11:45:41Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","file_date_updated":"2020-07-14T12:45:57Z","quality_controlled":"1","ec_funded":1,"page":"385 - 407","publisher":"Springer","external_id":{"isi":["000546326300021"]},"isi":1,"citation":{"short":"T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.","mla":"Brázdil, Tomáš, et al. <i>Strategy Representation by Decision Trees in Reactive Synthesis</i>. Vol. 10805, Springer, 2018, pp. 385–407, doi:<a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">10.1007/978-3-319-89960-2_21</a>.","ista":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. 2018. Strategy representation by decision trees in reactive synthesis. TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10805, 385–407.","ama":"Brázdil T, Chatterjee K, Kretinsky J, Toman V. Strategy representation by decision trees in reactive synthesis. In: Vol 10805. Springer; 2018:385-407. doi:<a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">10.1007/978-3-319-89960-2_21</a>","apa":"Brázdil, T., Chatterjee, K., Kretinsky, J., &#38; Toman, V. (2018). Strategy representation by decision trees in reactive synthesis (Vol. 10805, pp. 385–407). Presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. <a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">https://doi.org/10.1007/978-3-319-89960-2_21</a>","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Jan Kretinsky, and Viktor Toman. “Strategy Representation by Decision Trees in Reactive Synthesis,” 10805:385–407. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-89960-2_21\">https://doi.org/10.1007/978-3-319-89960-2_21</a>.","ieee":"T. Brázdil, K. Chatterjee, J. Kretinsky, and V. Toman, “Strategy representation by decision trees in reactive synthesis,” presented at the TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10805, pp. 385–407."},"year":"2018","date_updated":"2025-06-02T08:53:40Z","abstract":[{"text":"Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.","lang":"eng"}],"day":"12","doi":"10.1007/978-3-319-89960-2_21","ddc":["000"],"volume":10805,"has_accepted_license":"1","month":"04","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"start_date":"2018-04-14","name":"TACAS 2018: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2018-04-20","location":"Thessaloniki, Greece"},"type":"conference","date_published":"2018-04-12T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publist_id":"7584","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","file":[{"file_name":"2018_LNCS_Brazdil.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:45:57Z","file_size":1829940,"checksum":"b13874ffb114932ad9cc2586b7469db4","date_created":"2018-12-17T16:29:08Z","creator":"dernst","file_id":"5723","access_level":"open_access","relation":"main_file"}]},{"date_updated":"2023-09-08T11:52:02Z","year":"2018","citation":{"short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M. Huisman (Eds.), Springer, 2018, pp. 303–319.","mla":"Nickovic, Dejan, et al. <i>AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic</i>. Edited by Dirk Beyer and Marieke Huisman, vol. 10806, Springer, 2018, pp. 303–19, doi:<a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">10.1007/978-3-319-89963-3_18</a>.","ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2018. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10806, 303–319.","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In: Beyer D, Huisman M, eds. Vol 10806. Springer; 2018:303-319. doi:<a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">10.1007/978-3-319-89963-3_18</a>","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2018). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In D. Beyer &#38; M. Huisman (Eds.) (Vol. 10806, pp. 303–319). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece: Springer. <a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">https://doi.org/10.1007/978-3-319-89963-3_18</a>","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece, 2018, vol. 10806, pp. 303–319.","chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” edited by Dirk Beyer and Marieke Huisman, 10806:303–19. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-89963-3_18\">https://doi.org/10.1007/978-3-319-89963-3_18</a>."},"isi":1,"external_id":{"isi":["00445822600018"]},"doi":"10.1007/978-3-319-89963-3_18","day":"14","abstract":[{"text":"We introduce in this paper   AMT 2.0 , a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal.","lang":"eng"}],"volume":10806,"ddc":["000"],"_id":"299","scopus_import":"1","author":[{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lebeltel, Olivier","last_name":"Lebeltel","first_name":"Olivier"},{"full_name":"Maler, Oded","first_name":"Oded","last_name":"Maler"},{"first_name":"Thomas","last_name":"Ferrere","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ulus","first_name":"Dogan","full_name":"Ulus, Dogan"}],"publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2018-12-11T11:45:41Z","alternative_title":["LNCS"],"title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","intvolume":"     10806","page":"303 - 319","quality_controlled":"1","file_date_updated":"2020-07-14T12:45:58Z","publisher":"Springer","editor":[{"full_name":"Beyer, Dirk","first_name":"Dirk","last_name":"Beyer"},{"first_name":"Marieke","last_name":"Huisman","full_name":"Huisman, Marieke"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2018-04-14T00:00:00Z","type":"conference","oa":1,"publist_id":"7582","file":[{"date_updated":"2020-07-14T12:45:58Z","file_name":"2018_LNCS_Nickovic.pdf","content_type":"application/pdf","date_created":"2019-02-06T07:33:05Z","checksum":"e11db3b9c8e27a1c7d1c738cc5e4d25a","file_size":3267209,"file_id":"5928","creator":"dernst","access_level":"open_access","relation":"main_file"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"status":"public","id":"10861","relation":"later_version"}]},"status":"public","has_accepted_license":"1","oa_version":"Published Version","month":"04","language":[{"iso":"eng"}],"conference":{"start_date":"2018-04-14","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Thessaloniki, Greece","end_date":"2018-04-20"}},{"date_published":"2018-06-08T00:00:00Z","type":"book","date_updated":"2025-07-24T09:25:31Z","citation":{"ista":"Clarke EM, Henzinger TA, Veith H, Bloem R. 2018. Handbook of Model Checking 1st ed., Cham: Springer Nature, XLVIII, 1212p.","mla":"Clarke, Edmund M., et al. <i>Handbook of Model Checking</i>. 1st ed., Springer Nature, 2018, doi:<a href=\"https://doi.org/10.1007/978-3-319-10575-8\">10.1007/978-3-319-10575-8</a>.","short":"E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st ed., Springer Nature, Cham, 2018.","ieee":"E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, <i>Handbook of Model Checking</i>, 1st ed. Cham: Springer Nature, 2018.","chicago":"Clarke, Edmund M., Thomas A Henzinger, Helmut Veith, and Roderick Bloem. <i>Handbook of Model Checking</i>. 1st ed. Cham: Springer Nature, 2018. <a href=\"https://doi.org/10.1007/978-3-319-10575-8\">https://doi.org/10.1007/978-3-319-10575-8</a>.","ama":"Clarke EM, Henzinger TA, Veith H, Bloem R. <i>Handbook of Model Checking</i>. 1st ed. Cham: Springer Nature; 2018. doi:<a href=\"https://doi.org/10.1007/978-3-319-10575-8\">10.1007/978-3-319-10575-8</a>","apa":"Clarke, E. M., Henzinger, T. A., Veith, H., &#38; Bloem, R. (2018). <i>Handbook of Model Checking</i> (1st ed.). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-10575-8\">https://doi.org/10.1007/978-3-319-10575-8</a>"},"year":"2018","retracted":"1","abstract":[{"lang":"eng","text":"This book first explores the origins of this idea, grounded in theoretical work on temporal logic and automata. The editors and authors are among the world's leading researchers in this domain, and they contributed 32 chapters representing a thorough view of the development and application of the technique. Topics covered include binary decision diagrams, symbolic model checking, satisfiability modulo theories, partial-order reduction, abstraction, interpolation, concurrency, security protocols, games, probabilistic model checking, and process algebra, and chapters on the transfer of theory to industrial practice, property specification languages for hardware, and verification of real-time systems and hybrid systems.\r\n\r\nThe book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools."}],"publist_id":"3340","doi":"10.1007/978-3-319-10575-8","edition":"1","day":"08","publication_identifier":{"isbn":["978-3-319-10574-1"],"eisbn":["978-3-319-10575-8"]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","place":"Cham","author":[{"full_name":"Clarke, Edmund M.","first_name":"Edmund M.","last_name":"Clarke"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Helmut","last_name":"Veith","full_name":"Veith, Helmut"},{"full_name":"Bloem, Roderick","last_name":"Bloem","first_name":"Roderick"}],"_id":"3300","scopus_import":"1","title":"Handbook of Model Checking","month":"06","oa_version":"None","publication_status":"published","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:02:32Z","language":[{"iso":"eng"}],"page":"XLVIII, 1212","quality_controlled":"1","publisher":"Springer Nature"}]