[{"publisher":"Springer","status":"public","intvolume":"        18","department":[{"_id":"ToHe"}],"quality_controlled":"1","publication":"International Journal on Software Tools for Technology Transfer","page":"449 - 467","date_created":"2018-12-11T11:53:34Z","month":"08","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"ddc":["000"],"doi":"10.1007/s10009-015-0393-y","language":[{"iso":"eng"}],"title":"Guided search for hybrid systems based on coarse-grained space abstractions","ec_funded":1,"citation":{"mla":"Bogomolov, Sergiy, et al. “Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 18, no. 4, Springer, 2016, pp. 449–67, doi:<a href=\"https://doi.org/10.1007/s10009-015-0393-y\">10.1007/s10009-015-0393-y</a>.","chicago":"Bogomolov, Sergiy, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor Johnson, Hamed Ladan, Andreas Podelski, and Martin Wehrle. “Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer, 2016. <a href=\"https://doi.org/10.1007/s10009-015-0393-y\">https://doi.org/10.1007/s10009-015-0393-y</a>.","ieee":"S. Bogomolov <i>et al.</i>, “Guided search for hybrid systems based on coarse-grained space abstractions,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 18, no. 4. Springer, pp. 449–467, 2016.","ista":"Bogomolov S, Donzé A, Frehse G, Grosu R, Johnson T, Ladan H, Podelski A, Wehrle M. 2016. Guided search for hybrid systems based on coarse-grained space abstractions. International Journal on Software Tools for Technology Transfer. 18(4), 449–467.","ama":"Bogomolov S, Donzé A, Frehse G, et al. Guided search for hybrid systems based on coarse-grained space abstractions. <i>International Journal on Software Tools for Technology Transfer</i>. 2016;18(4):449-467. doi:<a href=\"https://doi.org/10.1007/s10009-015-0393-y\">10.1007/s10009-015-0393-y</a>","apa":"Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T., Ladan, H., … Wehrle, M. (2016). Guided search for hybrid systems based on coarse-grained space abstractions. <i>International Journal on Software Tools for Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s10009-015-0393-y\">https://doi.org/10.1007/s10009-015-0393-y</a>","short":"S. Bogomolov, A. Donzé, G. Frehse, R. Grosu, T. Johnson, H. Ladan, A. Podelski, M. Wehrle, International Journal on Software Tools for Technology Transfer 18 (2016) 449–467."},"type":"journal_article","author":[{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov"},{"first_name":"Alexandre","full_name":"Donzé, Alexandre","last_name":"Donzé"},{"first_name":"Goran","full_name":"Frehse, Goran","last_name":"Frehse"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"},{"full_name":"Johnson, Taylor","first_name":"Taylor","last_name":"Johnson"},{"first_name":"Hamed","full_name":"Ladan, Hamed","last_name":"Ladan"},{"last_name":"Podelski","full_name":"Podelski, Andreas","first_name":"Andreas"},{"first_name":"Martin","full_name":"Wehrle, Martin","last_name":"Wehrle"}],"day":"01","oa":1,"publication_status":"published","license":"https://creativecommons.org/licenses/by/4.0/","volume":18,"pubrep_id":"457","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)"},"file_date_updated":"2020-07-14T12:45:13Z","issue":"4","article_processing_charge":"Yes (via OA deal)","date_published":"2016-08-01T00:00:00Z","_id":"1705","abstract":[{"lang":"eng","text":"Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based on coarse-grained space abstractions for guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential."}],"file":[{"content_type":"application/pdf","file_id":"5146","relation":"main_file","date_created":"2018-12-12T10:15:26Z","file_name":"IST-2016-457-v1+1_s10009-015-0393-y.pdf","file_size":2296522,"creator":"system","checksum":"31561d7705599a9bd4ea816accc0752e","date_updated":"2020-07-14T12:45:13Z","access_level":"open_access"}],"date_updated":"2021-01-12T06:52:38Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"oa_version":"Published Version","has_accepted_license":"1","year":"2016","publist_id":"5431"},{"oa_version":"None","year":"2016","alternative_title":["Proceedings International Conference on Software Engineering"],"type":"conference","author":[{"first_name":"Yu","full_name":"Jiang, Yu","last_name":"Jiang"},{"full_name":"Liu, Han","first_name":"Han","last_name":"Liu"},{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui","full_name":"Kong, Hui","last_name":"Kong"},{"full_name":"Wang, Rui","first_name":"Rui","last_name":"Wang"},{"last_name":"Hosseini","first_name":"Mohamad","full_name":"Hosseini, Mohamad"},{"full_name":"Sun, Jiaguang","first_name":"Jiaguang","last_name":"Sun"},{"last_name":"Sha","full_name":"Sha, Lui","first_name":"Lui"}],"publist_id":"7341","day":"14","conference":{"end_date":"2016-05-22","start_date":"2016-05-14","name":"ICSE: International Conference on Software Engineering","location":"Austin, TX, USA"},"title":"Use runtime verification to improve the quality of medical care practice","citation":{"chicago":"Jiang, Yu, Han Liu, Hui Kong, Rui Wang, Mohamad Hosseini, Jiaguang Sun, and Lui Sha. “Use Runtime Verification to Improve the Quality of Medical Care Practice.” In <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>, 112–21. IEEE, 2016. <a href=\"https://doi.org/10.1145/2889160.2889233\">https://doi.org/10.1145/2889160.2889233</a>.","ieee":"Y. Jiang <i>et al.</i>, “Use runtime verification to improve the quality of medical care practice,” in <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>, Austin, TX, USA, 2016, pp. 112–121.","ista":"Jiang Y, Liu H, Kong H, Wang R, Hosseini M, Sun J, Sha L. 2016. Use runtime verification to improve the quality of medical care practice. Proceedings of the 38th International Conference on Software Engineering Companion . ICSE: International Conference on Software Engineering, Proceedings International Conference on Software Engineering, , 112–121.","mla":"Jiang, Yu, et al. “Use Runtime Verification to Improve the Quality of Medical Care Practice.” <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>, IEEE, 2016, pp. 112–21, doi:<a href=\"https://doi.org/10.1145/2889160.2889233\">10.1145/2889160.2889233</a>.","short":"Y. Jiang, H. Liu, H. Kong, R. Wang, M. Hosseini, J. Sun, L. Sha, in:, Proceedings of the 38th International Conference on Software Engineering Companion , IEEE, 2016, pp. 112–121.","ama":"Jiang Y, Liu H, Kong H, et al. Use runtime verification to improve the quality of medical care practice. In: <i>Proceedings of the 38th International Conference on Software Engineering Companion </i>. IEEE; 2016:112-121. doi:<a href=\"https://doi.org/10.1145/2889160.2889233\">10.1145/2889160.2889233</a>","apa":"Jiang, Y., Liu, H., Kong, H., Wang, R., Hosseini, M., Sun, J., &#38; Sha, L. (2016). Use runtime verification to improve the quality of medical care practice. In <i>Proceedings of the 38th International Conference on Software Engineering Companion </i> (pp. 112–121). Austin, TX, USA: IEEE. <a href=\"https://doi.org/10.1145/2889160.2889233\">https://doi.org/10.1145/2889160.2889233</a>"},"doi":"10.1145/2889160.2889233","date_updated":"2021-01-12T08:00:55Z","language":[{"iso":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"acknowledgement":"This work is supported by NSF CNS 13-30077, NSF CNS 13-29886, NSF CNS 15-45002, and NSFC 61303014.\r\nThe authors thank Dr.  Bobby and Dr.  Hill at Carle Hospital, Urbana, IL for their help with the discussion on medical  knowledge.\r\n\r\n","_id":"479","date_published":"2016-05-14T00:00:00Z","abstract":[{"text":"Clinical guidelines and decision support systems (DSS) play an important role in daily practices of medicine. Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care. During the collaboration with Carle hospital to develop a DSS, we identify that, for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties in guidelines, which brings new challenges to current simulation based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios, and applied the proposed technique to assist existing DSS. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital","lang":"eng"}],"date_created":"2018-12-11T11:46:42Z","month":"05","page":"112 - 121","status":"public","department":[{"_id":"ToHe"}],"quality_controlled":"1","publication":"Proceedings of the 38th International Conference on Software Engineering Companion ","publication_status":"published","publisher":"IEEE"},{"department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","publisher":"ACM","month":"01","date_created":"2018-12-11T11:52:01Z","page":"400 - 415","language":[{"iso":"eng"}],"doi":"10.1145/2837614.2837650","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"acknowledgement":"Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192 and FA8650-15-C-7564) and NSF (Grant CCF-1138967). ","day":"11","author":[{"first_name":"Cezara","full_name":"Dragoi, Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Zufferey, Damien","first_name":"Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"type":"conference","alternative_title":["ACM SIGPLAN Notices"],"citation":{"short":"C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, pp. 400–415.","ama":"Dragoi C, Henzinger TA, Zufferey D. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. In: Vol 20-22. ACM; 2016:400-415. doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>","apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2016). PSYNC: A partially synchronous language for fault-tolerant distributed algorithms (Vol. 20–22, pp. 400–415). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms,” 20–22:400–415. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>.","ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “PSYNC: A partially synchronous language for fault-tolerant distributed algorithms,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 400–415.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2016. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 20–22, 400–415.","mla":"Dragoi, Cezara, et al. <i>PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms</i>. Vol. 20–22, ACM, 2016, pp. 400–15, doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>."},"ec_funded":1,"title":"PSYNC: A partially synchronous language for fault-tolerant distributed algorithms","conference":{"location":"St. Petersburg, FL, USA","name":"POPL: Principles of Programming Languages","start_date":"2016-01-20","end_date":"2016-01-22"},"volume":"20-22","publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://hal.inria.fr/hal-01251199/"}],"_id":"1439","abstract":[{"text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.","lang":"eng"}],"date_published":"2016-01-11T00:00:00Z","scopus_import":1,"date_updated":"2021-01-12T06:50:45Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publist_id":"5759","oa_version":"Preprint","year":"2016"},{"publisher":"Springer","intvolume":"      9271","status":"public","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"quality_controlled":"1","page":"173 - 191","date_created":"2018-12-11T11:52:31Z","month":"01","acknowledgement":"This research was supported by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. 291734, and the SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2_148797.","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"doi":"10.1007/978-3-319-26916-0_10","language":[{"iso":"eng"}],"conference":{"location":"Madrid, Spain","start_date":"2015-09-04","end_date":"2015-09-05","name":"HSB: Hybrid Systems Biology"},"title":"Efficient reduction of kappa models by static inspection of the rule-set","ec_funded":1,"citation":{"chicago":"Beica, Andreea, Calin C Guet, and Tatjana Petrov. “Efficient Reduction of Kappa Models by Static Inspection of the Rule-Set,” 9271:173–91. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">https://doi.org/10.1007/978-3-319-26916-0_10</a>.","ieee":"A. Beica, C. C. Guet, and T. Petrov, “Efficient reduction of kappa models by static inspection of the rule-set,” presented at the HSB: Hybrid Systems Biology, Madrid, Spain, 2016, vol. 9271, pp. 173–191.","ista":"Beica A, Guet CC, Petrov T. 2016. Efficient reduction of kappa models by static inspection of the rule-set. HSB: Hybrid Systems Biology, LNCS, vol. 9271, 173–191.","mla":"Beica, Andreea, et al. <i>Efficient Reduction of Kappa Models by Static Inspection of the Rule-Set</i>. Vol. 9271, Springer, 2016, pp. 173–91, doi:<a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">10.1007/978-3-319-26916-0_10</a>.","short":"A. Beica, C.C. Guet, T. Petrov, in:, Springer, 2016, pp. 173–191.","ama":"Beica A, Guet CC, Petrov T. Efficient reduction of kappa models by static inspection of the rule-set. In: Vol 9271. Springer; 2016:173-191. doi:<a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">10.1007/978-3-319-26916-0_10</a>","apa":"Beica, A., Guet, C. C., &#38; Petrov, T. (2016). Efficient reduction of kappa models by static inspection of the rule-set (Vol. 9271, pp. 173–191). Presented at the HSB: Hybrid Systems Biology, Madrid, Spain: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">https://doi.org/10.1007/978-3-319-26916-0_10</a>"},"alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Beica","full_name":"Beica, Andreea","first_name":"Andreea"},{"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":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"day":"10","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1501.00440"}],"oa":1,"publication_status":"published","volume":9271,"date_published":"2016-01-10T00:00:00Z","_id":"1524","abstract":[{"text":"When designing genetic circuits, the typical primitives used in major existing modelling formalisms are gene interaction graphs, where edges between genes denote either an activation or inhibition relation. However, when designing experiments, it is important to be precise about the low-level mechanistic details as to how each such relation is implemented. The rule-based modelling language Kappa allows to unambiguously specify mechanistic details such as DNA binding sites, dimerisation of transcription factors, or co-operative interactions. Such a detailed description comes with complexity and computationally costly executions. We propose a general method for automatically transforming a rule-based program, by eliminating intermediate species and adjusting the rate constants accordingly. To the best of our knowledge, we show the first automated reduction of rule-based models based on equilibrium approximations.\r\nOur algorithm is an adaptation of an existing algorithm, which was designed for reducing reaction-based programs; our version of the algorithm scans the rule-based Kappa model in search for those interaction patterns known to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional checks are then performed in order to verify if the reduction is meaningful in the context of the full model. The reduced model is efficiently obtained by static inspection over the rule-set. The tool is tested on a detailed rule-based model of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has 11 rules and 5 agents, and provides a dramatic reduction in simulation time of several orders of magnitude.","lang":"eng"}],"date_updated":"2021-01-12T06:51:22Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"year":"2016","oa_version":"Preprint","publist_id":"5649"},{"date_published":"2016-01-01T00:00:00Z","_id":"1526","abstract":[{"lang":"eng","text":"We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of uncertain inputs and formalize their robustness using the analytic notion of Lipschitz continuity: a timed I/O system is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions over timed words such as the timed version of the Manhattan distance and the Skorokhod distance. We consider two models of timed I/O systems — timed transducers and asynchronous sequential circuits. We show that K-robustness of timed transducers can be decided in polynomial space under certain conditions. For asynchronous sequential circuits, we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete letter-to-letter transducers and show PSpace-completeness of the problem."}],"volume":9583,"publication_status":"published","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1506.01233"}],"oa":1,"publist_id":"5647","oa_version":"Preprint","year":"2016","scopus_import":1,"date_updated":"2021-01-12T06:51:23Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"01","date_created":"2018-12-11T11:52:32Z","page":"250 - 267","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","intvolume":"      9583","publisher":"Springer","day":"01","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","first_name":"Roopsha","last_name":"Samanta"}],"type":"conference","alternative_title":["LNCS"],"citation":{"ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of timed I/O systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 250–267.","ista":"Henzinger TA, Otop J, Samanta R. 2016. Lipschitz robustness of timed I/O systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 250–267.","chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Timed I/O Systems,” 9583:250–67. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>.","mla":"Henzinger, Thomas A., et al. <i>Lipschitz Robustness of Timed I/O Systems</i>. Vol. 9583, Springer, 2016, pp. 250–67, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>.","short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2016). Lipschitz robustness of timed I/O systems (Vol. 9583, pp. 250–267). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems. In: Vol 9583. Springer; 2016:250-267. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>"},"ec_funded":1,"title":"Lipschitz robustness of timed I/O systems","conference":{"location":"St. Petersburg, FL, USA","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2016-01-19","start_date":"2016-01-17"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-49122-5_12","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543."},{"date_published":"2016-08-31T00:00:00Z","_id":"1335","abstract":[{"lang":"eng","text":"In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted ω-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted ω-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted ω-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties."}],"volume":9837,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"oa":1,"publication_status":"published","year":"2016","oa_version":"Preprint","publist_id":"5932","date_updated":"2021-01-12T06:49:58Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"date_created":"2018-12-11T11:51:26Z","month":"08","page":"23 - 38","status":"public","intvolume":"      9837","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","alternative_title":["LNCS"],"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","day":"31","conference":{"location":"Edinburgh, United Kingdom","end_date":"2016-09-10","start_date":"2016-09-08","name":"SAS: Static Analysis Symposium"},"title":"Quantitative monitor automata","ec_funded":1,"citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.","mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Monitor Automata</i>. Vol. 9837, Springer, 2016, pp. 23–38, doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,” presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016, vol. 9837, pp. 23–38.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Monitor Automata,” 9837:23–38. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>."},"doi":"10.1007/978-3-662-53413-7_2","language":[{"iso":"eng"}],"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}]},{"date_created":"2018-12-11T11:51:28Z","month":"09","page":"153 - 166","intvolume":"      9928","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"}],"publisher":"Springer","alternative_title":["LNCS"],"type":"conference","author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"day":"01","conference":{"location":"Liverpool, United Kingdom","start_date":"2016-09-19","end_date":"2016-09-21","name":"SAGT: Symposium on Algorithmic Game Theory"},"title":"Dynamic resource allocation games","ec_funded":1,"citation":{"mla":"Avni, Guy, et al. <i>Dynamic Resource Allocation Games</i>. Vol. 9928, Springer, 2016, pp. 153–66, doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>.","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 153–166.","ista":"Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games,” 9928:153–66. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>.","apa":"Avni, G., Henzinger, T. A., &#38; Kupferman, O. (2016). Dynamic resource allocation games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In: Vol 9928. Springer; 2016:153-166. doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>","short":"G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166."},"ddc":["000"],"doi":"10.1007/978-3-662-53354-3_13","language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the European Research Council (ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"related_material":{"record":[{"id":"6761","relation":"later_version","status":"public"}]},"abstract":[{"text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.","lang":"eng"}],"_id":"1341","date_published":"2016-09-01T00:00:00Z","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:44:45Z","checksum":"0825eefd4e22774f6f62cb7d7389b05a","file_size":243458,"creator":"system","file_name":"IST-2016-645-v1+1_sagt-cr.pdf","date_created":"2018-12-12T10:14:22Z","relation":"main_file","file_id":"5073","content_type":"application/pdf"}],"volume":9928,"pubrep_id":"645","file_date_updated":"2020-07-14T12:44:45Z","oa":1,"publication_status":"published","has_accepted_license":"1","year":"2016","oa_version":"Preprint","publist_id":"5926","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-08-17T13:52:49Z","scopus_import":1},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:50:21Z","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-41540-6_21","citation":{"mla":"D’Antoni, Loris, et al. <i>QLOSE: Program Repair with Quantitative Objectives</i>. Vol. 9780, Springer, 2016, pp. 383–401, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>.","ieee":"L. D’Antoni, R. Samanta, and R. Singh, “QLOSE: Program repair with quantitative objectives,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 383–401.","ista":"D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.","chicago":"D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair with Quantitative Objectives,” 9780:383–401. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>.","apa":"D’Antoni, L., Samanta, R., &#38; Singh, R. (2016). QLOSE: Program repair with quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>","ama":"D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives. In: Vol 9780. Springer; 2016:383-401. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>","short":"L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401."},"ec_funded":1,"title":"QLOSE: Program repair with quantitative objectives","conference":{"location":"Toronto, Canada","start_date":"2016-07-17","end_date":"2016-07-23","name":"CAV: Computer Aided Verification"},"publist_id":"5819","day":"13","type":"conference","author":[{"full_name":"D'Antoni, Loris","first_name":"Loris","last_name":"D'Antoni"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","full_name":"Samanta, Roopsha","first_name":"Roopsha"},{"last_name":"Singh","full_name":"Singh, Rishabh","first_name":"Rishabh"}],"alternative_title":["LNCS"],"oa_version":"None","year":"2016","publisher":"Springer","publication_status":"published","department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","intvolume":"      9780","volume":9780,"page":"383 - 401","month":"07","date_created":"2018-12-11T11:51:45Z","_id":"1390","date_published":"2016-07-13T00:00:00Z","abstract":[{"text":"The goal of automatic program repair is to identify a set of syntactic changes that can turn a program that is incorrect with respect\r\nto a given specification into a correct one. Existing program repair techniques typically aim to find any program that meets the given specification. Such “best-effort” strategies can end up generating a program that is quite different from the original one. Novel techniques have been proposed to compute syntactically minimal program fixes, but the smallest syntactic fix to a program can still significantly alter the original program’s behaviour. We propose a new approach to program repair based on program distances, which can quantify changes not only to the program syntax but also to the program semantics. We call this the quantitative program repair problem where the “optimal” repair is derived using multiple distances. We implement a solution to the quantitative repair\r\nproblem in a prototype tool called Qlose\r\n(Quantitatively close), using the program synthesizer Sketch. We evaluate the effectiveness of different distances in obtaining desirable repairs by evaluating\r\nQlose on programs taken from educational tools such as CodeHunt and edX.","lang":"eng"}]},{"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T11:58:33Z","scopus_import":1,"oa_version":"Preprint","year":"2016","publist_id":"5818","volume":9780,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1603.06850"}],"oa":1,"publication_status":"published","_id":"1391","date_published":"2016-07-13T00:00:00Z","abstract":[{"text":"We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as &quot;the first array cell contains the array length,&quot; and &quot;the array contains equally many minimal and maximal elements.&quot; These properties cannot be expressed in quantified fragments of the theory of arrays, nor in the theory of concatenation. Using reduction to counter machines, we show that the satisfiability problem of AFL is PSPACE-complete, and with a natural restriction the complexity decreases to NP. We also show that adding either universal quantifiers or concatenation leads to undecidability.\r\nAFL contains terms that fold a function over an array. We demonstrate that folding, a well-known concept from functional languages, allows us to concisely summarize loops that count over arrays, which occurs frequently in real-life programs. We provide a tool that can discharge proof obligations in AFL, and we demonstrate on practical examples that our decision procedure can solve a broad range of problems in symbolic testing and program verification.","lang":"eng"}],"doi":"10.1007/978-3-319-41540-6_13","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1155"}]},"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"alternative_title":["LNCS"],"type":"conference","author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","last_name":"Kupriyanov","full_name":"Kupriyanov, Andrey","first_name":"Andrey"}],"day":"13","conference":{"start_date":"2016-07-17","end_date":"2016-07-23","name":"CAV: Computer Aided Verification","location":"Toronto, Canada"},"title":"Array folds logic","ec_funded":1,"citation":{"ista":"Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer Aided Verification, LNCS, vol. 9780, 230–248.","ieee":"P. Daca, T. A. Henzinger, and A. Kupriyanov, “Array folds logic,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 230–248.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds Logic,” 9780:230–48. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">https://doi.org/10.1007/978-3-319-41540-6_13</a>.","mla":"Daca, Przemyslaw, et al. <i>Array Folds Logic</i>. Vol. 9780, Springer, 2016, pp. 230–48, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">10.1007/978-3-319-41540-6_13</a>.","short":"P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248.","apa":"Daca, P., Henzinger, T. A., &#38; Kupriyanov, A. (2016). Array folds logic (Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">https://doi.org/10.1007/978-3-319-41540-6_13</a>","ama":"Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer; 2016:230-248. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_13\">10.1007/978-3-319-41540-6_13</a>"},"status":"public","intvolume":"      9780","department":[{"_id":"ToHe"}],"quality_controlled":"1","publisher":"Springer","date_created":"2018-12-11T11:51:45Z","month":"07","page":"230 - 248"},{"date_created":"2018-12-11T11:51:55Z","_id":"1421","abstract":[{"lang":"eng","text":"Hybridization methods enable the analysis of hybrid automata with complex, nonlinear dynamics through a sound abstraction process. Complex dynamics are converted to simpler ones with added noise, and then analysis is done using a reachability method for the simpler dynamics. Several such recent approaches advocate that only &quot;dynamic&quot; hybridization techniquesi.e., those where the dynamics are abstracted on-The-fly during a reachability computation are effective. In this paper, we demonstrate this is not the case, and create static hybridization methods that are more scalable than earlier approaches. The main insight in our approach is that quick, numeric simulations can be used to guide the process, eliminating the need for an exponential number of hybridization domains. Transitions between domains are generally timetriggered, avoiding accumulated error from geometric intersections. We enhance our static technique by combining time-Triggered transitions with occasional space-Triggered transitions, and demonstrate the benefits of the combined approach in what we call mixed-Triggered hybridization. Finally, error modes are inserted to confirm that the reachable states stay within the hybridized regions. The developed techniques can scale to higher dimensions than previous static approaches, while enabling the parallelization of the main performance bottleneck for many dynamic hybridization approaches: The nonlinear optimization required for sound dynamics abstraction. We implement our method as a model transformation pass in the HYST tool, and perform reachability analysis and evaluation using an unmodified version of SpaceEx on nonlinear models with up to six dimensions."}],"date_published":"2016-04-11T00:00:00Z","month":"04","page":"155 - 164","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","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","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Johnson","first_name":"Taylor","full_name":"Johnson, Taylor"},{"full_name":"Prakash, Pradyot","first_name":"Pradyot","last_name":"Prakash"}],"oa_version":"None","year":"2016","publist_id":"5786","day":"11","title":"Scalable static hybridization methods for analysis of nonlinear systems","conference":{"end_date":"2016-04-14","start_date":"2016-04-12","name":"HSCC 2016: International Conference on Hybrid Systems: Computation and Control","location":"Vienna, Austria"},"citation":{"short":"S. Bak, S. Bogomolov, T.A. Henzinger, T. Johnson, P. Prakash, in:, Springer, 2016, pp. 155–164.","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., Johnson, T., &#38; Prakash, P. (2016). Scalable static hybridization methods for analysis of nonlinear systems (pp. 155–164). Presented at the HSCC 2016: International Conference on Hybrid Systems: Computation and Control, Vienna, Austria: Springer. <a href=\"https://doi.org/10.1145/2883817.2883837\">https://doi.org/10.1145/2883817.2883837</a>","ama":"Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. Scalable static hybridization methods for analysis of nonlinear systems. In: Springer; 2016:155-164. doi:<a href=\"https://doi.org/10.1145/2883817.2883837\">10.1145/2883817.2883837</a>","ista":"Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. 2016. Scalable static hybridization methods for analysis of nonlinear systems. HSCC 2016: International Conference on Hybrid Systems: Computation and Control, 155–164.","ieee":"S. Bak, S. Bogomolov, T. A. Henzinger, T. Johnson, and P. Prakash, “Scalable static hybridization methods for analysis of nonlinear systems,” presented at the HSCC 2016: International Conference on Hybrid Systems: Computation and Control, Vienna, Austria, 2016, pp. 155–164.","chicago":"Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, Taylor Johnson, and Pradyot Prakash. “Scalable Static Hybridization Methods for Analysis of Nonlinear Systems,” 155–64. Springer, 2016. <a href=\"https://doi.org/10.1145/2883817.2883837\">https://doi.org/10.1145/2883817.2883837</a>.","mla":"Bak, Stanley, et al. <i>Scalable Static Hybridization Methods for Analysis of Nonlinear Systems</i>. Springer, 2016, pp. 155–64, doi:<a href=\"https://doi.org/10.1145/2883817.2883837\">10.1145/2883817.2883837</a>."},"ec_funded":1,"doi":"10.1145/2883817.2883837","scopus_import":1,"date_updated":"2021-01-12T06:50:37Z","language":[{"iso":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}]},{"page":"757 - 763","date_created":"2018-12-11T11:50:42Z","month":"11","publisher":"Springer","status":"public","intvolume":"      9995","quality_controlled":"1","department":[{"_id":"ToHe"}],"title":"Safety assured formal model driven design of the multifunction vehicle bus controller","conference":{"location":"Limassol, Cyprus","start_date":"2016-11-09","end_date":"2016-11-11","name":"FM: International Symposium on Formal Methods"},"citation":{"chicago":"Jiang, Yu, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller,” 9995:757–63. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">https://doi.org/10.1007/978-3-319-48989-6_47</a>.","ista":"Jiang Y, Liu H, Song H, Kong H, Gu M, Sun J, Sha L. 2016. Safety assured formal model driven design of the multifunction vehicle bus controller. FM: International Symposium on Formal Methods, LNCS, vol. 9995, 757–763.","ieee":"Y. Jiang <i>et al.</i>, “Safety assured formal model driven design of the multifunction vehicle bus controller,” presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus, 2016, vol. 9995, pp. 757–763.","mla":"Jiang, Yu, et al. <i>Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller</i>. Vol. 9995, Springer, 2016, pp. 757–63, doi:<a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">10.1007/978-3-319-48989-6_47</a>.","short":"Y. Jiang, H. Liu, H. Song, H. Kong, M. Gu, J. Sun, L. Sha, in:, Springer, 2016, pp. 757–763.","ama":"Jiang Y, Liu H, Song H, et al. Safety assured formal model driven design of the multifunction vehicle bus controller. In: Vol 9995. Springer; 2016:757-763. doi:<a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">10.1007/978-3-319-48989-6_47</a>","apa":"Jiang, Y., Liu, H., Song, H., Kong, H., Gu, M., Sun, J., &#38; Sha, L. (2016). Safety assured formal model driven design of the multifunction vehicle bus controller (Vol. 9995, pp. 757–763). Presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-319-48989-6_47\">https://doi.org/10.1007/978-3-319-48989-6_47</a>"},"type":"conference","author":[{"last_name":"Jiang","full_name":"Jiang, Yu","first_name":"Yu"},{"last_name":"Liu","full_name":"Liu, Han","first_name":"Han"},{"full_name":"Song, Houbing","first_name":"Houbing","last_name":"Song"},{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui","full_name":"Kong, Hui","last_name":"Kong"},{"last_name":"Gu","first_name":"Ming","full_name":"Gu, Ming"},{"last_name":"Sun","first_name":"Jiaguang","full_name":"Sun, Jiaguang"},{"last_name":"Sha","full_name":"Sha, Lui","first_name":"Lui"}],"alternative_title":["LNCS"],"day":"08","related_material":{"record":[{"relation":"later_version","id":"434","status":"public"}]},"project":[{"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","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"This research is sponsored in part by NSFC Program (No. 91218302, No. 61527812), National Science and Technology Major Project (No. 2016ZX01038101), Tsinghua University Initiative Scientific Research Program (20131089331), MIIT IT funds (Research and application of TCN key technologies) of China, and the National Key Technology R&D Program (No. 2015BAG14B01-02), Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23.\r\n","ddc":["004"],"doi":"10.1007/978-3-319-48989-6_47","language":[{"iso":"eng"}],"_id":"1205","abstract":[{"lang":"eng","text":"In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network."}],"date_published":"2016-11-08T00:00:00Z","file":[{"relation":"main_file","file_id":"4673","content_type":"application/pdf","date_created":"2018-12-12T10:08:13Z","creator":"system","file_size":281501,"file_name":"IST-2017-783-v1+1_FM-Safety-Assured-Development-of-MVBC.pdf","checksum":"fea0b3fae9a2a42e8bfec59840e30d8c","access_level":"open_access","date_updated":"2020-07-14T12:44:39Z"}],"oa":1,"publication_status":"published","pubrep_id":"783","volume":9995,"file_date_updated":"2020-07-14T12:44:39Z","oa_version":"Submitted Version","has_accepted_license":"1","year":"2016","publist_id":"6144","scopus_import":1,"date_updated":"2023-09-18T08:12:48Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:44:39Z","pubrep_id":"781","volume":9957,"file":[{"date_created":"2018-12-12T10:10:49Z","file_id":"4840","relation":"main_file","content_type":"application/pdf","checksum":"994e164b558c47bacf8dc066dd27c8fc","access_level":"open_access","date_updated":"2020-07-14T12:44:39Z","file_size":683955,"creator":"system","file_name":"IST-2017-781-v1+1_main.pdf"}],"_id":"1227","abstract":[{"text":"Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples.","lang":"eng"}],"date_published":"2016-09-25T00:00:00Z","scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:49:13Z","publist_id":"6107","has_accepted_license":"1","year":"2016","oa_version":"Submitted Version","publisher":"Springer","department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","intvolume":"      9957","page":"128 - 144","month":"09","date_created":"2018-12-11T11:50:49Z","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-47151-8_9","ddc":["005"],"citation":{"apa":"Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang, Y., &#38; Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol. 9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">https://doi.org/10.1007/978-3-319-47151-8_9</a>","ama":"Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine systems. In: Vol 9957. Springer; 2016:128-144. doi:<a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">10.1007/978-3-319-47151-8_9</a>","short":"H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C. Schilling, in:, Springer, 2016, pp. 128–144.","mla":"Kong, Hui, et al. <i>Discrete Abstraction of Multiaffine Systems</i>. Vol. 9957, Springer, 2016, pp. 128–44, doi:<a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">10.1007/978-3-319-47151-8_9</a>.","ieee":"H. Kong <i>et al.</i>, “Discrete abstraction of multiaffine systems,” presented at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.","ista":"Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology, LNCS, vol. 9957, 128–144.","chicago":"Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger, Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,” 9957:128–44. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">https://doi.org/10.1007/978-3-319-47151-8_9</a>."},"title":"Discrete abstraction of multiaffine systems","conference":{"name":"HSB: Hybrid Systems Biology","start_date":"2016-10-20","end_date":"2016-10-21","location":"Grenoble, France"},"day":"25","author":[{"full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Radu","full_name":"Grosu, Radu","last_name":"Grosu"},{"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":"Yu","full_name":"Jiang, Yu","last_name":"Jiang"},{"first_name":"Christian","full_name":"Schilling, Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","alternative_title":["LNCS"]},{"status":"public","intvolume":"      9583","quality_controlled":"1","department":[{"_id":"ToHe"}],"publisher":"Springer","date_created":"2018-12-11T11:50:50Z","month":"01","page":"328 - 347","doi":"10.1007/978-3-662-49122-5_16","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"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"related_material":{"record":[{"id":"1155","relation":"dissertation_contains","status":"public"}]},"acknowledgement":"We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand Michael Tautschnig for help with preparing the experiments. This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","type":"conference","author":[{"full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"alternative_title":["LNCS"],"day":"01","title":"Abstraction-driven concolic testing","conference":{"location":"St. Petersburg, FL, USA","start_date":"2016-01-17","end_date":"2016-01-19","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"citation":{"mla":"Daca, Przemyslaw, et al. <i>Abstraction-Driven Concolic Testing</i>. Vol. 9583, Springer, 2016, pp. 328–47, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>.","chicago":"Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven Concolic Testing,” 9583:328–47. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>.","ieee":"P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.","ista":"Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 328–347.","ama":"Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol 9583. Springer; 2016:328-347. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>","apa":"Daca, P., Gupta, A., &#38; Henzinger, T. A. (2016). Abstraction-driven concolic testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>","short":"P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347."},"ec_funded":1,"volume":9583,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1511.02615"}],"oa":1,"publication_status":"published","_id":"1230","date_published":"2016-01-01T00:00:00Z","abstract":[{"lang":"eng","text":"Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolictesting tool Crest and the model checker CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to Crest from 48% to 63% in the best case, and from 66% to 71% on average."}],"scopus_import":1,"date_updated":"2023-09-07T11:58:33Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","year":"2016","publist_id":"6104"},{"acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant  agreement  267989  (QUAREM),  the  Austrian  Science  Fund  (FWF)  under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation under grant agreement P202/12/G061.","related_material":{"record":[{"relation":"later_version","id":"471","status":"public"},{"status":"public","relation":"dissertation_contains","id":"1155"}]},"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-49674-9_7","ec_funded":1,"citation":{"chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model checking for unbounded temporal properties. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands, 2016, vol. 9636, pp. 112–129.","mla":"Daca, Przemyslaw, et al. <i>Faster Statistical Model Checking for Unbounded Temporal Properties</i>. Vol. 9636, Springer, 2016, pp. 112–29, doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Faster statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>"},"conference":{"location":"Eindhoven, The Netherlands","end_date":"2016-04-08","start_date":"2016-04-02","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"title":"Faster statistical model checking for unbounded temporal properties","day":"01","alternative_title":["LNCS"],"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"full_name":"Petrov, Tatjana","first_name":"Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"type":"conference","publisher":"Springer","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"quality_controlled":"1","status":"public","intvolume":"      9636","page":"112 - 129","month":"01","date_created":"2018-12-11T11:50:51Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T11:58:33Z","scopus_import":1,"publist_id":"6099","oa_version":"Preprint","year":"2016","publication_status":"published","main_file_link":[{"url":"https://arxiv.org/abs/1504.05739","open_access":"1"}],"oa":1,"volume":9636,"_id":"1234","date_published":"2016-01-01T00:00:00Z","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"}]},{"pubrep_id":"780","file_date_updated":"2020-07-14T12:44:41Z","oa":1,"publication_status":"published","date_published":"2016-04-27T00:00:00Z","_id":"1256","abstract":[{"lang":"eng","text":"Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform."}],"file":[{"checksum":"42f0462911cc9957f2356b12fb33b4b6","access_level":"open_access","date_updated":"2020-07-14T12:44:41Z","file_size":1293599,"creator":"system","file_name":"IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf","date_created":"2018-12-12T10:12:31Z","file_id":"4949","relation":"main_file","content_type":"application/pdf"}],"article_number":"7461337","scopus_import":1,"date_updated":"2021-01-12T06:49:26Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","year":"2016","has_accepted_license":"1","publist_id":"6069","status":"public","department":[{"_id":"ToHe"}],"quality_controlled":"1","publisher":"IEEE","date_created":"2018-12-11T11:50:58Z","month":"04","doi":"10.1109/RTAS.2016.7461337","ddc":["005"],"language":[{"iso":"eng"}],"acknowledgement":"This work is supported in part by NSF CNS 13-30077, NSF CNS 13-29886, NSF CNS 15-45002, NSFC 61303014, NSFC 61202010, and NSFC 91218302.","author":[{"full_name":"Jiang, Yu","first_name":"Yu","last_name":"Jiang"},{"first_name":"Yixiao","full_name":"Yang, Yixiao","last_name":"Yang"},{"first_name":"Han","full_name":"Liu, Han","last_name":"Liu"},{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","last_name":"Kong","full_name":"Kong, Hui","first_name":"Hui"},{"last_name":"Gu","first_name":"Ming","full_name":"Gu, Ming"},{"last_name":"Sun","full_name":"Sun, Jiaguang","first_name":"Jiaguang"},{"last_name":"Sha","full_name":"Sha, Lui","first_name":"Lui"}],"type":"conference","day":"27","title":"From stateflow simulation to verified implementation: A verification approach and a real-time train controller design","conference":{"start_date":"2016-04-11","end_date":"2016-04-14","name":"RTAS: Real-time and Embedded Technology and Applications Symposium","location":"Vienna, Austria"},"citation":{"ama":"Jiang Y, Yang Y, Liu H, et al. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. In: IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">10.1109/RTAS.2016.7461337</a>","apa":"Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., &#38; Sha, L. (2016). From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria: IEEE. <a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">https://doi.org/10.1109/RTAS.2016.7461337</a>","short":"Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016.","mla":"Jiang, Yu, et al. <i>From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design</i>. 7461337, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">10.1109/RTAS.2016.7461337</a>.","chicago":"Jiang, Yu, Yixiao Yang, Han Liu, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design.” IEEE, 2016. <a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">https://doi.org/10.1109/RTAS.2016.7461337</a>.","ieee":"Y. Jiang <i>et al.</i>, “From stateflow simulation to verified implementation: A verification approach and a real-time train controller design,” presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria, 2016.","ista":"Jiang Y, Yang Y, Liu H, Kong H, Gu M, Sun J, Sha L. 2016. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. RTAS: Real-time and Embedded Technology and Applications Symposium, 7461337."}},{"date_updated":"2022-02-25T11:59:23Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","publication_identifier":{"issn":["2296-665X"]},"article_type":"original","oa_version":"Published Version","has_accepted_license":"1","year":"2015","file_date_updated":"2022-02-25T11:55:26Z","volume":3,"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)"},"publication_status":"published","oa":1,"article_number":"42","file":[{"file_name":"2015_FrontiersEnvironmScience_Parise.pdf","creator":"dernst","file_size":1371201,"date_updated":"2022-02-25T11:55:26Z","access_level":"open_access","checksum":"26c222487564e1be02a11d688d6f769d","content_type":"application/pdf","relation":"main_file","file_id":"10795","success":1,"date_created":"2022-02-25T11:55:26Z"}],"_id":"10794","date_published":"2015-06-10T00:00:00Z","abstract":[{"lang":"eng","text":"Mathematical models are of fundamental importance in the understanding of complex population dynamics. For instance, they can be used to predict the population evolution starting from different initial conditions or to test how a system responds to external perturbations. For this analysis to be meaningful in real applications, however, it is of paramount importance to choose an appropriate model structure and to infer the model parameters from measured data. While many parameter inference methods are available for models based on deterministic ordinary differential equations, the same does not hold for more detailed individual-based models. Here we consider, in particular, stochastic models in which the time evolution of the species abundances is described by a continuous-time Markov chain. These models are governed by a master equation that is typically difficult to solve. Consequently, traditional inference methods that rely on iterative evaluation of parameter likelihoods are computationally intractable. The aim of this paper is to present recent advances in parameter inference for continuous-time Markov chain models, based on a moment closure approximation of the parameter likelihood, and to investigate how these results can help in understanding, and ultimately controlling, complex systems in ecology. Specifically, we illustrate through an agricultural pest case study how parameters of a stochastic individual-based model can be identified from measured data and how the resulting model can be used to solve an optimal control problem in a stochastic setting. In particular, we show how the matter of determining the optimal combination of two different pest control methods can be formulated as a chance constrained optimization problem where the control action is modeled as a state reset, leading to a hybrid system formulation."}],"article_processing_charge":"No","language":[{"iso":"eng"}],"keyword":["General Environmental Science"],"doi":"10.3389/fenvs.2015.00042","ddc":["000","570"],"acknowledgement":"The authors would like to acknowledge contributions from Baptiste Mottet who performed preliminary analysis regarding parameter inference for the considered case study in a student project (Mottet, 2014/2015).\r\nThe research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement No. [291734] and from SystemsX under the project SignalX.","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"day":"10","author":[{"full_name":"Parise, Francesca","first_name":"Francesca","last_name":"Parise"},{"last_name":"Lygeros","full_name":"Lygeros, John","first_name":"John"},{"first_name":"Jakob","full_name":"Ruess, Jakob","last_name":"Ruess","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282"}],"type":"journal_article","ec_funded":1,"citation":{"short":"F. Parise, J. Lygeros, J. Ruess, Frontiers in Environmental Science 3 (2015).","apa":"Parise, F., Lygeros, J., &#38; Ruess, J. (2015). Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. Frontiers. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>","ama":"Parise F, Lygeros J, Ruess J. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. 2015;3. doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>","ista":"Parise F, Lygeros J, Ruess J. 2015. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. Frontiers in Environmental Science. 3, 42.","ieee":"F. Parise, J. Lygeros, and J. Ruess, “Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study,” <i>Frontiers in Environmental Science</i>, vol. 3. Frontiers, 2015.","chicago":"Parise, Francesca, John Lygeros, and Jakob Ruess. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>. Frontiers, 2015. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>.","mla":"Parise, Francesca, et al. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>, vol. 3, 42, Frontiers, 2015, doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>."},"title":"Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"publication":"Frontiers in Environmental Science","intvolume":"         3","status":"public","publisher":"Frontiers","month":"06","date_created":"2022-02-25T11:42:25Z"},{"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","day":"31","title":"Nested weighted automata","conference":{"location":"Kyoto, Japan","name":"LICS: Logic in Computer Science","end_date":"2015-07-10","start_date":"2015-07-06"},"citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). Nested weighted automata. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174926.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174926, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>."},"ec_funded":1,"doi":"10.1109/LICS.2015.72","language":[{"iso":"eng"}],"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"related_material":{"record":[{"status":"public","id":"467","relation":"later_version"},{"relation":"earlier_version","id":"5415","status":"public"},{"relation":"earlier_version","id":"5436","status":"public"}]},"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.\r\nA Technical Report of the paper is available at: \r\nhttps://repository.ist.ac.at/331/\r\n","date_created":"2018-12-11T11:53:17Z","month":"07","status":"public","publication":"Proceedings - Symposium on Logic in Computer Science","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IEEE","oa_version":"None","year":"2015","publist_id":"5494","scopus_import":1,"external_id":{"arxiv":["1606.03598"]},"date_updated":"2023-02-23T12:26:19Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1656","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, nor in any other know 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 run-time 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":"2015-07-31T00:00:00Z","article_number":"7174926","arxiv":1,"volume":"2015-July","publication_status":"published"},{"_id":"1657","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"date_published":"2015-07-01T00:00:00Z","publication_status":"published","year":"2015","oa_version":"None","publist_id":"5493","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:26:16Z","page":"244 - 256","series_title":"LICS","date_created":"2018-12-11T11:53:18Z","month":"07","publisher":"IEEE","status":"public","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","conference":{"start_date":"2015-07-06","end_date":"2015-07-10","name":"LICS: Logic in Computer Science","location":"Kyoto, Japan"},"citation":{"chicago":"Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>.","ieee":"K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.","ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.","mla":"Chatterjee, Krishnendu, et al. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IEEE, 2015, pp. 244–56, doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>.","short":"K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.","ama":"Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>","apa":"Chatterjee, K., Komárková, Z., &#38; Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>"},"ec_funded":1,"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Zuzana","full_name":"Komárková, Zuzana","last_name":"Komárková"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"}],"type":"conference","alternative_title":["LICS"],"day":"01","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"466"},{"id":"5429","relation":"earlier_version","status":"public"},{"id":"5435","relation":"earlier_version","status":"public"}]},"acknowledgement":"A Technical Report of this paper is available at:  https://repository.ist.ac.at/327\r\n","doi":"10.1109/LICS.2015.32","language":[{"iso":"eng"}]},{"doi":"10.1007/978-3-319-23401-4_8","language":[{"iso":"eng"}],"related_material":{"record":[{"id":"1148","relation":"later_version","status":"public"}]},"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Podelski","full_name":"Podelski, Andreas","first_name":"Andreas"},{"last_name":"Ruess","first_name":"Jakob","full_name":"Ruess, Jakob","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282"},{"first_name":"Christian","full_name":"Schilling, Christian","last_name":"Schilling"}],"day":"01","conference":{"start_date":"2015-09-16","end_date":"2015-09-18","name":"CMSB: Computational Methods in Systems Biology","location":"Nantes, France"},"title":"Adaptive moment closure for parameter inference of biochemical reaction networks","ec_funded":1,"citation":{"chicago":"Bogomolov, Sergiy, Thomas A Henzinger, Andreas Podelski, Jakob Ruess, and Christian Schilling. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">https://doi.org/10.1007/978-3-319-23401-4_8</a>.","ieee":"S. Bogomolov, T. A. Henzinger, A. Podelski, J. Ruess, and C. Schilling, “Adaptive moment closure for parameter inference of biochemical reaction networks,” vol. 9308. Springer, pp. 77–89, 2015.","ista":"Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. 2015. Adaptive moment closure for parameter inference of biochemical reaction networks. 9308, 77–89.","mla":"Bogomolov, Sergiy, et al. <i>Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks</i>. Vol. 9308, Springer, 2015, pp. 77–89, doi:<a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">10.1007/978-3-319-23401-4_8</a>.","short":"S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, C. Schilling, 9308 (2015) 77–89.","ama":"Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. Adaptive moment closure for parameter inference of biochemical reaction networks. 2015;9308:77-89. doi:<a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">10.1007/978-3-319-23401-4_8</a>","apa":"Bogomolov, S., Henzinger, T. A., Podelski, A., Ruess, J., &#38; Schilling, C. (2015). Adaptive moment closure for parameter inference of biochemical reaction networks. Presented at the CMSB: Computational Methods in Systems Biology, Nantes, France: Springer. <a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">https://doi.org/10.1007/978-3-319-23401-4_8</a>"},"status":"public","intvolume":"      9308","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"quality_controlled":"1","publisher":"Springer","date_created":"2018-12-11T11:53:18Z","series_title":"Lecture Notes in Computer Science","month":"09","page":"77 - 89","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-21T16:17:24Z","scopus_import":1,"oa_version":"None","year":"2015","publist_id":"5492","volume":9308,"publication_status":"published","abstract":[{"text":"Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space.","lang":"eng"}],"_id":"1658","date_published":"2015-09-01T00:00:00Z"},{"_id":"1659","date_published":"2015-07-01T00:00:00Z","abstract":[{"lang":"eng","text":"The target discounted-sum problem is the following: Given a rational discount factor 0 &lt; λ &lt; 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata."}],"file":[{"file_name":"2015_LICS_Boker.pdf","creator":"dernst","file_size":340215,"checksum":"6abebca9c1a620e9e103a8f9222befac","date_updated":"2020-07-14T12:45:10Z","access_level":"open_access","content_type":"application/pdf","file_id":"7852","relation":"main_file","date_created":"2020-05-15T08:53:29Z"}],"article_processing_charge":"No","file_date_updated":"2020-07-14T12:45:10Z","oa":1,"publication_status":"published","has_accepted_license":"1","oa_version":"Submitted Version","year":"2015","publist_id":"5491","publication_identifier":{"eisbn":["978-1-4799-8875-4 "],"issn":["1043-6871 "]},"date_updated":"2023-02-23T12:26:27Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"date_created":"2018-12-11T11:53:19Z","series_title":"Logic in Computer Science","month":"07","page":"750 - 761","status":"public","department":[{"_id":"ToHe"}],"quality_controlled":"1","publication":"LICS","publisher":"IEEE","type":"conference","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi","first_name":"Udi","last_name":"Boker"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"day":"01","conference":{"end_date":"2015-07-10","start_date":"2015-007-06","name":"LICS: Logic in Computer Science","location":"Kyoto, Japan"},"title":"The target discounted-sum problem","ec_funded":1,"citation":{"short":"U. Boker, T.A. Henzinger, J. Otop, in:, LICS, IEEE, 2015, pp. 750–761.","ama":"Boker U, Henzinger TA, Otop J. The target discounted-sum problem. In: <i>LICS</i>. Logic in Computer Science. IEEE; 2015:750-761. doi:<a href=\"https://doi.org/10.1109/LICS.2015.74\">10.1109/LICS.2015.74</a>","apa":"Boker, U., Henzinger, T. A., &#38; Otop, J. (2015). The target discounted-sum problem. In <i>LICS</i> (pp. 750–761). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.74\">https://doi.org/10.1109/LICS.2015.74</a>","chicago":"Boker, Udi, Thomas A Henzinger, and Jan Otop. “The Target Discounted-Sum Problem.” In <i>LICS</i>, 750–61. Logic in Computer Science. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.74\">https://doi.org/10.1109/LICS.2015.74</a>.","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem. LICS. LICS: Logic in Computer ScienceLogic in Computer Science, 750–761.","ieee":"U. Boker, T. A. Henzinger, and J. Otop, “The target discounted-sum problem,” in <i>LICS</i>, Kyoto, Japan, 2015, pp. 750–761.","mla":"Boker, Udi, et al. “The Target Discounted-Sum Problem.” <i>LICS</i>, IEEE, 2015, pp. 750–61, doi:<a href=\"https://doi.org/10.1109/LICS.2015.74\">10.1109/LICS.2015.74</a>."},"ddc":["000"],"doi":"10.1109/LICS.2015.74","language":[{"iso":"eng"}],"acknowledgement":"A technical report of the article is available at: https://research-explorer.app.ist.ac.at/record/5439","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_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"}],"related_material":{"record":[{"relation":"earlier_version","id":"5439","status":"public"}]}}]