[{"ec_funded":1,"department":[{"_id":"ToHe"}],"external_id":{"arxiv":["1603.06850"],"isi":["000387731400013"]},"article_processing_charge":"No","date_updated":"2026-04-15T10:02:12Z","title":"Array folds logic","main_file_link":[{"url":"http://arxiv.org/abs/1603.06850","open_access":"1"}],"author":[{"first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","first_name":"Andrey","last_name":"Kupriyanov","full_name":"Kupriyanov, Andrey"}],"publist_id":"5818","date_published":"2016-07-13T00:00:00Z","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"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"}],"publisher":"Springer","year":"2016","page":"230 - 248","month":"07","isi":1,"language":[{"iso":"eng"}],"oa":1,"date_created":"2018-12-11T11:51:45Z","arxiv":1,"related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"corr_author":"1","oa_version":"Preprint","status":"public","conference":{"start_date":"2016-07-17","name":"CAV: Computer Aided Verification","location":"Toronto, Canada","end_date":"2016-07-23"},"type":"conference","alternative_title":["LNCS"],"day":"13","intvolume":"      9780","publication_status":"published","_id":"1391","scopus_import":"1","doi":"10.1007/978-3-319-41540-6_13","volume":9780,"citation":{"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>","short":"P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248.","ista":"Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer Aided Verification, LNCS, vol. 9780, 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>","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>.","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>.","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."},"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"department":[{"_id":"ToHe"}],"day":"11","publication_status":"published","external_id":{"isi":["000390844400018"]},"article_processing_charge":"No","_id":"1421","date_updated":"2025-09-18T14:21:28Z","scopus_import":"1","title":"Scalable static hybridization methods for analysis of nonlinear systems","author":[{"first_name":"Stanley","last_name":"Bak","full_name":"Bak, Stanley"},{"last_name":"Bogomolov","orcid":"0000-0002-0686-0365","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","full_name":"Bogomolov, Sergiy"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Johnson, Taylor","first_name":"Taylor","last_name":"Johnson"},{"last_name":"Prakash","first_name":"Pradyot","full_name":"Prakash, Pradyot"}],"date_published":"2016-04-11T00:00:00Z","publist_id":"5786","date_created":"2018-12-11T11:51:55Z","ec_funded":1,"oa_version":"None","status":"public","conference":{"end_date":"2016-04-14","start_date":"2016-04-12","name":"HSCC: Hybrid Systems - Computation and Control","location":"Vienna, Austria"},"type":"conference","page":"155 - 164","month":"04","year":"2016","language":[{"iso":"eng"}],"isi":1,"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1145/2883817.2883837","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"abstract":[{"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.","lang":"eng"}],"citation":{"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>","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: 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>","short":"S. Bak, S. Bogomolov, T.A. Henzinger, T. Johnson, P. Prakash, in:, Springer, 2016, pp. 155–164.","ista":"Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. 2016. Scalable static hybridization methods for analysis of nonlinear systems. HSCC: Hybrid Systems - Computation and Control, 155–164.","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>.","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>.","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: Hybrid Systems - Computation and Control, Vienna, Austria, 2016, pp. 155–164."},"publisher":"Springer"},{"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1145/2837614.2837650","volume":"20-22","citation":{"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>.","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>","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, 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.","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."},"publication_status":"published","day":"11","_id":"1439","scopus_import":"1","acknowledgement":"Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192 and FA8650-15-C-7564) and NSF (Grant CCF-1138967). ","date_created":"2018-12-11T11:52:01Z","status":"public","oa_version":"Preprint","alternative_title":["ACM SIGPLAN Notices"],"type":"conference","conference":{"location":"St. Petersburg, FL, USA","start_date":"2016-01-20","name":"POPL: Principles of Programming Languages","end_date":"2016-01-22"},"month":"01","year":"2016","page":"400 - 415","isi":1,"language":[{"iso":"eng"}],"oa":1,"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"abstract":[{"lang":"eng","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."}],"publisher":"ACM","department":[{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000374053600033"]},"date_updated":"2025-09-18T11:44:23Z","title":"PSYNC: A partially synchronous language for fault-tolerant distributed algorithms","publist_id":"5759","date_published":"2016-01-11T00:00:00Z","main_file_link":[{"url":"https://hal.inria.fr/hal-01251199/","open_access":"1"}],"author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara","last_name":"Dragoi","full_name":"Dragoi, Cezara"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien","last_name":"Zufferey","orcid":"0000-0002-3197-8736"}],"ec_funded":1},{"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.","scopus_import":"1","_id":"1524","day":"10","intvolume":"      9271","publication_status":"published","conference":{"end_date":"2015-09-05","name":"HSB: Hybrid Systems Biology","start_date":"2015-09-04","location":"Madrid, Spain"},"alternative_title":["LNCS"],"type":"conference","status":"public","oa_version":"Preprint","corr_author":"1","date_created":"2018-12-11T11:52:31Z","arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","citation":{"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>","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.","short":"A. Beica, C.C. Guet, T. Petrov, in:, Springer, 2016, pp. 173–191.","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>","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>.","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."},"volume":9271,"doi":"10.1007/978-3-319-26916-0_10","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1501.00440"}],"author":[{"full_name":"Beica, Andreea","last_name":"Beica","first_name":"Andreea"},{"full_name":"Guet, Calin C","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","orcid":"0000-0001-6220-2052"},{"last_name":"Petrov","orcid":"0000-0002-9041-0905","first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana"}],"publist_id":"5649","date_published":"2016-01-10T00:00:00Z","date_updated":"2025-06-04T12:06:27Z","title":"Efficient reduction of kappa models by static inspection of the rule-set","external_id":{"arxiv":["1501.00440"]},"article_processing_charge":"No","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"ec_funded":1,"oa":1,"language":[{"iso":"eng"}],"page":"173 - 191","year":"2016","month":"01","publisher":"Springer","abstract":[{"lang":"eng","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."}],"project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}]},{"ec_funded":1,"external_id":{"arxiv":["1506.01233"],"isi":["000375148800012"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","last_name":"Samanta","full_name":"Samanta, Roopsha"}],"main_file_link":[{"url":"http://arxiv.org/abs/1506.01233","open_access":"1"}],"date_published":"2016-01-01T00:00:00Z","publist_id":"5647","title":"Lipschitz robustness of timed I/O systems","date_updated":"2025-09-18T11:06:25Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publisher":"Springer","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."}],"isi":1,"language":[{"iso":"eng"}],"year":"2016","month":"01","page":"250 - 267","oa":1,"corr_author":"1","date_created":"2018-12-11T11:52:32Z","arxiv":1,"conference":{"start_date":"2016-01-17","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","location":"St. Petersburg, FL, USA","end_date":"2016-01-19"},"type":"conference","alternative_title":["LNCS"],"oa_version":"Preprint","status":"public","_id":"1526","day":"01","intvolume":"      9583","publication_status":"published","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.","scopus_import":"1","doi":"10.1007/978-3-662-49122-5_12","citation":{"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>.","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.","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>","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>","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.","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>."},"volume":9583,"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"doi":"10.1007/s10009-015-0393-y","citation":{"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.","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>","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.","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>","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.","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>."},"volume":18,"file_date_updated":"2020-07-14T12:45:13Z","quality_controlled":"1","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"5146","date_updated":"2020-07-14T12:45:13Z","file_size":2296522,"checksum":"31561d7705599a9bd4ea816accc0752e","date_created":"2018-12-12T10:15:26Z","file_name":"IST-2016-457-v1+1_s10009-015-0393-y.pdf","creator":"system","access_level":"open_access"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2018-12-11T11:53:34Z","corr_author":"1","status":"public","publication":"International Journal on Software Tools for Technology Transfer","oa_version":"Published Version","type":"journal_article","publication_status":"published","intvolume":"        18","day":"01","_id":"1705","scopus_import":"1","has_accepted_license":"1","ddc":["000"],"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"abstract":[{"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.","lang":"eng"}],"pubrep_id":"457","publisher":"Springer","year":"2016","month":"08","page":"449 - 467","language":[{"iso":"eng"}],"isi":1,"oa":1,"ec_funded":1,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"department":[{"_id":"ToHe"}],"article_processing_charge":"Yes (via OA deal)","external_id":{"isi":["000379708300007"]},"issue":"4","date_updated":"2025-09-18T10:50:19Z","title":"Guided search for hybrid systems based on coarse-grained space abstractions","date_published":"2016-08-01T00:00:00Z","publist_id":"5431","author":[{"first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy"},{"last_name":"Donzé","first_name":"Alexandre","full_name":"Donzé, Alexandre"},{"last_name":"Frehse","first_name":"Goran","full_name":"Frehse, Goran"},{"full_name":"Grosu, Radu","last_name":"Grosu","first_name":"Radu"},{"first_name":"Taylor","last_name":"Johnson","full_name":"Johnson, Taylor"},{"last_name":"Ladan","first_name":"Hamed","full_name":"Ladan, Hamed"},{"first_name":"Andreas","last_name":"Podelski","full_name":"Podelski, Andreas"},{"last_name":"Wehrle","first_name":"Martin","full_name":"Wehrle, Martin"}]},{"type":"conference","alternative_title":["Proceedings International Conference on Software Engineering"],"conference":{"end_date":"2016-05-22","name":"ICSE: International Conference on Software Engineering","start_date":"2016-05-14","location":"Austin, TX, USA"},"oa_version":"None","status":"public","publication":"Proceedings of the 38th International Conference on Software Engineering Companion ","date_created":"2018-12-11T11:46:42Z","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","scopus_import":"1","_id":"479","publication_status":"published","day":"14","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.","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>.","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>","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.","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.","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","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","publist_id":"7341","date_published":"2016-05-14T00:00:00Z","author":[{"full_name":"Jiang, Yu","last_name":"Jiang","first_name":"Yu"},{"full_name":"Liu, Han","first_name":"Han","last_name":"Liu"},{"full_name":"Kong, Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui","last_name":"Kong","orcid":"0000-0002-3066-6941"},{"last_name":"Wang","first_name":"Rui","full_name":"Wang, Rui"},{"last_name":"Hosseini","first_name":"Mohamad","full_name":"Hosseini, Mohamad"},{"full_name":"Sun, Jiaguang","last_name":"Sun","first_name":"Jiaguang"},{"last_name":"Sha","first_name":"Lui","full_name":"Sha, Lui"}],"date_updated":"2025-09-22T14:22:48Z","title":"Use runtime verification to improve the quality of medical care practice","article_processing_charge":"No","external_id":{"isi":["000402155300016"]},"department":[{"_id":"ToHe"}],"publisher":"IEEE","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"}],"language":[{"iso":"eng"}],"isi":1,"year":"2016","page":"112 - 121","month":"05"},{"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"pubrep_id":"499","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","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. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea.","lang":"eng"}],"language":[{"iso":"eng"}],"page":"90 - 102","month":"01","year":"2015","oa":1,"ec_funded":1,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"department":[{"_id":"ToHe"}],"author":[{"full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara","last_name":"Dragoi"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien","last_name":"Zufferey","orcid":"0000-0002-3197-8736"}],"date_published":"2015-01-01T00:00:00Z","publist_id":"5681","series_title":"Leibniz International Proceedings in Informatics","title":"The need for language support for fault-tolerant distributed systems","date_updated":"2025-04-15T06:26:02Z","doi":"10.4230/LIPIcs.SNAPL.2015.90","volume":32,"citation":{"ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 90–102, 2015.","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for Language Support for Fault-Tolerant Distributed Systems.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>.","apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2015). The need for language support for fault-tolerant distributed systems. Presented at the SNAPL: Summit oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for fault-tolerant distributed systems. 32, 90–102.","ama":"Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>","mla":"Dragoi, Cezara, et al. <i>The Need for Language Support for Fault-Tolerant Distributed Systems</i>. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 90–102, doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>."},"quality_controlled":"1","file_date_updated":"2020-07-14T12:44:58Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2018-12-12T10:14:02Z","creator":"system","file_name":"IST-2016-499-v1+1_9.pdf","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_id":"5050","file_size":489362,"date_updated":"2020-07-14T12:44:58Z","checksum":"cf5e94baa89a2dc4c5de01abc676eda8"}],"corr_author":"1","date_created":"2018-12-11T11:52:22Z","conference":{"end_date":"2015-05-06","start_date":"2015-05-03","name":"SNAPL: Summit oN Advances in Programming Languages","location":"Asilomar, CA, United States"},"type":"conference","alternative_title":["LIPIcs"],"status":"public","oa_version":"Published Version","publication_identifier":{"isbn":["978-3-939897-80-4 "]},"_id":"1498","day":"01","intvolume":"        32","publication_status":"published","ddc":["005"],"has_accepted_license":"1","scopus_import":1},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_updated":"2025-04-15T06:26:02Z","title":"Polynomial time decidability of weighted synchronization under partial observability","author":[{"orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"},{"full_name":"Larsen, Kim","last_name":"Larsen","first_name":"Kim"},{"full_name":"Laursen, Simon","last_name":"Laursen","first_name":"Simon"},{"full_name":"Srba, Jiří","last_name":"Srba","first_name":"Jiří"}],"publist_id":"5680","date_published":"2015-01-01T00:00:00Z","ec_funded":1,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"month":"01","page":"142 - 154","year":"2015","language":[{"iso":"eng"}],"oa":1,"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"We consider weighted automata with both positive and negative integer weights on edges and\r\nstudy the problem of synchronization using adaptive strategies that may only observe whether\r\nthe current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata."}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","pubrep_id":"498","intvolume":"        42","day":"01","publication_status":"published","_id":"1499","scopus_import":1,"ddc":["000","003"],"acknowledgement":"The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement 601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Czech Science Foundation under grant agreement P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734.","has_accepted_license":"1","date_created":"2018-12-11T11:52:22Z","status":"public","oa_version":"Published Version","conference":{"location":"Madrid, Spain","name":"CONCUR: Concurrency Theory","start_date":"2015-09-01","end_date":"2015-09-04"},"alternative_title":["LIPIcs"],"type":"conference","file_date_updated":"2020-07-14T12:44:58Z","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_updated":"2020-07-14T12:44:58Z","file_size":623563,"checksum":"49eb5021caafaabe5356c65b9c5f8c9c","relation":"main_file","content_type":"application/pdf","file_id":"4672","access_level":"open_access","date_created":"2018-12-12T10:08:12Z","file_name":"IST-2016-498-v1+1_32.pdf","creator":"system"}],"doi":"10.4230/LIPIcs.CONCUR.2015.142","citation":{"chicago":"Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time Decidability of Weighted Synchronization under Partial Observability,” 42:142–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>.","ieee":"J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability of weighted synchronization under partial observability,” presented at the CONCUR: Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.","mla":"Kretinsky, Jan, et al. <i>Polynomial Time Decidability of Weighted Synchronization under Partial Observability</i>. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>.","ama":"Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>","apa":"Kretinsky, J., Larsen, K., Laursen, S., &#38; Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","ista":"Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability of weighted synchronization under partial observability. CONCUR: Concurrency Theory, LIPIcs, vol. 42, 142–154."},"volume":42},{"volume":47,"citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>.","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” <i>Formal Methods in System Design</i>, vol. 47, no. 2. Springer, pp. 230–264, 2015.","mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. 2015;47(2):230-264. doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>","apa":"Chatterjee, K., Chmelik, M., &#38; Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264."},"doi":"10.1007/s10703-015-0235-2","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","publication":"Formal Methods in System Design","oa_version":"Preprint","status":"public","type":"journal_article","date_created":"2018-12-11T11:52:23Z","arxiv":1,"related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"corr_author":"1","scopus_import":"1","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","publication_status":"published","intvolume":"        47","day":"01","_id":"1501","abstract":[{"text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. ","lang":"eng"}],"publisher":"Springer","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","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"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"oa":1,"page":"230 - 264","month":"10","year":"2015","isi":1,"language":[{"iso":"eng"}],"ec_funded":1,"title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","date_updated":"2026-04-15T10:02:12Z","issue":"2","date_published":"2015-10-01T00:00:00Z","publist_id":"5677","main_file_link":[{"url":"https://arxiv.org/abs/1405.0835","open_access":"1"}],"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin"},{"last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"arxiv":["1405.0835"],"isi":["000361752300003"]}},{"doi":"10.1145/2737166.2737175","citation":{"ieee":"N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.","chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>.","mla":"Beneš, Nikola, et al. <i>Complete Composition Operators for IOCO-Testing Theory</i>. ACM, 2015, pp. 101–10, doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>.","apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>","ista":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition operators for IOCO-testing theory. CBSE: Component-Based Software Engineering , Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering , , 101–110.","short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>"},"quality_controlled":"1","file_date_updated":"2020-07-14T12:44:59Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"file_id":"5303","content_type":"application/pdf","relation":"main_file","checksum":"c6ce681035c163a158751f240cb7d389","file_size":467561,"date_updated":"2020-07-14T12:44:59Z","creator":"system","file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf","date_created":"2018-12-12T10:17:46Z","access_level":"open_access"}],"related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"date_created":"2018-12-11T11:52:24Z","conference":{"end_date":"2015-05-08","location":"Montreal, QC, Canada","name":"CBSE: Component-Based Software Engineering ","start_date":"2015-05-04"},"alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"type":"conference","status":"public","oa_version":"Submitted Version","publication_identifier":{"isbn":["978-1-4503-3471-6"]},"_id":"1502","day":"01","publication_status":"published","ddc":["000"],"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) and Z211-N23 (Wittgestein Award), by People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373 (nSafeCer).  Jan Křetínský has been partially supported by the Czech Science Foundation, grant No.  P202/12/G061.  Nikola Beneš has been supported by the\r\nMEYS project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.","has_accepted_license":"1","scopus_import":"1","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"publisher":"ACM","pubrep_id":"625","abstract":[{"lang":"eng","text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system."}],"isi":1,"language":[{"iso":"eng"}],"page":"101 - 110","month":"05","year":"2015","oa":1,"ec_funded":1,"external_id":{"isi":["000380554800013"]},"article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"author":[{"full_name":"Beneš, Nikola","first_name":"Nikola","last_name":"Beneš"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","last_name":"Daca","full_name":"Daca, Przemyslaw"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan"},{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic"}],"publist_id":"5676","date_published":"2015-05-01T00:00:00Z","date_updated":"2026-04-15T10:02:12Z","title":"Complete composition operators for IOCO-testing theory"},{"ec_funded":1,"date_published":"2015-06-30T00:00:00Z","publist_id":"5633","author":[{"last_name":"Ruess","orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","first_name":"Jakob","full_name":"Ruess, Jakob"},{"full_name":"Parise, Francesca","last_name":"Parise","first_name":"Francesca"},{"last_name":"Milias Argeitis","first_name":"Andreas","full_name":"Milias Argeitis, Andreas"},{"full_name":"Khammash, Mustafa","first_name":"Mustafa","last_name":"Khammash"},{"full_name":"Lygeros, John","last_name":"Lygeros","first_name":"John"}],"main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4491780/"}],"date_updated":"2025-09-23T09:24:24Z","title":"Iterative experiment design guides the characterization of a light-inducible gene expression circuit","issue":"26","article_processing_charge":"No","external_id":{"isi":["000357079400070"],"pmid":["26085136"]},"department":[{"_id":"ToHe"},{"_id":"GaTk"}],"publisher":"National Academy of Sciences","abstract":[{"lang":"eng","text":"Systems biology rests on the idea that biological complexity can be better unraveled through the interplay of modeling and experimentation. However, the success of this approach depends critically on the informativeness of the chosen experiments, which is usually unknown a priori. Here, we propose a systematic scheme based on iterations of optimal experiment design, flow cytometry experiments, and Bayesian parameter inference to guide the discovery process in the case of stochastic biochemical reaction networks. To illustrate the benefit of our methodology, we apply it to the characterization of an engineered light-inducible gene expression circuit in yeast and compare the performance of the resulting model with models identified from nonoptimal experiments. In particular, we compare the parameter posterior distributions and the precision to which the outcome of future experiments can be predicted. Moreover, we illustrate how the identified stochastic model can be used to determine light induction patterns that make either the average amount of protein or the variability in a population of cells follow a desired profile. Our results show that optimal experiment design allows one to derive models that are accurate enough to precisely predict and regulate the protein expression in heterogeneous cell populations over extended periods of time."}],"project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa":1,"language":[{"iso":"eng"}],"isi":1,"year":"2015","page":"8148 - 8153","month":"06","type":"journal_article","publication":"PNAS","status":"public","oa_version":"Submitted Version","pmid":1,"date_created":"2018-12-11T11:52:36Z","acknowledgement":"J.R., F.P., and J.L. acknowledge support from the European Commission under the Network of Excellence HYCON2 (highly-complex and networked control systems) and SystemsX.ch under the SignalX Project. J.R. acknowledges support from the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme FP7/2007-2013 under REA (Research Executive Agency) Grant 291734. M.K. acknowledges support from Human Frontier Science Program Grant RP0061/2011 (www.hfsp.org). ","scopus_import":"1","_id":"1538","publication_status":"published","intvolume":"       112","day":"30","citation":{"chicago":"Ruess, Jakob, Francesca Parise, Andreas Milias Argeitis, Mustafa Khammash, and John Lygeros. “Iterative Experiment Design Guides the Characterization of a Light-Inducible Gene Expression Circuit.” <i>PNAS</i>. National Academy of Sciences, 2015. <a href=\"https://doi.org/10.1073/pnas.1423947112\">https://doi.org/10.1073/pnas.1423947112</a>.","ieee":"J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, and J. Lygeros, “Iterative experiment design guides the characterization of a light-inducible gene expression circuit,” <i>PNAS</i>, vol. 112, no. 26. National Academy of Sciences, pp. 8148–8153, 2015.","mla":"Ruess, Jakob, et al. “Iterative Experiment Design Guides the Characterization of a Light-Inducible Gene Expression Circuit.” <i>PNAS</i>, vol. 112, no. 26, National Academy of Sciences, 2015, pp. 8148–53, doi:<a href=\"https://doi.org/10.1073/pnas.1423947112\">10.1073/pnas.1423947112</a>.","ama":"Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. Iterative experiment design guides the characterization of a light-inducible gene expression circuit. <i>PNAS</i>. 2015;112(26):8148-8153. doi:<a href=\"https://doi.org/10.1073/pnas.1423947112\">10.1073/pnas.1423947112</a>","ista":"Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. 2015. Iterative experiment design guides the characterization of a light-inducible gene expression circuit. PNAS. 112(26), 8148–8153.","apa":"Ruess, J., Parise, F., Milias Argeitis, A., Khammash, M., &#38; Lygeros, J. (2015). Iterative experiment design guides the characterization of a light-inducible gene expression circuit. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1423947112\">https://doi.org/10.1073/pnas.1423947112</a>","short":"J. Ruess, F. Parise, A. Milias Argeitis, M. Khammash, J. Lygeros, PNAS 112 (2015) 8148–8153."},"volume":112,"doi":"10.1073/pnas.1423947112","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1"},{"doi":"10.1063/1.4937937","article_number":"244103","citation":{"mla":"Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical Reaction Networks with Partially Finite State Space.” <i>Journal of Chemical Physics</i>, vol. 143, no. 24, 244103, American Institute of Physics, 2015, doi:<a href=\"https://doi.org/10.1063/1.4937937\">10.1063/1.4937937</a>.","ista":"Ruess J. 2015. Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. Journal of Chemical Physics. 143(24), 244103.","short":"J. Ruess, Journal of Chemical Physics 143 (2015).","apa":"Ruess, J. (2015). Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. <i>Journal of Chemical Physics</i>. American Institute of Physics. <a href=\"https://doi.org/10.1063/1.4937937\">https://doi.org/10.1063/1.4937937</a>","ama":"Ruess J. Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. <i>Journal of Chemical Physics</i>. 2015;143(24). doi:<a href=\"https://doi.org/10.1063/1.4937937\">10.1063/1.4937937</a>","ieee":"J. Ruess, “Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space,” <i>Journal of Chemical Physics</i>, vol. 143, no. 24. American Institute of Physics, 2015.","chicago":"Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical Reaction Networks with Partially Finite State Space.” <i>Journal of Chemical Physics</i>. American Institute of Physics, 2015. <a href=\"https://doi.org/10.1063/1.4937937\">https://doi.org/10.1063/1.4937937</a>."},"volume":143,"quality_controlled":"1","file_date_updated":"2020-07-14T12:45:01Z","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"4641","date_updated":"2020-07-14T12:45:01Z","file_size":605355,"checksum":"838657118ae286463a2b7737319f35ce","date_created":"2018-12-12T10:07:43Z","file_name":"IST-2016-593-v1+1_Minimal_moment_equations.pdf","creator":"system","access_level":"open_access"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","corr_author":"1","date_created":"2018-12-11T11:52:36Z","type":"journal_article","publication":"Journal of Chemical Physics","oa_version":"Published Version","status":"public","_id":"1539","publication_status":"published","day":"22","intvolume":"       143","has_accepted_license":"1","ddc":["000"],"scopus_import":"1","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_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":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"publisher":"American Institute of Physics","pubrep_id":"593","abstract":[{"text":"Many stochastic models of biochemical reaction networks contain some chemical species for which the number of molecules that are present in the system can only be finite (for instance due to conservation laws), but also other species that can be present in arbitrarily large amounts. The prime example of such networks are models of gene expression, which typically contain a small and finite number of possible states for the promoter but an infinite number of possible states for the amount of mRNA and protein. One of the main approaches to analyze such models is through the use of equations for the time evolution of moments of the chemical species. Recently, a new approach based on conditional moments of the species with infinite state space given all the different possible states of the finite species has been proposed. It was argued that this approach allows one to capture more details about the full underlying probability distribution with a smaller number of equations. Here, I show that the result that less moments provide more information can only stem from an unnecessarily complicated description of the system in the classical formulation. The foundation of this argument will be the derivation of moment equations that describe the complete probability distribution over the finite state space but only low-order moments over the infinite state space. I will show that the number of equations that is needed is always less than what was previously claimed and always less than the number of conditional moment equations up to the same order. To support these arguments, a symbolic algorithm is provided that can be used to derive minimal systems of unconditional moment equations for models with partially finite state space. ","lang":"eng"}],"language":[{"iso":"eng"}],"isi":1,"month":"12","year":"2015","oa":1,"ec_funded":1,"article_processing_charge":"No","external_id":{"isi":["000370412900068"]},"department":[{"_id":"ToHe"},{"_id":"GaTk"}],"publist_id":"5632","date_published":"2015-12-22T00:00:00Z","author":[{"first_name":"Jakob","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","last_name":"Ruess","orcid":"0000-0003-1615-3282","full_name":"Ruess, Jakob"}],"date_updated":"2025-09-23T09:34:48Z","issue":"24","title":"Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space"},{"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-319-26287-1_1","citation":{"mla":"Ray, Rajarshi, et al. <i>XSpeed: Accelerating Reachability Analysis on Multi-Core Processors</i>. Vol. 9434, Springer, 2015, pp. 3–18, doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">10.1007/978-3-319-26287-1_1</a>.","ama":"Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. XSpeed: Accelerating reachability analysis on multi-core processors. 2015;9434:3-18. doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">10.1007/978-3-319-26287-1_1</a>","short":"R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, R. Grosu, 9434 (2015) 3–18.","apa":"Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., &#38; Grosu, R. (2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">https://doi.org/10.1007/978-3-319-26287-1_1</a>","ista":"Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. 2015. XSpeed: Accelerating reachability analysis on multi-core processors. 9434, 3–18.","chicago":"Ray, Rajarshi, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov, and Radu Grosu. “XSpeed: Accelerating Reachability Analysis on Multi-Core Processors.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">https://doi.org/10.1007/978-3-319-26287-1_1</a>.","ieee":"R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, and R. Grosu, “XSpeed: Accelerating reachability analysis on multi-core processors,” vol. 9434. Springer, pp. 3–18, 2015."},"volume":9434,"_id":"1541","day":"28","intvolume":"      9434","publication_status":"published","acknowledgement":"This work 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, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","scopus_import":1,"date_created":"2018-12-11T11:52:37Z","conference":{"end_date":"2015-11-19","start_date":"2015-11-17","name":"HVC: Haifa Verification Conference","location":"Haifa, Israel"},"type":"conference","alternative_title":["LNCS"],"oa_version":"None","status":"public","language":[{"iso":"eng"}],"month":"11","year":"2015","page":"3 - 18","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"publisher":"Springer","abstract":[{"text":"We present XSpeed a parallel state-space exploration algorithm for continuous systems with linear dynamics and nondeterministic inputs. The motivation of having parallel algorithms is to exploit the computational power of multi-core processors to speed-up performance. The parallelization is achieved on two fronts. First, we propose a parallel implementation of the support function algorithm by sampling functions in parallel. Second, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input. A GP-GPU implementation is also presented following a lazy evaluation strategy on support functions. The parallel algorithms are implemented in the tool XSpeed. We evaluated the performance on two benchmarks including an 28 dimension Helicopter model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experiments illustrate that our parallel algorithm with time slicing not only speeds-up performance but also improves precision.","lang":"eng"}],"department":[{"_id":"ToHe"}],"author":[{"last_name":"Ray","first_name":"Rajarshi","full_name":"Ray, Rajarshi"},{"first_name":"Amit","last_name":"Gurung","full_name":"Gurung, Amit"},{"last_name":"Das","first_name":"Binayak","full_name":"Das, Binayak"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"full_name":"Grosu, Radu","last_name":"Grosu","first_name":"Radu"}],"publist_id":"5630","date_published":"2015-11-28T00:00:00Z","title":"XSpeed: Accelerating reachability analysis on multi-core processors","series_title":"Lecture Notes in Computer Science","date_updated":"2025-04-15T06:26:02Z","ec_funded":1},{"ec_funded":1,"author":[{"full_name":"Forejt, Vojtěch","last_name":"Forejt","first_name":"Vojtěch"},{"last_name":"Krčál","first_name":"Jan","full_name":"Krčál, Jan"},{"full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"date_published":"2015-11-22T00:00:00Z","publist_id":"5577","date_updated":"2025-09-23T08:21:59Z","title":"Controller synthesis for MDPs and frequency LTL\\GU","external_id":{"isi":["000375574900012"]},"article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Springer","abstract":[{"text":"Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.","lang":"eng"}],"project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"isi":1,"language":[{"iso":"eng"}],"month":"11","page":"162 - 177","year":"2015","conference":{"end_date":"2015-11-28","location":"Suva, Fiji","start_date":"2015-11-24","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning"},"alternative_title":["LNCS"],"type":"conference","status":"public","oa_version":"None","date_created":"2018-12-11T11:52:55Z","acknowledgement":"This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).\r\n","scopus_import":"1","_id":"1594","day":"22","intvolume":"      9450","publication_status":"published","volume":9450,"citation":{"mla":"Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\\GU</i>. Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>.","ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>","apa":"Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>","short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.","ista":"Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450, 162–177.","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>.","ieee":"V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177."},"doi":"10.1007/978-3-662-48899-7_12","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1"},{"publication_status":"published","intvolume":"      9206","day":"16","_id":"1601","scopus_import":"1","has_accepted_license":"1","ddc":["000"],"date_created":"2018-12-11T11:52:57Z","oa_version":"Submitted Version","status":"public","alternative_title":["LNCS"],"type":"conference","conference":{"location":"San Francisco, CA, United States","start_date":"2015-07-18","name":"CAV: Computer Aided Verification","end_date":"2015-07-24"},"file_date_updated":"2020-07-14T12:45:04Z","quality_controlled":"1","file":[{"date_updated":"2020-07-14T12:45:04Z","file_size":1651779,"checksum":"5885236fa88a439baba9ac6f3e801e93","relation":"main_file","content_type":"application/pdf","file_id":"7850","access_level":"open_access","date_created":"2020-05-15T08:38:12Z","file_name":"2015_CAV_Babiak.pdf","creator":"dernst"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","doi":"10.1007/978-3-319-21690-4_31","volume":9206,"citation":{"apa":"Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>","ista":"Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification, LNCS, vol. 9206, 479–486.","short":"T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>","mla":"Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer, 2015, pp. 479–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>.","ieee":"T. Babiak <i>et al.</i>, “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.","chicago":"Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein, Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata Format,” 9206:479–86. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>."},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","external_id":{"isi":["000364182900031"]},"date_updated":"2025-09-23T13:50:55Z","title":"The Hanoi omega-automata format","date_published":"2015-07-16T00:00:00Z","publist_id":"5566","author":[{"full_name":"Babiak, Tomáš","first_name":"Tomáš","last_name":"Babiak"},{"full_name":"Blahoudek, František","first_name":"František","last_name":"Blahoudek"},{"first_name":"Alexandre","last_name":"Duret Lutz","full_name":"Duret Lutz, Alexandre"},{"first_name":"Joachim","last_name":"Klein","full_name":"Klein, Joachim"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881"},{"last_name":"Mueller","first_name":"Daniel","full_name":"Mueller, Daniel"},{"full_name":"Parker, David","first_name":"David","last_name":"Parker"},{"full_name":"Strejček, Jan","last_name":"Strejček","first_name":"Jan"}],"ec_funded":1,"page":"479 - 486","month":"07","year":"2015","isi":1,"language":[{"iso":"eng"}],"oa":1,"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"abstract":[{"text":"We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.","lang":"eng"}],"publisher":"Springer"},{"scopus_import":"1","acknowledgement":"This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734.","publication_status":"published","day":"16","intvolume":"      9206","_id":"1603","publication_identifier":{"eisbn":["978-3-319-21690-4"]},"status":"public","oa_version":"Preprint","type":"conference","alternative_title":["LNCS"],"conference":{"location":"San Francisco, CA, United States","start_date":"2015-07-18","name":"CAV: Computer Aided Verification","end_date":"2015-07-24"},"arxiv":1,"date_created":"2018-12-11T11:52:58Z","related_material":{"record":[{"id":"5549","status":"public","relation":"research_paper"}]},"corr_author":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","citation":{"ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &#38; Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>","ista":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.","ama":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>","mla":"Brázdil, Tomáš, et al. <i>Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Vol. 9206, Springer, 2015, pp. 158–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>."},"volume":9206,"doi":"10.1007/978-3-319-21690-4_10","date_updated":"2025-09-23T08:23:16Z","title":"Counterexample explanation by learning small strategies in Markov decision processes","date_published":"2015-07-16T00:00:00Z","publist_id":"5564","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"full_name":"Fellner, Andreas","last_name":"Fellner","first_name":"Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","full_name":"Kretinsky, Jan"}],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.02834"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"arxiv":["1502.02834"],"isi":["000364182900010"]},"ec_funded":1,"oa":1,"month":"07","page":"158 - 177","year":"2015","language":[{"iso":"eng"}],"isi":1,"abstract":[{"lang":"eng","text":"For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour."}],"publisher":"Springer","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}]},{"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"abstract":[{"text":"Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.","lang":"eng"}],"publisher":"Springer","year":"2015","page":"19 - 35","month":"11","language":[{"iso":"eng"}],"oa":1,"ec_funded":1,"department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_updated":"2025-04-15T06:26:03Z","title":"Abstraction-based parameter synthesis for multiaffine systems","author":[{"last_name":"Bogomolov","orcid":"0000-0002-0686-0365","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","full_name":"Bogomolov, Sergiy"},{"last_name":"Schilling","orcid":"0000-0003-3658-1065","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian"},{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"full_name":"Batt, Grégory","first_name":"Grégory","last_name":"Batt"},{"orcid":"0000-0002-3066-6941","last_name":"Kong","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui","full_name":"Kong, Hui"},{"first_name":"Radu","last_name":"Grosu","full_name":"Grosu, Radu"}],"publist_id":"5561","date_published":"2015-11-28T00:00:00Z","doi":"10.1007/978-3-319-26287-1_2","citation":{"ieee":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu, “Abstraction-based parameter synthesis for multiaffine systems,” presented at the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35.","chicago":"Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,” 9434:19–35. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>.","short":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:, Springer, 2015, pp. 19–35.","apa":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., &#38; Grosu, R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol. 9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>","ista":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference, LNCS, vol. 9434, 19–35.","ama":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35. doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>","mla":"Bogomolov, Sergiy, et al. <i>Abstraction-Based Parameter Synthesis for Multiaffine Systems</i>. Vol. 9434, Springer, 2015, pp. 19–35, doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>."},"volume":9434,"file_date_updated":"2020-07-14T12:45:05Z","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"3aab260f3f34641d622030ba22645b3e","date_updated":"2020-07-14T12:45:05Z","file_size":1053207,"file_id":"7851","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"2015_LNCS_Bogomolov.pdf","creator":"dernst","date_created":"2020-05-15T08:43:19Z"}],"date_created":"2018-12-11T11:52:59Z","corr_author":"1","status":"public","oa_version":"Submitted Version","conference":{"location":"Haifa, Israel","start_date":"2015-11-17","name":"HVC: Haifa Verification Conference","end_date":"2015-11-19"},"type":"conference","alternative_title":["LNCS"],"intvolume":"      9434","day":"28","publication_status":"published","_id":"1605","scopus_import":1,"ddc":["000"],"acknowledgement":"This work was partly supported by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/).","has_accepted_license":"1"},{"ec_funded":1,"date_updated":"2025-09-23T10:41:02Z","title":"Runtime verification for hybrid analysis tools","author":[{"full_name":"Nguyen, Luan","last_name":"Nguyen","first_name":"Luan"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"},{"full_name":"Bogomolov, Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov"},{"full_name":"Johnson, Taylor","first_name":"Taylor","last_name":"Johnson"}],"date_published":"2015-11-15T00:00:00Z","publist_id":"5562","department":[{"_id":"ToHe"}],"external_id":{"isi":["000370624400019"]},"article_processing_charge":"No","abstract":[{"lang":"eng","text":"In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST."}],"publisher":"Springer Nature","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"page":"281 - 286","month":"11","year":"2015","isi":1,"language":[{"iso":"eng"}],"status":"public","oa_version":"None","publication":"6th International Conference","conference":{"end_date":"2015-09-25","location":"Vienna, Austria","name":"RV: Runtime Verification","start_date":"2015-09-22"},"type":"conference","alternative_title":["LNCS"],"date_created":"2018-12-11T11:52:59Z","scopus_import":"1","day":"15","intvolume":"      9333","publication_status":"published","publication_identifier":{"isbn":["978-3-319-23819-7"]},"_id":"1606","citation":{"chicago":"Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson. “Runtime Verification for Hybrid Analysis Tools.” In <i>6th International Conference</i>, 9333:281–86. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>.","ieee":"L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, “Runtime verification for hybrid analysis tools,” in <i>6th International Conference</i>, Vienna, Austria, 2015, vol. 9333, pp. 281–286.","mla":"Nguyen, Luan, et al. “Runtime Verification for Hybrid Analysis Tools.” <i>6th International Conference</i>, vol. 9333, Springer Nature, 2015, pp. 281–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>.","ama":"Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid analysis tools. In: <i>6th International Conference</i>. Vol 9333. Springer Nature; 2015:281-286. doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>","ista":"Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Runtime verification for hybrid analysis tools. 6th International Conference. RV: Runtime Verification, LNCS, vol. 9333, 281–286.","apa":"Nguyen, L., Schilling, C., Bogomolov, S., &#38; Johnson, T. (2015). Runtime verification for hybrid analysis tools. In <i>6th International Conference</i> (Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>","short":"L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, in:, 6th International Conference, Springer Nature, 2015, pp. 281–286."},"volume":9333,"doi":"10.1007/978-3-319-23820-3_19","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1"},{"doi":"10.1007/978-3-319-23401-4_8","volume":9308,"citation":{"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>.","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>","short":"S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, C. Schilling, 9308 (2015) 77–89.","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.","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>","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.","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>."},"quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2018-12-11T11:53:18Z","related_material":{"record":[{"id":"1148","status":"public","relation":"later_version"}]},"status":"public","oa_version":"None","conference":{"location":"Nantes, France","name":"CMSB: Computational Methods in Systems Biology","start_date":"2015-09-16","end_date":"2015-09-18"},"alternative_title":["LNCS"],"type":"conference","day":"01","intvolume":"      9308","publication_status":"published","_id":"1658","scopus_import":"1","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"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"}],"publisher":"Springer","year":"2015","month":"09","page":"77 - 89","language":[{"iso":"eng"}],"isi":1,"ec_funded":1,"department":[{"_id":"ToHe"},{"_id":"GaTk"}],"external_id":{"isi":["000366198300008"]},"article_processing_charge":"No","title":"Adaptive moment closure for parameter inference of biochemical reaction networks","date_updated":"2025-09-23T07:44:58Z","series_title":"Lecture Notes in Computer Science","author":[{"full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski, Andreas"},{"full_name":"Ruess, Jakob","last_name":"Ruess","orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","first_name":"Jakob"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"}],"publist_id":"5492","date_published":"2015-09-01T00:00:00Z"}]