[{"citation":{"chicago":"Jiang, Yu, Han Liu, Huobing Song, Hui Kong, Rui Wang, Yong Guan, and Lui Sha. “Safety-Assured Model-Driven Design of the Multifunction Vehicle Bus Controller.” <i>IEEE Transactions on Intelligent Transportation Systems</i>. IEEE, 2018. <a href=\"https://doi.org/10.1109/TITS.2017.2778077\">https://doi.org/10.1109/TITS.2017.2778077</a>.","ista":"Jiang Y, Liu H, Song H, Kong H, Wang R, Guan Y, Sha L. 2018. Safety-assured model-driven design of the multifunction vehicle bus controller. IEEE Transactions on Intelligent Transportation Systems. 19(10), 3320–3333.","ieee":"Y. Jiang <i>et al.</i>, “Safety-assured model-driven design of the multifunction vehicle bus controller,” <i>IEEE Transactions on Intelligent Transportation Systems</i>, vol. 19, no. 10. IEEE, pp. 3320–3333, 2018.","mla":"Jiang, Yu, et al. “Safety-Assured Model-Driven Design of the Multifunction Vehicle Bus Controller.” <i>IEEE Transactions on Intelligent Transportation Systems</i>, vol. 19, no. 10, IEEE, 2018, pp. 3320–33, doi:<a href=\"https://doi.org/10.1109/TITS.2017.2778077\">10.1109/TITS.2017.2778077</a>.","short":"Y. Jiang, H. Liu, H. Song, H. Kong, R. Wang, Y. Guan, L. Sha, IEEE Transactions on Intelligent Transportation Systems 19 (2018) 3320–3333.","ama":"Jiang Y, Liu H, Song H, et al. Safety-assured model-driven design of the multifunction vehicle bus controller. <i>IEEE Transactions on Intelligent Transportation Systems</i>. 2018;19(10):3320-3333. doi:<a href=\"https://doi.org/10.1109/TITS.2017.2778077\">10.1109/TITS.2017.2778077</a>","apa":"Jiang, Y., Liu, H., Song, H., Kong, H., Wang, R., Guan, Y., &#38; Sha, L. (2018). Safety-assured model-driven design of the multifunction vehicle bus controller. <i>IEEE Transactions on Intelligent Transportation Systems</i>. IEEE. <a href=\"https://doi.org/10.1109/TITS.2017.2778077\">https://doi.org/10.1109/TITS.2017.2778077</a>"},"title":"Safety-assured model-driven design of the multifunction vehicle bus controller","day":"01","author":[{"first_name":"Yu","full_name":"Jiang, Yu","last_name":"Jiang"},{"last_name":"Liu","first_name":"Han","full_name":"Liu, Han"},{"first_name":"Huobing","full_name":"Song, Huobing","last_name":"Song"},{"first_name":"Hui","full_name":"Kong, Hui","last_name":"Kong","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rui","full_name":"Wang, Rui","last_name":"Wang"},{"last_name":"Guan","first_name":"Yong","full_name":"Guan, Yong"},{"first_name":"Lui","full_name":"Sha, Lui","last_name":"Sha"}],"type":"journal_article","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1205"}]},"language":[{"iso":"eng"}],"doi":"10.1109/TITS.2017.2778077","page":"3320 - 3333","month":"01","date_created":"2018-12-11T11:46:27Z","publisher":"IEEE","isi":1,"publication":"IEEE Transactions on Intelligent Transportation Systems","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","intvolume":"        19","publist_id":"7389","year":"2018","oa_version":"None","scopus_import":"1","external_id":{"isi":["000446651100020"]},"date_updated":"2023-09-18T08:12:49Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","issue":"10","_id":"434","date_published":"2018-01-01T00:00:00Z","abstract":[{"text":"In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network.","lang":"eng"}],"publication_status":"published","volume":19},{"quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"Information and Computation","intvolume":"       254","status":"public","publisher":"Elsevier","isi":1,"month":"06","date_created":"2018-12-11T11:49:58Z","page":"143 - 166","language":[{"iso":"eng"}],"doi":"10.1016/j.ic.2016.10.006","related_material":{"record":[{"id":"5428","relation":"earlier_version","status":"public"}]},"project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"day":"01","type":"journal_article","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"ec_funded":1,"citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” <i>Information and Computation</i>, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. <i>Information and Computation</i>. 2017;254(2):143-166. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2017). Quantitative fair simulation games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>"},"title":"Quantitative fair simulation games","volume":254,"publication_status":"published","_id":"1066","date_published":"2017-06-01T00:00:00Z","abstract":[{"text":"Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms.","lang":"eng"}],"issue":"2","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2023-09-20T12:07:48Z","scopus_import":"1","external_id":{"isi":["000402025600002"]},"publist_id":"6322","oa_version":"None","year":"2017"},{"status":"public","intvolume":"     10206","quality_controlled":"1","department":[{"_id":"ToHe"}],"isi":1,"publisher":"Springer","date_created":"2018-12-11T11:50:14Z","month":"03","page":"169 - 187","ddc":["000"],"doi":"10.1007/978-3-662-54580-5_10","language":[{"iso":"eng"}],"project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"type":"conference","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy"},{"first_name":"Shubham","full_name":"Goel, Shubham","last_name":"Goel"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Rodríguez Navas, Guillermo","first_name":"Guillermo","last_name":"Rodríguez Navas"}],"alternative_title":["LNCS"],"day":"31","title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","conference":{"end_date":"2017-04-29","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Uppsala, Sweden"},"citation":{"chicago":"Avni, Guy, Shubham Goel, Thomas A Henzinger, and Guillermo Rodríguez Navas. “Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults,” 10206:169–87. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>.","ista":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. 2017. Computing scores of forwarding schemes in switched networks with probabilistic faults. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10206, 169–187.","ieee":"G. Avni, S. Goel, T. A. Henzinger, and G. Rodríguez Navas, “Computing scores of forwarding schemes in switched networks with probabilistic faults,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10206, pp. 169–187.","mla":"Avni, Guy, et al. <i>Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults</i>. Vol. 10206, Springer, 2017, pp. 169–87, doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>.","short":"G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017, pp. 169–187.","ama":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding schemes in switched networks with probabilistic faults. In: Vol 10206. Springer; 2017:169-187. doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>","apa":"Avni, G., Goel, S., Henzinger, T. A., &#38; Rodríguez Navas, G. (2017). Computing scores of forwarding schemes in switched networks with probabilistic faults (Vol. 10206, pp. 169–187). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>"},"pubrep_id":"758","volume":10206,"file_date_updated":"2018-12-12T10:08:37Z","oa":1,"publication_status":"published","abstract":[{"lang":"eng","text":"Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability. \r\n\r\nWe study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant ℓ, we compute the {\\em score} of the scheme, namely the probability (induced by faults) that at least ℓ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a &quot;product-like&quot; structure. Its special structure allows us to reason about it symbolically, and reduce the scoring problem to #SAT. Our solution is generic and can be adapted to different networks and other contexts. Also, we show the computational complexity of the scoring problem is #P-complete, and we study methods to estimate the score. We evaluate the effectiveness of our techniques with an implementation. "}],"_id":"1116","date_published":"2017-03-31T00:00:00Z","file":[{"creator":"system","file_size":321800,"file_name":"IST-2017-758-v1+1_tacas-cr.pdf","access_level":"open_access","date_updated":"2018-12-12T10:08:37Z","file_id":"4698","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:08:37Z"}],"article_processing_charge":"No","publication_identifier":{"issn":["03029743"]},"external_id":{"isi":["000440733400010"]},"scopus_import":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2023-09-20T11:32:43Z","has_accepted_license":"1","oa_version":"Submitted Version","year":"2017","publist_id":"6246"},{"pubrep_id":"730","file_date_updated":"2020-07-14T12:44:34Z","oa":1,"publication_status":"published","_id":"1155","date_published":"2017-01-02T00:00:00Z","abstract":[{"lang":"eng","text":"This dissertation concerns the automatic verification of probabilistic systems and programs with arrays by statistical and logical methods. Although statistical and logical methods are different in nature, we show that they can be successfully combined for system analysis. In the first part of the dissertation we present a new statistical algorithm for the verification of probabilistic systems with respect to unbounded properties, including linear temporal logic. Our algorithm often performs faster than the previous approaches, and at the same time requires less information about the system. In addition, our method can be generalized to unbounded quantitative properties such as mean-payoff bounds. In the second part, we introduce two techniques for comparing probabilistic systems. Probabilistic systems are typically compared using the notion of equivalence, which requires the systems to have the equal probability of all behaviors. However, this notion is often too strict, since probabilities are typically only empirically estimated, and any imprecision may break the relation between processes. On the one hand, we propose to replace the Boolean notion of equivalence by a quantitative distance of similarity. For this purpose, we introduce a statistical framework for estimating distances between Markov chains based on their simulation runs, and we investigate which distances can be approximated in our framework. On the other hand, we propose to compare systems with respect to a new qualitative logic, which expresses that behaviors occur with probability one or a positive probability. This qualitative analysis is robust with respect to modeling errors and applicable to many domains. In the last part, we present a new quantifier-free logic for integer arrays, which allows us to express counting. Counting properties are prevalent in array-manipulating programs, however they cannot be expressed in the quantified fragments of the theory of arrays. We present a decision procedure for our logic, and provide several complexity results."}],"file":[{"date_created":"2018-12-12T10:11:26Z","file_id":"4880","relation":"main_file","content_type":"application/pdf","access_level":"open_access","date_updated":"2020-07-14T12:44:34Z","checksum":"1406a681cb737508234fde34766be2c2","file_size":1028586,"creator":"system","file_name":"IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf"}],"article_processing_charge":"No","publication_identifier":{"issn":["2663-337X"]},"date_updated":"2023-09-07T11:58:34Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","year":"2017","oa_version":"Published Version","has_accepted_license":"1","publist_id":"6203","status":"public","department":[{"_id":"ToHe"}],"degree_awarded":"PhD","publisher":"Institute of Science and Technology Austria","supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"date_created":"2018-12-11T11:50:27Z","month":"01","page":"163","ddc":["004","005"],"doi":"10.15479/AT:ISTA:TH_730","language":[{"iso":"eng"}],"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"status":"public","id":"1093","relation":"part_of_dissertation"},{"id":"1230","relation":"part_of_dissertation","status":"public"},{"status":"public","id":"1234","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"1391"},{"id":"1501","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","id":"1502","status":"public"},{"status":"public","id":"2063","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"2167"}]},"acknowledgement":" First of all, I want to thank my advisor, prof. Thomas A. Henzinger, for his guidance during my PhD program. I am grateful for the freedom I was given to pursue my research interests, and his continuous support. Working with prof. Henzinger was a truly inspiring experience and taught me what it means to be a scientist. I want to express my gratitude to my collaborators: Nikola Beneš, Krishnendu Chatterjee, Martin Chmelík, Ashutosh Gupta, Willibald Krenn, Jan Kˇretínský, Dejan Nickovic, Andrey Kupriyanov, and Tatjana Petrov. I have learned a great deal from my collaborators, and without their help this thesis would not be possible. In addition, I want to thank the members of my thesis committee: Dirk Beyer, Dejan Nickovic, and Georg Weissenbacher for their advice and reviewing this dissertation. I would especially like to acknowledge the late Helmut Veith, who was a member of my committee. I will remember Helmut for his kindness, enthusiasm, and wit, as well as for being an inspiring scientist. Finally, I would like to thank my colleagues for making my stay at IST such a pleasant experience: Guy Avni, Sergiy Bogomolov, Ventsislav Chonev, Rasmus Ibsen-Jensen, Mirco Giacobbe, Bernhard Kragl, Hui Kong, Petr Novotný, Jan Otop, Andreas Pavlogiannis, Tantjana Petrov, Arjun Radhakrishna, Jakob Ruess, Thorsten Tarrach, as well as other members of groups Henzinger and Chatterjee. ","author":[{"last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"}],"type":"dissertation","alternative_title":["ISTA Thesis"],"day":"02","title":"Statistical and logical methods for property checking","citation":{"mla":"Daca, Przemyslaw. <i>Statistical and Logical Methods for Property Checking</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>.","chicago":"Daca, Przemyslaw. “Statistical and Logical Methods for Property Checking.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>.","ista":"Daca P. 2017. Statistical and logical methods for property checking. Institute of Science and Technology Austria.","ieee":"P. Daca, “Statistical and logical methods for property checking,” Institute of Science and Technology Austria, 2017.","ama":"Daca P. Statistical and logical methods for property checking. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>","apa":"Daca, P. (2017). <i>Statistical and logical methods for property checking</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>","short":"P. Daca, Statistical and Logical Methods for Property Checking, Institute of Science and Technology Austria, 2017."},"ec_funded":1},{"day":"01","type":"conference","author":[{"last_name":"Kong","first_name":"Hui","full_name":"Kong, Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941"},{"orcid":"0000-0002-0686-0365","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"last_name":"Schilling","full_name":"Schilling, Christian","first_name":"Christian"},{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"citation":{"ama":"Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA. Safety verification of nonlinear hybrid systems based on invariant clusters. In: <i>Proceedings of the 20th International Conference on Hybrid Systems</i>. ACM; 2017:163-172. doi:<a href=\"https://doi.org/10.1145/3049797.3049814\">10.1145/3049797.3049814</a>","apa":"Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., &#38; Henzinger, T. A. (2017). Safety verification of nonlinear hybrid systems based on invariant clusters. In <i>Proceedings of the 20th International Conference on Hybrid Systems</i> (pp. 163–172). Pittsburgh, PA, United States: ACM. <a href=\"https://doi.org/10.1145/3049797.3049814\">https://doi.org/10.1145/3049797.3049814</a>","short":"H. Kong, S. Bogomolov, C. Schilling, Y. Jiang, T.A. Henzinger, in:, Proceedings of the 20th International Conference on Hybrid Systems, ACM, 2017, pp. 163–172.","mla":"Kong, Hui, et al. “Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters.” <i>Proceedings of the 20th International Conference on Hybrid Systems</i>, ACM, 2017, pp. 163–72, doi:<a href=\"https://doi.org/10.1145/3049797.3049814\">10.1145/3049797.3049814</a>.","chicago":"Kong, Hui, Sergiy Bogomolov, Christian Schilling, Yu Jiang, and Thomas A Henzinger. “Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters.” In <i>Proceedings of the 20th International Conference on Hybrid Systems</i>, 163–72. ACM, 2017. <a href=\"https://doi.org/10.1145/3049797.3049814\">https://doi.org/10.1145/3049797.3049814</a>.","ista":"Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA. 2017. Safety verification of nonlinear hybrid systems based on invariant clusters. Proceedings of the 20th International Conference on Hybrid Systems. HSCC: Hybrid Systems Computation and Control , 163–172.","ieee":"H. Kong, S. Bogomolov, C. Schilling, Y. Jiang, and T. A. Henzinger, “Safety verification of nonlinear hybrid systems based on invariant clusters,” in <i>Proceedings of the 20th International Conference on Hybrid Systems</i>, Pittsburgh, PA, United States, 2017, pp. 163–172."},"conference":{"location":"Pittsburgh, PA, United States","name":"HSCC: Hybrid Systems Computation and Control ","end_date":"2017-04-20","start_date":"2017-04-18"},"title":"Safety verification of nonlinear hybrid systems based on invariant clusters","language":[{"iso":"eng"}],"ddc":["000"],"doi":"10.1145/3049797.3049814","month":"04","date_created":"2018-12-11T11:47:47Z","page":"163 - 172","quality_controlled":"1","department":[{"_id":"ToHe"}],"publication":"Proceedings of the 20th International Conference on Hybrid Systems","status":"public","publisher":"ACM","publist_id":"7067","oa_version":"Submitted Version","has_accepted_license":"1","year":"2017","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T08:08:17Z","scopus_import":1,"publication_identifier":{"isbn":["978-145034590-3"]},"file":[{"file_name":"IST-2017-817-v1+1_p163-kong.pdf","creator":"system","file_size":1650530,"date_updated":"2020-07-14T12:47:34Z","access_level":"open_access","checksum":"b7667434cbf5b5f0ade3bea1dbe5bf63","content_type":"application/pdf","file_id":"4873","relation":"main_file","date_created":"2018-12-12T10:11:20Z"}],"abstract":[{"lang":"eng","text":"In this paper, we propose an approach to automatically compute invariant clusters for nonlinear semialgebraic hybrid systems. An invariant cluster for an ordinary differential equation (ODE) is a multivariate polynomial invariant g(u→, x→) = 0, parametric in u→, which can yield an infinite number of concrete invariants by assigning different values to u→ so that every trajectory of the system can be overapproximated precisely by the intersection of a group of concrete invariants. For semialgebraic systems, which involve ODEs with multivariate polynomial right-hand sides, given a template multivariate polynomial g(u→, x→), an invariant cluster can be obtained by first computing the remainder of the Lie derivative of g(u→, x→) divided by g(u→, x→) and then solving the system of polynomial equations obtained from the coefficients of the remainder. Based on invariant clusters and sum-of-squares (SOS) programming, we present a new method for the safety verification of hybrid systems. Experiments on nonlinear benchmark systems from biology and control theory show that our approach is efficient. "}],"_id":"663","date_published":"2017-04-01T00:00:00Z","file_date_updated":"2020-07-14T12:47:34Z","pubrep_id":"817","publication_status":"published","oa":1},{"article_number":"5","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"4661","date_created":"2018-12-12T10:08:02Z","file_name":"IST-2017-886-v1+1_LIPIcs-CONCUR-2017-5.pdf","creator":"system","file_size":570294,"date_updated":"2020-07-14T12:47:49Z","access_level":"open_access","checksum":"d2bda4783821a6358333fe27f11f4737"}],"date_published":"2017-08-01T00:00:00Z","_id":"711","abstract":[{"text":"Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.","lang":"eng"}],"publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:47:49Z","volume":85,"pubrep_id":"886","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publist_id":"6976","year":"2017","has_accepted_license":"1","oa_version":"Published Version","date_updated":"2021-01-12T08:11:53Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"publication_identifier":{"issn":["18688969"]},"month":"08","date_created":"2018-12-11T11:48:04Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","status":"public","intvolume":"        85","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Bidirectional nested weighted automata (Vol. 85). Presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.5</a>","ama":"Chatterjee K, Henzinger TA, Otop J. Bidirectional nested weighted automata. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">10.4230/LIPIcs.CONCUR.2017.5</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Bidirectional nested weighted automata,” presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany, 2017, vol. 85.","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Bidirectional nested weighted automata. 28th International Conference on Concurrency Theory, CONCUR, LIPIcs, vol. 85, 5.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Bidirectional Nested Weighted Automata,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.5</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Bidirectional Nested Weighted Automata</i>. Vol. 85, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">10.4230/LIPIcs.CONCUR.2017.5</a>."},"conference":{"location":"Berlin, Germany","name":"28th International Conference on Concurrency Theory, CONCUR","end_date":"2017-09-08","start_date":"2017-09-05"},"title":"Bidirectional nested weighted automata","day":"01","alternative_title":["LIPIcs"],"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"type":"conference","language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.CONCUR.2017.5","ddc":["004","005"]},{"isi":1,"publication_status":"published","publisher":"Springer","intvolume":"        51","status":"public","volume":51,"publication":"Formal Methods in System Design","quality_controlled":"1","department":[{"_id":"ToHe"}],"article_processing_charge":"No","issue":"2","page":"267 - 269","_id":"743","abstract":[{"lang":"eng","text":"This special issue of the Journal on Formal Methods in System Design is dedicated to Prof. Helmut Veith, who unexpectedly passed away in March 2016. Helmut Veith was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the formal methods community. Helmut was not only known for his numerous and influential contributions in the field of automated verification (most prominently his work on Counterexample-Guided Abstraction Refinement [1,2]), but also for his untiring and passionate efforts for the logic community: he co-organized the Vienna Summer of Logic (an event comprising twelve conferences and numerous workshops which attracted thousands of researchers from all over the world), he initiated the Vienna Center for Logic and Algorithms (which promotes international collaboration on logic and algorithms and organizes outreach events such as the LogicLounge), and he coordinated the Doctoral Program on Logical Methods in Computer Science at TU Wien (currently educating more than 40 doctoral students) and a National Research Network on Rigorous Systems Engineering (uniting fifteen researchers in Austria to address the challenge of building reliable and safe computer\r\nsystems). With his enthusiasm and commitment, Helmut completely reshaped the Austrian research landscape in the field of logic and verification in his few years as a full professor at TU Wien."}],"date_created":"2018-12-11T11:48:16Z","date_published":"2017-11-14T00:00:00Z","month":"11","doi":"10.1007/s10703-017-0307-6","external_id":{"isi":["000415615600001"]},"date_updated":"2023-09-27T12:29:29Z","language":[{"iso":"eng"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"Preface of the special issue in memoriam Helmut Veith","citation":{"short":"G. Gottlob, T.A. Henzinger, G. Weißenbacher, Formal Methods in System Design 51 (2017) 267–269.","ama":"Gottlob G, Henzinger TA, Weißenbacher G. Preface of the special issue in memoriam Helmut Veith. <i>Formal Methods in System Design</i>. 2017;51(2):267-269. doi:<a href=\"https://doi.org/10.1007/s10703-017-0307-6\">10.1007/s10703-017-0307-6</a>","apa":"Gottlob, G., Henzinger, T. A., &#38; Weißenbacher, G. (2017). Preface of the special issue in memoriam Helmut Veith. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-017-0307-6\">https://doi.org/10.1007/s10703-017-0307-6</a>","chicago":"Gottlob, Georg, Thomas A Henzinger, and Georg Weißenbacher. “Preface of the Special Issue in Memoriam Helmut Veith.” <i>Formal Methods in System Design</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s10703-017-0307-6\">https://doi.org/10.1007/s10703-017-0307-6</a>.","ieee":"G. Gottlob, T. A. Henzinger, and G. Weißenbacher, “Preface of the special issue in memoriam Helmut Veith,” <i>Formal Methods in System Design</i>, vol. 51, no. 2. Springer, pp. 267–269, 2017.","ista":"Gottlob G, Henzinger TA, Weißenbacher G. 2017. Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. 51(2), 267–269.","mla":"Gottlob, Georg, et al. “Preface of the Special Issue in Memoriam Helmut Veith.” <i>Formal Methods in System Design</i>, vol. 51, no. 2, Springer, 2017, pp. 267–69, doi:<a href=\"https://doi.org/10.1007/s10703-017-0307-6\">10.1007/s10703-017-0307-6</a>."},"type":"journal_article","author":[{"last_name":"Gottlob","full_name":"Gottlob, Georg","first_name":"Georg"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Weißenbacher","full_name":"Weißenbacher, Georg","first_name":"Georg"}],"oa_version":"None","year":"2017","publist_id":"6924","day":"14"},{"abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"_id":"465","date_published":"2017-09-13T00:00:00Z","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"5090","date_created":"2018-12-12T10:14:37Z","file_name":"IST-2015-321-v1+1_main.pdf","creator":"system","file_size":279071,"date_updated":"2020-07-14T12:46:33Z","access_level":"open_access","checksum":"08041379ba408d40664f449eb5907a8f"},{"date_created":"2018-12-12T10:14:38Z","content_type":"application/pdf","relation":"main_file","file_id":"5091","checksum":"08041379ba408d40664f449eb5907a8f","date_updated":"2020-07-14T12:46:33Z","access_level":"open_access","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","creator":"system","file_size":279071}],"issue":"3","pubrep_id":"955","tmp":{"name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","short":"CC BY-ND (4.0)"},"volume":13,"file_date_updated":"2020-07-14T12:46:33Z","oa":1,"publication_status":"published","oa_version":"Published Version","has_accepted_license":"1","year":"2017","publist_id":"7356","publication_identifier":{"issn":["18605974"]},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:26:25Z","date_created":"2018-12-11T11:46:37Z","month":"09","status":"public","intvolume":"        13","publication":"Logical Methods in Computer Science","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"International Federation of Computational Logic","type":"journal_article","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"day":"13","title":"Edit distance for pushdown automata","citation":{"mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017)."},"ec_funded":1,"ddc":["004"],"doi":"10.23638/LMCS-13(3:23)2017","language":[{"iso":"eng"}],"project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"}],"related_material":{"record":[{"relation":"earlier_version","id":"1610","status":"public"},{"relation":"earlier_version","id":"5438","status":"public"}]}},{"oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}],"publication_status":"published","volume":18,"issue":"4","arxiv":1,"_id":"467","abstract":[{"text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.","lang":"eng"}],"date_published":"2017-12-01T00:00:00Z","article_number":"31","publication_identifier":{"issn":["15293785"]},"external_id":{"arxiv":["1606.03598"]},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:26:19Z","oa_version":"Preprint","year":"2017","publist_id":"7354","publisher":"ACM","intvolume":"        18","status":"public","publication":"ACM Transactions on Computational Logic (TOCL)","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","date_created":"2018-12-11T11:46:38Z","month":"12","related_material":{"record":[{"status":"public","id":"1656","relation":"earlier_version"},{"relation":"earlier_version","id":"5415","status":"public"},{"status":"public","relation":"earlier_version","id":"5436"}]},"project":[{"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"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.1145/3152769","language":[{"iso":"eng"}],"title":"Nested weighted automata","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 18(4), 31.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>"},"ec_funded":1,"type":"journal_article","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"day":"01"},{"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana"}],"type":"journal_article","day":"01","title":"Faster statistical model checking for unbounded temporal properties","ec_funded":1,"citation":{"ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(2). doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017).","mla":"Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2, 12, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2. ACM, 2017.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 18(2), 12."},"doi":"10.1145/3060139","language":[{"iso":"eng"}],"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"related_material":{"record":[{"status":"public","id":"1234","relation":"earlier_version"}]},"date_created":"2018-12-11T11:46:39Z","month":"05","status":"public","intvolume":"        18","quality_controlled":"1","department":[{"_id":"ToHe"}],"publication":"ACM Transactions on Computational Logic (TOCL)","publisher":"ACM","year":"2017","oa_version":"Submitted Version","publist_id":"7349","publication_identifier":{"issn":["15293785"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-21T16:48:11Z","scopus_import":1,"date_published":"2017-05-01T00:00:00Z","_id":"471","abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. ","lang":"eng"}],"article_number":"12","issue":"2","volume":18,"main_file_link":[{"url":"https://arxiv.org/abs/1504.05739","open_access":"1"}],"oa":1,"publication_status":"published"},{"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"doi":"10.4204/EPTCS.259.3","ddc":["004"],"language":[{"iso":"eng"}],"conference":{"name":"CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies","end_date":"2017-04-29","start_date":"2017-04-29","location":"Uppsala, Sweden"},"title":"Causality-based model checking","citation":{"chicago":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” In <i>Electronic Proceedings in Theoretical Computer Science</i>, 259:31–38. Open Publishing Association, 2017. <a href=\"https://doi.org/10.4204/EPTCS.259.3\">https://doi.org/10.4204/EPTCS.259.3</a>.","ista":"Finkbeiner B, Kupriyanov A. 2017. Causality-based model checking. Electronic Proceedings in Theoretical Computer Science. CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies, EPTCS, vol. 259, 31–38.","ieee":"B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in <i>Electronic Proceedings in Theoretical Computer Science</i>, Uppsala, Sweden, 2017, vol. 259, pp. 31–38.","mla":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” <i>Electronic Proceedings in Theoretical Computer Science</i>, vol. 259, Open Publishing Association, 2017, pp. 31–38, doi:<a href=\"https://doi.org/10.4204/EPTCS.259.3\">10.4204/EPTCS.259.3</a>.","short":"B. Finkbeiner, A. Kupriyanov, in:, Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2017, pp. 31–38.","ama":"Finkbeiner B, Kupriyanov A. Causality-based model checking. In: <i>Electronic Proceedings in Theoretical Computer Science</i>. Vol 259. Open Publishing Association; 2017:31-38. doi:<a href=\"https://doi.org/10.4204/EPTCS.259.3\">10.4204/EPTCS.259.3</a>","apa":"Finkbeiner, B., &#38; Kupriyanov, A. (2017). Causality-based model checking. In <i>Electronic Proceedings in Theoretical Computer Science</i> (Vol. 259, pp. 31–38). Uppsala, Sweden: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.259.3\">https://doi.org/10.4204/EPTCS.259.3</a>"},"alternative_title":["EPTCS"],"author":[{"first_name":"Bernd","full_name":"Finkbeiner, Bernd","last_name":"Finkbeiner"},{"id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","full_name":"Kupriyanov, Andrey","first_name":"Andrey","last_name":"Kupriyanov"}],"type":"conference","day":"10","publisher":"Open Publishing Association","intvolume":"       259","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"}],"publication":"Electronic Proceedings in Theoretical Computer Science","page":"31 - 38","date_created":"2018-12-11T11:47:07Z","month":"10","publication_identifier":{"issn":["2075-2180"]},"date_updated":"2023-10-17T12:02:46Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","year":"2017","has_accepted_license":"1","oa_version":"Submitted Version","publist_id":"7264","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1710.03391v1","open_access":"1"}],"publication_status":"published","volume":259,"pubrep_id":"925","file_date_updated":"2020-07-14T12:47:00Z","article_processing_charge":"No","_id":"549","date_published":"2017-10-10T00:00:00Z","abstract":[{"lang":"eng","text":"Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of model checking algorithms that capture the causal relationships in a special data structure called concurrent traces. Concurrent traces identify key events in an execution history and link them through their cause-effect relationships. The model checker builds a tableau of concurrent traces, where the case splits represent different causal explanations of a hypothetical error. Causality-based model checking has been implemented in the ARCTOR tool, and applied to previously intractable multi-threaded benchmarks."}],"file":[{"date_created":"2018-12-12T10:12:21Z","relation":"main_file","file_id":"4939","content_type":"application/pdf","checksum":"6274f6c0da3376a7b079180d81568518","access_level":"open_access","date_updated":"2020-07-14T12:47:00Z","creator":"system","file_size":209294,"file_name":"IST-2018-925-v1+1_1710.03391v1.pdf"}]},{"date_updated":"2025-06-02T08:53:45Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","publication_identifier":{"isbn":["978-3-319-63120-2"],"issn":["0302-9743"]},"editor":[{"last_name":"Aceto","full_name":"Aceto, Luca","first_name":"Luca"},{"first_name":"Giorgio","full_name":"Bacci, Giorgio","last_name":"Bacci"},{"first_name":"Anna","full_name":"Ingólfsdóttir, Anna","last_name":"Ingólfsdóttir"},{"last_name":"Legay","first_name":"Axel","full_name":"Legay, Axel"},{"full_name":"Mardare, Radu","first_name":"Radu","last_name":"Mardare"}],"publist_id":"7170","oa_version":"Submitted Version","year":"2017","has_accepted_license":"1","publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:47:25Z","volume":10460,"article_processing_charge":"No","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:47:25Z","checksum":"b2402766ec02c79801aac634bd8f9f6c","file_size":192826,"creator":"dernst","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","date_created":"2019-11-19T08:06:50Z","file_id":"7048","relation":"main_file","content_type":"application/pdf"}],"_id":"625","abstract":[{"lang":"eng","text":"In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the computational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games."}],"date_published":"2017-07-25T00:00:00Z","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 and S11407-N23 (RiSE/SHiNE), and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003.","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"ddc":["000"],"doi":"10.1007/978-3-319-63121-9_18","ec_funded":1,"citation":{"ama":"Chatterjee K, Doyen L, Henzinger TA. The cost of exactness in quantitative reachability. In: Aceto L, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, eds. <i>Models, Algorithms, Logics and Tools</i>. Vol 10460. Theoretical Computer Science and General Issues. Springer; 2017:367-381. doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, &#38; R. Mardare (Eds.), <i>Models, Algorithms, Logics and Tools</i> (Vol. 10460, pp. 367–381). Springer. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017, pp. 367–381.","mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost of Exactness in Quantitative Reachability.” In <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto, Giorgio Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare, 10460:367–81. Theoretical Computer Science and General Issues. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2017.The cost of exactness in quantitative reachability. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, 367–381.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in <i>Models, Algorithms, Logics and Tools</i>, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381."},"title":"The cost of exactness in quantitative reachability","day":"25","alternative_title":["LNCS"],"type":"book_chapter","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"Models, Algorithms, Logics and Tools","status":"public","intvolume":"     10460","page":"367 - 381","month":"07","series_title":"Theoretical Computer Science and General Issues","date_created":"2018-12-11T11:47:34Z"},{"file":[{"file_name":"IST-2017-741-v1+1_main.pdf","file_size":569863,"creator":"system","checksum":"f395d0d20102b89aeaad8b4ef4f18f4f","date_updated":"2020-07-14T12:47:27Z","access_level":"open_access","content_type":"application/pdf","file_id":"4897","relation":"main_file","date_created":"2018-12-12T10:11:41Z"},{"file_name":"IST-2018-741-v2+2_main.pdf","creator":"system","file_size":563276,"date_updated":"2020-07-14T12:47:27Z","access_level":"open_access","checksum":"f416ee1ae4497b23ecdf28b1f18bb8df","content_type":"application/pdf","file_id":"4898","relation":"main_file","date_created":"2018-12-12T10:11:42Z"}],"date_published":"2017-03-31T00:00:00Z","_id":"631","abstract":[{"lang":"eng","text":"Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata."}],"file_date_updated":"2020-07-14T12:47:27Z","volume":10205,"pubrep_id":"966","publication_status":"published","oa":1,"publist_id":"7162","has_accepted_license":"1","oa_version":"Submitted Version","year":"2017","date_updated":"2023-09-07T12:53:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"publication_identifier":{"isbn":["978-366254576-8"]},"month":"03","date_created":"2018-12-11T11:47:36Z","page":"589 - 606","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","intvolume":"     10205","publisher":"Springer","day":"31","alternative_title":["LNCS"],"type":"conference","author":[{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov"},{"last_name":"Frehse","first_name":"Goran","full_name":"Frehse, Goran"},{"last_name":"Giacobbe","full_name":"Giacobbe, Mirco","first_name":"Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"citation":{"mla":"Bogomolov, Sergiy, et al. <i>Counterexample Guided Refinement of Template Polyhedra</i>. Vol. 10205, Springer, 2017, pp. 589–606, doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">10.1007/978-3-662-54577-5_34</a>.","chicago":"Bogomolov, Sergiy, Goran Frehse, Mirco Giacobbe, and Thomas A Henzinger. “Counterexample Guided Refinement of Template Polyhedra,” 10205:589–606. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">https://doi.org/10.1007/978-3-662-54577-5_34</a>.","ieee":"S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample guided refinement of template polyhedra,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205, pp. 589–606.","ista":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. 2017. Counterexample guided refinement of template polyhedra. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 589–606.","ama":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">10.1007/978-3-662-54577-5_34</a>","apa":"Bogomolov, S., Frehse, G., Giacobbe, M., &#38; Henzinger, T. A. (2017). Counterexample guided refinement of template polyhedra (Vol. 10205, pp. 589–606). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">https://doi.org/10.1007/978-3-662-54577-5_34</a>","short":"S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017, pp. 589–606."},"conference":{"location":"Uppsala, Sweden","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2017-04-29","start_date":"2017-04-22"},"title":"Counterexample guided refinement of template polyhedra","language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-54577-5_34","ddc":["000"],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by the European Commission under grant 643921 (UnCoVerCPS), and by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems).","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"6894"}]},"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}]},{"publication_status":"published","volume":10381,"_id":"633","date_published":"2017-01-01T00:00:00Z","abstract":[{"text":"A Rapidly-exploring Random Tree (RRT) is an algorithm which can search a non-convex region of space by incrementally building a space-filling tree. The tree is constructed from random points drawn from system’s state space and is biased to grow towards large unexplored areas in the system. RRT can provide better coverage of a system’s possible behaviors compared with random simulations, but is more lightweight than full reachability analysis. In this paper, we explore some of the design decisions encountered while implementing a hybrid extension of the RRT algorithm, which have not been elaborated on before. In particular, we focus on handling non-determinism, which arises due to discrete transitions. We introduce the notion of important points to account for this phenomena. We showcase our ideas using heater and navigation benchmarks.","lang":"eng"}],"date_updated":"2021-01-12T08:07:06Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"publication_identifier":{"isbn":["978-331963500-2"]},"editor":[{"last_name":"Abate","first_name":"Alessandro","full_name":"Abate, Alessandro"},{"full_name":"Bodo, Sylvie","first_name":"Sylvie","last_name":"Bodo"}],"publist_id":"7159","year":"2017","oa_version":"None","publisher":"Springer","department":[{"_id":"ToHe"}],"quality_controlled":"1","intvolume":"     10381","status":"public","page":"83 - 89","month":"01","date_created":"2018-12-11T11:47:37Z","project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-63501-9_6","citation":{"ista":"Bak S, Bogomolov S, Henzinger TA, Kumar A. 2017. Challenges and tool implementation of hybrid rapidly exploring random trees. NSV: Numerical Software Verification, LNCS, vol. 10381, 83–89.","ieee":"S. Bak, S. Bogomolov, T. A. Henzinger, and A. Kumar, “Challenges and tool implementation of hybrid rapidly exploring random trees,” presented at the NSV: Numerical Software Verification, Heidelberg, Germany, 2017, vol. 10381, pp. 83–89.","chicago":"Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, and Aviral Kumar. “Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees.” edited by Alessandro Abate and Sylvie Bodo, 10381:83–89. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">https://doi.org/10.1007/978-3-319-63501-9_6</a>.","mla":"Bak, Stanley, et al. <i>Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees</i>. Edited by Alessandro Abate and Sylvie Bodo, vol. 10381, Springer, 2017, pp. 83–89, doi:<a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">10.1007/978-3-319-63501-9_6</a>.","short":"S. Bak, S. Bogomolov, T.A. Henzinger, A. Kumar, in:, A. Abate, S. Bodo (Eds.), Springer, 2017, pp. 83–89.","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., &#38; Kumar, A. (2017). Challenges and tool implementation of hybrid rapidly exploring random trees. In A. Abate &#38; S. Bodo (Eds.) (Vol. 10381, pp. 83–89). Presented at the NSV: Numerical Software Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">https://doi.org/10.1007/978-3-319-63501-9_6</a>","ama":"Bak S, Bogomolov S, Henzinger TA, Kumar A. Challenges and tool implementation of hybrid rapidly exploring random trees. In: Abate A, Bodo S, eds. Vol 10381. Springer; 2017:83-89. doi:<a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">10.1007/978-3-319-63501-9_6</a>"},"conference":{"name":"NSV: Numerical Software Verification","end_date":"2017-07-23","start_date":"2017-07-22","location":"Heidelberg, Germany"},"title":"Challenges and tool implementation of hybrid rapidly exploring random trees","day":"01","alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Aviral","full_name":"Kumar, Aviral","last_name":"Kumar"}]},{"citation":{"ista":"Bakhirkin A, Ferrere T, Maler O, Ulus D. 2017. On the quantitative semantics of regular expressions over real-valued signals. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 189–206.","ieee":"A. Bakhirkin, T. Ferrere, O. Maler, and D. Ulus, “On the quantitative semantics of regular expressions over real-valued signals,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 189–206.","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Oded Maler, and Dogan Ulus. “On the Quantitative Semantics of Regular Expressions over Real-Valued Signals.” edited by Alessandro Abate and Gilles Geeraerts, 10419:189–206. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>.","mla":"Bakhirkin, Alexey, et al. <i>On the Quantitative Semantics of Regular Expressions over Real-Valued Signals</i>. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 189–206, doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>.","short":"A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206.","apa":"Bakhirkin, A., Ferrere, T., Maler, O., &#38; Ulus, D. (2017). On the quantitative semantics of regular expressions over real-valued signals. In A. Abate &#38; G. Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>","ama":"Bakhirkin A, Ferrere T, Maler O, Ulus D. On the quantitative semantics of regular expressions over real-valued signals. In: Abate A, Geeraerts G, eds. Vol 10419. Springer; 2017:189-206. doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>"},"title":"On the quantitative semantics of regular expressions over real-valued signals","conference":{"start_date":"2017-09-05","end_date":"2017-09-07","name":"FORMATS: Formal Modelling and Analysis of Timed Systems","location":"Berlin, Germany"},"day":"03","author":[{"first_name":"Alexey","full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin"},{"full_name":"Ferrere, Thomas","first_name":"Thomas","last_name":"Ferrere","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Maler","first_name":"Oded","full_name":"Maler, Oded"},{"last_name":"Ulus","first_name":"Dogan","full_name":"Ulus, Dogan"}],"type":"conference","alternative_title":["LNCS"],"project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-65765-3_11","page":"189 - 206","month":"08","date_created":"2018-12-11T11:47:38Z","publisher":"Springer","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","intvolume":"     10419","editor":[{"last_name":"Abate","full_name":"Abate, Alessandro","first_name":"Alessandro"},{"last_name":"Geeraerts","first_name":"Gilles","full_name":"Geeraerts, Gilles"}],"publist_id":"7152","oa_version":"Submitted Version","year":"2017","scopus_import":1,"date_updated":"2021-01-12T08:07:14Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"isbn":["978-331965764-6"]},"abstract":[{"lang":"eng","text":"Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems."}],"_id":"636","date_published":"2017-08-03T00:00:00Z","publication_status":"published","oa":1,"main_file_link":[{"url":"https://hal.archives-ouvertes.fr/hal-01552132","open_access":"1"}],"volume":10419},{"department":[{"_id":"ToHe"}],"quality_controlled":"1","volume":10152,"intvolume":"     10152","status":"public","publisher":"Springer","publication_status":"published","month":"01","_id":"638","series_title":"LNCS","date_published":"2017-01-01T00:00:00Z","abstract":[{"text":"This book constitutes the refereed proceedings of the 9th InternationalWorkshop on Numerical Software Verification, NSV 2016, held in Toronto, ON, Canada in July 2011 - colocated with CAV 2016, the 28th International Conference on Computer Aided Verification.\r\nThe NSV workshop is dedicated to the development of logical and mathematical techniques for the reasoning about programmability and reliability.","lang":"eng"}],"date_created":"2018-12-11T11:47:38Z","article_processing_charge":"No","date_updated":"2022-05-24T07:09:52Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-319-54292-8","publication_identifier":{"issn":["0302-9743"],"eisbn":["978-3-319-54292-8"]},"publist_id":"7150","day":"01","oa_version":"None","year":"2017","type":"conference_editor","citation":{"mla":"Bogomolov, Sergiy, et al., editors. <i>Numerical Software Verification</i>. Vol. 10152, Springer, 2017, doi:<a href=\"https://doi.org/10.1007/978-3-319-54292-8\">10.1007/978-3-319-54292-8</a>.","chicago":"Bogomolov, Sergiy, Matthieu Martel, and Pavithra Prabhakar, eds. <i>Numerical Software Verification</i>. Vol. 10152. LNCS. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-54292-8\">https://doi.org/10.1007/978-3-319-54292-8</a>.","ieee":"S. Bogomolov, M. Martel, and P. Prabhakar, Eds., <i>Numerical Software Verification</i>, vol. 10152. Springer, 2017.","ista":"Bogomolov S, Martel M, Prabhakar P eds. 2017. Numerical Software Verification, Springer,p.","ama":"Bogomolov S, Martel M, Prabhakar P, eds. <i>Numerical Software Verification</i>. Vol 10152. Springer; 2017. doi:<a href=\"https://doi.org/10.1007/978-3-319-54292-8\">10.1007/978-3-319-54292-8</a>","apa":"Bogomolov, S., Martel, M., &#38; Prabhakar, P. (Eds.). (2017). <i>Numerical Software Verification</i> (Vol. 10152). Presented at the NSV: Numerical Software Verification, Toronto, ON, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-54292-8\">https://doi.org/10.1007/978-3-319-54292-8</a>","short":"S. Bogomolov, M. Martel, P. Prabhakar, eds., Numerical Software Verification, Springer, 2017."},"conference":{"name":"NSV: Numerical Software Verification","start_date":"2016-07-17","end_date":"2016-07-18","location":"Toronto, ON, Canada"},"editor":[{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"last_name":"Martel","full_name":"Martel, Matthieu","first_name":"Matthieu"},{"first_name":"Pavithra","full_name":"Prabhakar, Pavithra","last_name":"Prabhakar"}],"title":"Numerical Software Verification"},{"related_material":{"record":[{"status":"public","relation":"later_version","id":"133"}]},"ddc":["000"],"doi":"10.15479/AT:IST-2018-853-v2-2","publication_identifier":{"issn":["2664-1690"]},"date_updated":"2023-02-21T16:59:21Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Synchronizing the asynchronous","citation":{"chicago":"Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. <i>Synchronizing the Asynchronous</i>. IST Austria, 2017. <a href=\"https://doi.org/10.15479/AT:IST-2018-853-v2-2\">https://doi.org/10.15479/AT:IST-2018-853-v2-2</a>.","ieee":"T. A. Henzinger, B. Kragl, and S. Qadeer, <i>Synchronizing the asynchronous</i>. IST Austria, 2017.","ista":"Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST Austria, 28p.","mla":"Henzinger, Thomas A., et al. <i>Synchronizing the Asynchronous</i>. IST Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:IST-2018-853-v2-2\">10.15479/AT:IST-2018-853-v2-2</a>.","short":"T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST Austria, 2017.","ama":"Henzinger TA, Kragl B, Qadeer S. <i>Synchronizing the Asynchronous</i>. IST Austria; 2017. doi:<a href=\"https://doi.org/10.15479/AT:IST-2018-853-v2-2\">10.15479/AT:IST-2018-853-v2-2</a>","apa":"Henzinger, T. A., Kragl, B., &#38; Qadeer, S. (2017). <i>Synchronizing the asynchronous</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2018-853-v2-2\">https://doi.org/10.15479/AT:IST-2018-853-v2-2</a>"},"alternative_title":["IST Austria Technical Report"],"year":"2017","oa_version":"Published Version","has_accepted_license":"1","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"}],"type":"technical_report","day":"04","oa":1,"publisher":"IST Austria","publication_status":"published","status":"public","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:47:30Z","page":"28","_id":"6426","abstract":[{"text":"Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent asynchronous computation threads. We show that specifications and correctness proofs for asynchronous programs can be structured by introducing the fiction, for proof purposes, that intermediate, non-quiescent states of asynchronous operations can be ignored. Then, the task of specification becomes relatively simple and the task of verification can be naturally decomposed into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure of an asynchronous program, the atomic effect of non-atomic operations and the synchronous effect of asynchronous operations. This structuring of specifications and proofs corresponds to the introduction of multiple layers of stepwise refinement for asynchronous programs. We present the first proof rule, called synchronization, to reduce asynchronous invocations on a lower layer to synchronous invocations on a higher layer. We implemented our proof method in CIVL and evaluated it on a collection of benchmark programs.","lang":"eng"}],"date_created":"2019-05-13T08:15:55Z","date_published":"2017-08-04T00:00:00Z","file":[{"date_updated":"2020-07-14T12:47:30Z","access_level":"open_access","checksum":"b48d42725182d7ca10107a118815f4cf","file_name":"main(1).pdf","file_size":971347,"creator":"dernst","date_created":"2019-05-13T08:14:44Z","content_type":"application/pdf","file_id":"6431","relation":"main_file"}],"month":"08"},{"page":"116 - 132","date_created":"2018-12-11T11:47:41Z","month":"09","publisher":"Springer","status":"public","department":[{"_id":"ToHe"}],"quality_controlled":"1","title":"Conic abstractions for hybrid systems","conference":{"end_date":"2017-09-07","start_date":"2017-09-05","name":"FORMATS: Formal Modelling and Analysis of Timed Systems","location":"Berlin, Germany"},"citation":{"short":"S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017, pp. 116–132.","apa":"Bogomolov, S., Giacobbe, M., Henzinger, T. A., &#38; Kong, H. (2017). Conic abstractions for hybrid systems (Vol. 10419, pp. 116–132). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">https://doi.org/10.1007/978-3-319-65765-3_7</a>","ama":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid systems. In: Vol 10419. Springer; 2017:116-132. doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">10.1007/978-3-319-65765-3_7</a>","ieee":"S. Bogomolov, M. Giacobbe, T. A. Henzinger, and H. Kong, “Conic abstractions for hybrid systems,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 116–132.","ista":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. 2017. Conic abstractions for hybrid systems. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 116–132.","chicago":"Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic Abstractions for Hybrid Systems,” 10419:116–32. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">https://doi.org/10.1007/978-3-319-65765-3_7</a>.","mla":"Bogomolov, Sergiy, et al. <i>Conic Abstractions for Hybrid Systems</i>. Vol. 10419, Springer, 2017, pp. 116–32, doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">10.1007/978-3-319-65765-3_7</a>."},"author":[{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","last_name":"Kong","first_name":"Hui","full_name":"Kong, Hui"}],"type":"conference","alternative_title":["LNCS"],"day":"01","related_material":{"record":[{"relation":"dissertation_contains","id":"6894","status":"public"}]},"project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"doi":"10.1007/978-3-319-65765-3_7","ddc":["005"],"language":[{"iso":"eng"}],"_id":"647","abstract":[{"lang":"eng","text":"Despite researchers’ efforts in the last couple of decades, reachability analysis is still a challenging problem even for linear hybrid systems. Among the existing approaches, the most practical ones are mainly based on bounded-time reachable set over-approximations. For the purpose of unbounded-time analysis, one important strategy is to abstract the original system and find an invariant for the abstraction. In this paper, we propose an approach to constructing a new kind of abstraction called conic abstraction for affine hybrid systems, and to computing reachable sets based on this abstraction. The essential feature of a conic abstraction is that it partitions the state space of a system into a set of convex polyhedral cones which is derived from a uniform conic partition of the derivative space. Such a set of polyhedral cones is able to cut all trajectories of the system into almost straight segments so that every segment of a reach pipe in a polyhedral cone tends to be straight as well, and hence can be over-approximated tightly by polyhedra using similar techniques as HyTech or PHAVer. In particular, for diagonalizable affine systems, our approach can guarantee to find an invariant for unbounded reachable sets, which is beyond the capability of bounded-time reachability analysis tools. We implemented the approach in a tool and experiments on benchmarks show that our approach is more powerful than SpaceEx and PHAVer in dealing with diagonalizable systems."}],"date_published":"2017-09-01T00:00:00Z","file":[{"date_created":"2018-12-12T10:12:38Z","relation":"main_file","file_id":"4956","content_type":"application/pdf","access_level":"open_access","date_updated":"2020-07-14T12:47:31Z","checksum":"faf546914ba29bcf9974ee36b6b16750","file_size":3806864,"creator":"system","file_name":"IST-2017-831-v1+1_main.pdf"}],"oa":1,"publication_status":"published","pubrep_id":"831","volume":"10419 ","file_date_updated":"2020-07-14T12:47:31Z","has_accepted_license":"1","year":"2017","oa_version":"Submitted Version","publist_id":"7129","publication_identifier":{"isbn":["978-331965764-6"]},"scopus_import":1,"date_updated":"2023-09-07T12:53:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854","name":"IST Austria Open Access Fund"}],"related_material":{"record":[{"relation":"earlier_version","id":"1729","status":"public"}]},"language":[{"iso":"eng"}],"doi":"10.1007/s10703-016-0256-5","ddc":["000"],"citation":{"short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, Formal Methods in System Design 50 (2017) 97–139.","ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. 2017;50(2-3):97-139. doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2017). From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>.","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2017. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods in System Design. 50(2–3), 97–139.","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3. Springer, pp. 97–139, 2017.","mla":"Cerny, Pavol, et al. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3, Springer, 2017, pp. 97–139, doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>."},"ec_funded":1,"title":"From non-preemptive to preemptive scheduling using synchronization synthesis","day":"01","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny"},{"first_name":"Edmund","full_name":"Clarke, Edmund","last_name":"Clarke"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ryzhyk","first_name":"Leonid","full_name":"Ryzhyk, Leonid"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","first_name":"Roopsha","last_name":"Samanta"},{"id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","last_name":"Tarrach","first_name":"Thorsten","full_name":"Tarrach, Thorsten"}],"type":"journal_article","publisher":"Springer","isi":1,"publication":"Formal Methods in System Design","department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","intvolume":"        50","page":"97 - 139","month":"06","date_created":"2018-12-11T11:51:27Z","scopus_import":"1","external_id":{"isi":["000399888900001"]},"date_updated":"2023-09-20T11:13:51Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"5929","oa_version":"Published Version","year":"2017","has_accepted_license":"1","publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:44:44Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"pubrep_id":"656","volume":50,"article_processing_charge":"No","issue":"2-3","file":[{"date_updated":"2020-07-14T12:44:44Z","access_level":"open_access","checksum":"1163dfd997e8212c789525d4178b1653","file_name":"IST-2016-656-v1+1_s10703-016-0256-5.pdf","file_size":1416170,"creator":"system","date_created":"2018-12-12T10:13:05Z","content_type":"application/pdf","file_id":"4985","relation":"main_file"}],"_id":"1338","date_published":"2017-06-01T00:00:00Z","abstract":[{"lang":"eng","text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively."}]},{"publist_id":"5898","has_accepted_license":"1","year":"2017","oa_version":"Published Version","scopus_import":"1","external_id":{"isi":["000414343200003"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2025-05-28T11:57:04Z","publication_identifier":{"issn":["00015903"]},"article_processing_charge":"No","issue":"8","file":[{"file_size":755241,"creator":"dernst","file_name":"2017_ActaInformatica_Giacobbe.pdf","access_level":"open_access","date_updated":"2020-07-14T12:44:46Z","checksum":"4e661d9135d7f8c342e8e258dee76f3e","relation":"main_file","file_id":"5841","content_type":"application/pdf","date_created":"2019-01-17T15:57:29Z"}],"_id":"1351","date_published":"2017-12-01T00:00:00Z","abstract":[{"lang":"eng","text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights."}],"publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:44:46Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"pubrep_id":"649","volume":54,"citation":{"apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2017). Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. 2017;54(8):765-787. doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787.","mla":"Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>.","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking the evolution of gene regulatory networks,” <i>Acta Informatica</i>, vol. 54, no. 8. Springer, pp. 765–787, 2017.","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>."},"ec_funded":1,"title":"Model checking the evolution of gene regulatory networks","day":"01","author":[{"first_name":"Mirco","full_name":"Giacobbe, Mirco","last_name":"Giacobbe","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Calin C","full_name":"Guet, Calin C","last_name":"Guet","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"orcid":"0000-0003-2361-3953","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","last_name":"Paixao","first_name":"Tiago","full_name":"Paixao, Tiago"},{"full_name":"Petrov, Tatjana","first_name":"Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"type":"journal_article","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FP7","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","grant_number":"618091"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"name":"Limits to selection in biology and in evolutionary computation","grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"related_material":{"record":[{"id":"1835","relation":"earlier_version","status":"public"}]},"language":[{"iso":"eng"}],"ddc":["006","576"],"doi":"10.1007/s00236-016-0278-x","page":"765 - 787","month":"12","date_created":"2018-12-11T11:51:32Z","publisher":"Springer","isi":1,"publication":"Acta Informatica","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"quality_controlled":"1","intvolume":"        54","status":"public"}]