[{"title":"The target discounted-sum problem","department":[{"_id":"ToHe"}],"file":[{"access_level":"open_access","file_id":"7852","file_name":"2015_LICS_Boker.pdf","creator":"dernst","date_updated":"2020-07-14T12:45:10Z","file_size":340215,"checksum":"6abebca9c1a620e9e103a8f9222befac","content_type":"application/pdf","date_created":"2020-05-15T08:53:29Z","relation":"main_file"}],"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"doi":"10.1109/LICS.2015.74","quality_controlled":"1","date_published":"2015-07-01T00:00:00Z","day":"01","author":[{"last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","full_name":"Boker, Udi"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"article_processing_charge":"No","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2015","acknowledgement":"A technical report of the article is available at: https://research-explorer.app.ist.ac.at/record/5439","status":"public","conference":{"name":"LICS: Logic in Computer Science","start_date":"2015-007-06","end_date":"2015-07-10","location":"Kyoto, Japan"},"scopus_import":1,"file_date_updated":"2020-07-14T12:45:10Z","type":"conference","has_accepted_license":"1","_id":"1659","publist_id":"5491","abstract":[{"lang":"eng","text":"The target discounted-sum problem is the following: Given a rational discount factor 0 &lt; λ &lt; 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata."}],"month":"07","series_title":"Logic in Computer Science","language":[{"iso":"eng"}],"publisher":"IEEE","publication":"LICS","ddc":["000"],"citation":{"ama":"Boker U, Henzinger TA, Otop J. The target discounted-sum problem. In: <i>LICS</i>. Logic in Computer Science. IEEE; 2015:750-761. doi:<a href=\"https://doi.org/10.1109/LICS.2015.74\">10.1109/LICS.2015.74</a>","ieee":"U. Boker, T. A. Henzinger, and J. Otop, “The target discounted-sum problem,” in <i>LICS</i>, Kyoto, Japan, 2015, pp. 750–761.","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem. LICS. LICS: Logic in Computer ScienceLogic in Computer Science, 750–761.","apa":"Boker, U., Henzinger, T. A., &#38; Otop, J. (2015). The target discounted-sum problem. In <i>LICS</i> (pp. 750–761). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.74\">https://doi.org/10.1109/LICS.2015.74</a>","chicago":"Boker, Udi, Thomas A Henzinger, and Jan Otop. “The Target Discounted-Sum Problem.” In <i>LICS</i>, 750–61. Logic in Computer Science. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.74\">https://doi.org/10.1109/LICS.2015.74</a>.","short":"U. Boker, T.A. Henzinger, J. Otop, in:, LICS, IEEE, 2015, pp. 750–761.","mla":"Boker, Udi, et al. “The Target Discounted-Sum Problem.” <i>LICS</i>, IEEE, 2015, pp. 750–61, doi:<a href=\"https://doi.org/10.1109/LICS.2015.74\">10.1109/LICS.2015.74</a>."},"date_created":"2018-12-11T11:53:19Z","ec_funded":1,"page":"750 - 761","publication_identifier":{"issn":["1043-6871 "],"eisbn":["978-1-4799-8875-4 "]},"related_material":{"record":[{"id":"5439","relation":"earlier_version","status":"public"}]},"date_updated":"2025-04-15T06:26:00Z","oa":1,"oa_version":"Submitted Version"},{"publication_status":"published","year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Bogomolov, Sergiy","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov"},{"last_name":"Magazzeni","first_name":"Daniele","full_name":"Magazzeni, Daniele"},{"full_name":"Minopoli, Stefano","first_name":"Stefano","last_name":"Minopoli"},{"last_name":"Wehrle","first_name":"Martin","full_name":"Wehrle, Martin"}],"day":"01","date_published":"2015-06-01T00:00:00Z","corr_author":"1","article_processing_charge":"No","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"department":[{"_id":"ToHe"}],"title":"PDDL+ planning with hybrid automata: Foundations of translating must behavior","oa":1,"date_updated":"2025-05-19T11:37:28Z","oa_version":"None","page":"42 - 46","ec_funded":1,"date_created":"2018-12-11T11:53:23Z","citation":{"ieee":"S. Bogomolov, D. Magazzeni, S. Minopoli, and M. Wehrle, “PDDL+ planning with hybrid automata: Foundations of translating must behavior,” presented at the ICAPS: International Conference on Automated Planning and Scheduling, Jerusalem, Israel, 2015, pp. 42–46.","ama":"Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. PDDL+ planning with hybrid automata: Foundations of translating must behavior. In: AAAI Press; 2015:42-46.","ista":"Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. 2015. PDDL+ planning with hybrid automata: Foundations of translating must behavior. ICAPS: International Conference on Automated Planning and Scheduling, 42–46.","chicago":"Bogomolov, Sergiy, Daniele Magazzeni, Stefano Minopoli, and Martin Wehrle. “PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior,” 42–46. AAAI Press, 2015.","apa":"Bogomolov, S., Magazzeni, D., Minopoli, S., &#38; Wehrle, M. (2015). PDDL+ planning with hybrid automata: Foundations of translating must behavior (pp. 42–46). Presented at the ICAPS: International Conference on Automated Planning and Scheduling, Jerusalem, Israel: AAAI Press.","short":"S. Bogomolov, D. Magazzeni, S. Minopoli, M. Wehrle, in:, AAAI Press, 2015, pp. 42–46.","mla":"Bogomolov, Sergiy, et al. <i>PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior</i>. AAAI Press, 2015, pp. 42–46."},"publisher":"AAAI Press","main_file_link":[{"url":"https://www.aaai.org/ocs/index.php/ICAPS/ICAPS15/paper/view/10606/10394","open_access":"1"}],"publist_id":"5479","abstract":[{"lang":"eng","text":"Planning in hybrid domains poses a special challenge due to the involved mixed discrete-continuous dynamics. A recent solving approach for such domains is based on applying model checking techniques on a translation of PDDL+ planning problems to hybrid automata. However, the proposed translation is limited because must behavior is only overapproximated, and hence, processes and events are not reflected exactly. In this paper, we present the theoretical foundation of an exact PDDL+ translation. We propose a schema to convert a hybrid automaton with must transitions into an equivalent hybrid automaton featuring only may transitions."}],"_id":"1670","type":"conference","language":[{"iso":"eng"}],"month":"06","status":"public","acknowledgement":"This work was partly supported 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/), 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 Swiss National Science Foundation (SNSF) as part of the project “Automated Reformulation and Pruning in Factored State Spaces (ARAP)”.","scopus_import":"1","conference":{"end_date":"2015-06-11","location":"Jerusalem, Israel","start_date":"2015-06-07","name":"ICAPS: International Conference on Automated Planning and Scheduling"}},{"volume":17,"date_created":"2018-12-11T11:53:26Z","citation":{"short":"J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational Logic 17 (2015).","mla":"Michaliszyn, Jakub, et al. “On the Decidability of Elementary Modal Logics.” <i>ACM Transactions on Computational Logic</i>, vol. 17, no. 1, 2, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2817825\">10.1145/2817825</a>.","ama":"Michaliszyn J, Otop J, Kieroňski E. On the decidability of elementary modal logics. <i>ACM Transactions on Computational Logic</i>. 2015;17(1). doi:<a href=\"https://doi.org/10.1145/2817825\">10.1145/2817825</a>","ieee":"J. Michaliszyn, J. Otop, and E. Kieroňski, “On the decidability of elementary modal logics,” <i>ACM Transactions on Computational Logic</i>, vol. 17, no. 1. ACM, 2015.","chicago":"Michaliszyn, Jakub, Jan Otop, and Emanuel Kieroňski. “On the Decidability of Elementary Modal Logics.” <i>ACM Transactions on Computational Logic</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2817825\">https://doi.org/10.1145/2817825</a>.","apa":"Michaliszyn, J., Otop, J., &#38; Kieroňski, E. (2015). On the decidability of elementary modal logics. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/2817825\">https://doi.org/10.1145/2817825</a>","ista":"Michaliszyn J, Otop J, Kieroňski E. 2015. On the decidability of elementary modal logics. ACM Transactions on Computational Logic. 17(1), 2."},"intvolume":"        17","publication":"ACM Transactions on Computational Logic","publisher":"ACM","ec_funded":1,"oa_version":"None","date_updated":"2025-09-23T09:43:38Z","issue":"1","scopus_import":"1","status":"public","month":"09","language":[{"iso":"eng"}],"external_id":{"isi":["000367919000002"]},"isi":1,"article_number":"2","type":"journal_article","publist_id":"5468","abstract":[{"lang":"eng","text":"We consider the satisfiability problem for modal logic over first-order definable classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008] that modal logic is decidable over classes definable by universal Horn formulae. We provide a full classification of Horn formulae with respect to the complexity of the corresponding satisfiability problem. It turns out, that except for the trivial case of inconsistent formulae, local satisfiability is eitherNP-complete or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete, or ExpTime-complete. We also show that the finite satisfiability problem for modal logic over Horn definable classes of frames is decidable. On the negative side, we show undecidability of two related problems. First, we exhibit a simple universal three-variable formula defining the class of frames over which modal logic is undecidable. Second, we consider the satisfiability problem of bimodal logic over Horn definable classes of frames, and also present a formula leading to undecidability."}],"_id":"1680","article_processing_charge":"No","date_published":"2015-09-01T00:00:00Z","author":[{"first_name":"Jakub","full_name":"Michaliszyn, Jakub","last_name":"Michaliszyn"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"},{"first_name":"Emanuel","full_name":"Kieroňski, Emanuel","last_name":"Kieroňski"}],"day":"01","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2015","publication_status":"published","title":"On the decidability of elementary modal logics","department":[{"_id":"ToHe"}],"quality_controlled":"1","doi":"10.1145/2817825","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}]},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"}],"doi":"10.1145/2728606.2728608","arxiv":1,"article_processing_charge":"No","author":[{"last_name":"Svoreňová","full_name":"Svoreňová, Mária","first_name":"Mária"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Cěrná","first_name":"Ivana","full_name":"Cěrná, Ivana"},{"first_name":"Cǎlin","full_name":"Belta, Cǎlin","last_name":"Belta"}],"day":"14","date_published":"2015-04-14T00:00:00Z","year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","scopus_import":"1","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","start_date":"2015-04-14","end_date":"2015-04-16","location":"Seattle, WA, United States"},"status":"public","external_id":{"arxiv":["1410.5387"]},"language":[{"iso":"eng"}],"month":"04","publist_id":"5456","abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study."}],"_id":"1689","type":"conference","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"ec_funded":1,"page":"259 - 268","date_created":"2018-12-11T11:53:29Z","citation":{"short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–268.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 259–68, doi:<a href=\"https://doi.org/10.1145/2728606.2728608\">10.1145/2728606.2728608</a>.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” in <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, Seattle, WA, United States, 2015, pp. 259–268.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2015:259-268. doi:<a href=\"https://doi.org/10.1145/2728606.2728608\">10.1145/2728606.2728608</a>","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 259–68. ACM, 2015. <a href=\"https://doi.org/10.1145/2728606.2728608\">https://doi.org/10.1145/2728606.2728608</a>.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i> (pp. 259–268). Seattle, WA, United States: ACM. <a href=\"https://doi.org/10.1145/2728606.2728608\">https://doi.org/10.1145/2728606.2728608</a>","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268."},"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","publisher":"ACM","oa_version":"Preprint","date_updated":"2025-06-11T06:33:00Z","oa":1,"related_material":{"record":[{"id":"1407","relation":"later_version","status":"public"}]}},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2015","oa_version":"None","date_updated":"2025-04-15T06:26:00Z","publication_status":"published","date_created":"2018-12-11T11:53:29Z","citation":{"ama":"Bak S, Bogomolov S, Johnson T. HYST: A source transformation and translation tool for hybrid automaton models. In: Springer; 2015:128-133. doi:<a href=\"https://doi.org/10.1145/2728606.2728630\">10.1145/2728606.2728630</a>","ieee":"S. Bak, S. Bogomolov, and T. Johnson, “HYST: A source transformation and translation tool for hybrid automaton models,” presented at the HSCC: Hybrid Systems - Computation and Control, Seattle, WA, United States, 2015, pp. 128–133.","ista":"Bak S, Bogomolov S, Johnson T. 2015. HYST: A source transformation and translation tool for hybrid automaton models. HSCC: Hybrid Systems - Computation and Control, 128–133.","chicago":"Bak, Stanley, Sergiy Bogomolov, and Taylor Johnson. “HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models,” 128–33. Springer, 2015. <a href=\"https://doi.org/10.1145/2728606.2728630\">https://doi.org/10.1145/2728606.2728630</a>.","apa":"Bak, S., Bogomolov, S., &#38; Johnson, T. (2015). HYST: A source transformation and translation tool for hybrid automaton models (pp. 128–133). Presented at the HSCC: Hybrid Systems - Computation and Control, Seattle, WA, United States: Springer. <a href=\"https://doi.org/10.1145/2728606.2728630\">https://doi.org/10.1145/2728606.2728630</a>","short":"S. Bak, S. Bogomolov, T. Johnson, in:, Springer, 2015, pp. 128–133.","mla":"Bak, Stanley, et al. <i>HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models</i>. Springer, 2015, pp. 128–33, doi:<a href=\"https://doi.org/10.1145/2728606.2728630\">10.1145/2728606.2728630</a>."},"publisher":"Springer","date_published":"2015-04-14T00:00:00Z","ec_funded":1,"author":[{"full_name":"Bak, Stanley","first_name":"Stanley","last_name":"Bak"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"first_name":"Taylor","full_name":"Johnson, Taylor","last_name":"Johnson"}],"page":"128 - 133","day":"14","month":"04","language":[{"iso":"eng"}],"quality_controlled":"1","doi":"10.1145/2728606.2728630","type":"conference","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"publist_id":"5454","abstract":[{"lang":"eng","text":"A number of powerful and scalable hybrid systems model checkers have recently emerged. Although all of them honor roughly the same hybrid systems semantics, they have drastically different model description languages. This situation (a) makes it difficult to quickly evaluate a specific hybrid automaton model using the different tools, (b) obstructs comparisons of reachability approaches, and (c) impedes the widespread application of research results that perform model modification and could benefit many of the tools. In this paper, we present Hyst, a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of HyCreate, Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation passes that serve to both ease the translation and potentially improve reachability results for the supported tools. Although these model transformation passes could be implemented within each tool, the Hyst approach provides a single place for model modification, generating modified input sources for the unmodified target tools. Our evaluation demonstrates Hyst is capable of automatically translating benchmarks in several classes (including affine and nonlinear hybrid automata) to the input formats of several tools. Additionally, we illustrate a general model transformation pass based on pseudo-invariants implemented in Hyst that illustrates the reachability improvement."}],"_id":"1690","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2015-04-16","location":"Seattle, WA, United States","start_date":"2015-04-14"},"scopus_import":"1","title":"HYST: A source transformation and translation tool for hybrid automaton models","status":"public","acknowledgement":"The material presented in this paper is based upon work sup-ported by the Air Force Research Laboratory’s Information Directorate (AFRL/RI) through the Visiting Faculty Research Program (VFRP) under contract number FA8750-13-2-0115 and the Air Force Office of Scientific Research (AFOSR). Any opinions,findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the AFRL/RI or AFOSR. This work was also partly supported in part by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR14 AVACS, http://www.avacs.org/), by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}]},{"scopus_import":1,"conference":{"start_date":"2015-04-14","location":"Seattle, WA, United States","end_date":"2015-04-16","name":"HSCC: Hybrid Systems - Computation and Control"},"department":[{"_id":"ToHe"}],"title":"Eliminating spurious transitions in reachability with support functions","status":"public","language":[{"iso":"eng"}],"month":"04","publist_id":"5452","abstract":[{"text":"Computing an approximation of the reachable states of a hybrid system is a challenge, mainly because overapproximating the solutions of ODEs with a finite number of sets does not scale well. Using template polyhedra can greatly reduce the computational complexity, since it replaces complex operations on sets with a small number of optimization problems. However, the use of templates may make the over-approximation too conservative. Spurious transitions, which are falsely considered reachable, are particularly detrimental to performance and accuracy, and may exacerbate the state explosion problem. In this paper, we examine how spurious transitions can be avoided with minimal computational effort. To this end, detecting spurious transitions is reduced to the well-known problem of showing that two convex sets are disjoint by finding a hyperplane that separates them. We generalize this to owpipes by considering hyperplanes that evolve with time in correspondence to the dynamics of the system. The approach is implemented in the model checker SpaceEx and demonstrated on examples.","lang":"eng"}],"_id":"1692","quality_controlled":"1","type":"conference","doi":"10.1145/2728606.2728622","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"publication_identifier":{"isbn":["978-1-4503-3433-4"]},"ec_funded":1,"author":[{"full_name":"Frehse, Goran","first_name":"Goran","last_name":"Frehse"},{"last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"first_name":"Marius","full_name":"Greitschus, Marius","last_name":"Greitschus"},{"last_name":"Strump","full_name":"Strump, Thomas","first_name":"Thomas"},{"last_name":"Podelski","full_name":"Podelski, Andreas","first_name":"Andreas"}],"page":"149 - 158","day":"14","date_created":"2018-12-11T11:53:30Z","citation":{"mla":"Frehse, Goran, et al. “Eliminating Spurious Transitions in Reachability with Support Functions.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 149–58, doi:<a href=\"https://doi.org/10.1145/2728606.2728622\">10.1145/2728606.2728622</a>.","short":"G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, A. Podelski, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 149–158.","chicago":"Frehse, Goran, Sergiy Bogomolov, Marius Greitschus, Thomas Strump, and Andreas Podelski. “Eliminating Spurious Transitions in Reachability with Support Functions.” In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 149–58. ACM, 2015. <a href=\"https://doi.org/10.1145/2728606.2728622\">https://doi.org/10.1145/2728606.2728622</a>.","apa":"Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., &#38; Podelski, A. (2015). Eliminating spurious transitions in reachability with support functions. In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i> (pp. 149–158). Seattle, WA, United States: ACM. <a href=\"https://doi.org/10.1145/2728606.2728622\">https://doi.org/10.1145/2728606.2728622</a>","ista":"Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. 2015. Eliminating spurious transitions in reachability with support functions. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 149–158.","ieee":"G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, and A. Podelski, “Eliminating spurious transitions in reachability with support functions,” in <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, Seattle, WA, United States, 2015, pp. 149–158.","ama":"Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. Eliminating spurious transitions in reachability with support functions. In: <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2015:149-158. doi:<a href=\"https://doi.org/10.1145/2728606.2728622\">10.1145/2728606.2728622</a>"},"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","publisher":"ACM","date_published":"2015-04-14T00:00:00Z","oa_version":"None","year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","date_updated":"2025-04-15T06:26:00Z"},{"oa_version":"Preprint","oa":1,"date_updated":"2025-09-23T13:47:20Z","main_file_link":[{"url":"http://arxiv.org/abs/1209.3234","open_access":"1"}],"volume":241,"page":"177 - 196","ec_funded":1,"date_created":"2018-12-11T11:53:32Z","citation":{"ieee":"Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J. Raskin, “The complexity of multi-mean-payoff and multi-energy games,” <i>Information and Computation</i>, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.","ama":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. 2015;241(4):177-196. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>","apa":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &#38; Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>","chicago":"Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger, Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>.","ista":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015. The complexity of multi-mean-payoff and multi-energy games. Information and Computation. 241(4), 177–196.","short":"Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.","mla":"Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” <i>Information and Computation</i>, vol. 241, no. 4, Elsevier, 2015, pp. 177–96, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>."},"intvolume":"       241","publication":"Information and Computation","publisher":"Elsevier","external_id":{"arxiv":["1209.3234"],"isi":["000353352800008"]},"isi":1,"language":[{"iso":"eng"}],"month":"04","publist_id":"5443","abstract":[{"text":"In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf objectives are coNP-complete.","lang":"eng"}],"_id":"1698","type":"journal_article","scopus_import":"1","issue":"4","status":"public","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148), ERC Start grant (279499: inVEST).","year":"2015","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_status":"published","corr_author":"1","arxiv":1,"article_processing_charge":"No","author":[{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Alexander","full_name":"Rabinovich, Alexander","last_name":"Rabinovich"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"}],"day":"01","date_published":"2015-04-01T00:00:00Z","quality_controlled":"1","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"doi":"10.1016/j.ic.2015.03.001","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"The complexity of multi-mean-payoff and multi-energy games"},{"abstract":[{"text":"Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.","lang":"eng"}],"publist_id":"5255","has_accepted_license":"1","_id":"1846","type":"journal_article","isi":1,"external_id":{"isi":["000351160200008"]},"language":[{"iso":"eng"}],"month":"04","status":"public","scopus_import":"1","file_date_updated":"2020-07-14T12:45:19Z","issue":"2-3","oa":1,"date_updated":"2025-09-23T10:33:12Z","oa_version":"Submitted Version","ec_funded":1,"page":"269 - 297","date_created":"2018-12-11T11:54:20Z","ddc":["000"],"intvolume":"        52","citation":{"mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>.","short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>.","apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., &#38; Srba, J. (2015). Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>","ista":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.","ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. 2015;52(2-3):269-297. doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>","ieee":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” <i>Acta Informatica</i>, vol. 52, no. 2–3. Springer, pp. 269–297, 2015."},"publication":"Acta Informatica","publisher":"Springer","article_type":"original","volume":52,"quality_controlled":"1","doi":"10.1007/s00236-015-0215-4","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Refinement checking on parametric modal transition systems","file":[{"file_size":488482,"checksum":"fb4037ddc4fc05f33080dd3547ede350","content_type":"application/pdf","date_created":"2020-05-15T08:57:44Z","relation":"main_file","access_level":"open_access","file_id":"7854","file_name":"2015_ActaInfo_Benes.pdf","creator":"dernst","date_updated":"2020-07-14T12:45:19Z"}],"publication_status":"published","year":"2015","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"last_name":"Beneš","full_name":"Beneš, Nikola","first_name":"Nikola"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"last_name":"Larsen","full_name":"Larsen, Kim","first_name":"Kim"},{"full_name":"Möller, Mikael","first_name":"Mikael","last_name":"Möller"},{"last_name":"Sickert","full_name":"Sickert, Salomon","first_name":"Salomon"},{"full_name":"Srba, Jiří","first_name":"Jiří","last_name":"Srba"}],"day":"01","date_published":"2015-04-01T00:00:00Z","corr_author":"1","article_processing_charge":"No"},{"ec_funded":1,"publication":"Journal of the ACM","publisher":"ACM","date_created":"2018-12-11T11:54:23Z","intvolume":"        62","citation":{"short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM 62 (2015).","mla":"Chatterjee, Krishnendu, et al. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>, vol. 62, no. 1, 9, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>.","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. 2015;62(1). doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and synthesizing systems in probabilistic environments,” <i>Journal of the ACM</i>, vol. 62, no. 1. ACM, 2015.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2015). Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2015. Measuring and synthesizing systems in probabilistic environments. Journal of the ACM. 62(1), 9."},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1004.0739"}],"volume":62,"related_material":{"record":[{"id":"3864","status":"public","relation":"earlier_version"}]},"oa":1,"date_updated":"2025-09-23T09:33:01Z","oa_version":"Preprint","status":"public","scopus_import":"1","issue":"1","_id":"1856","abstract":[{"text":"The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε &gt; 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.","lang":"eng"}],"publist_id":"5244","type":"journal_article","article_number":"9","isi":1,"language":[{"iso":"eng"}],"external_id":{"isi":["000350563000009"],"arxiv":["1004.0739"]},"month":"02","day":"01","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Jobstmann","first_name":"Barbara","full_name":"Jobstmann, Barbara"},{"full_name":"Singh, Rohit","first_name":"Rohit","last_name":"Singh"}],"date_published":"2015-02-01T00:00:00Z","arxiv":1,"article_processing_charge":"No","publication_status":"published","year":"2015","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Measuring and synthesizing systems in probabilistic environments","doi":"10.1145/2699430","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1"},{"oa_version":"None","date_updated":"2025-09-23T09:36:19Z","volume":25,"publication":"ACM Transactions on Modeling and Computer Simulation","publisher":"ACM","citation":{"ama":"Ruess J, Lygeros J. Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2688906\">10.1145/2688906</a>","ieee":"J. Ruess and J. Lygeros, “Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","ista":"Ruess J, Lygeros J. 2015. Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. ACM Transactions on Modeling and Computer Simulation. 25(2), 8.","chicago":"Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference and Experiment Design for Stochastic Biochemical Reaction Networks.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2688906\">https://doi.org/10.1145/2688906</a>.","apa":"Ruess, J., &#38; Lygeros, J. (2015). Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2688906\">https://doi.org/10.1145/2688906</a>","short":"J. Ruess, J. Lygeros, ACM Transactions on Modeling and Computer Simulation 25 (2015).","mla":"Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference and Experiment Design for Stochastic Biochemical Reaction Networks.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 8, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2688906\">10.1145/2688906</a>."},"date_created":"2018-12-11T11:54:25Z","intvolume":"        25","article_number":"8","language":[{"iso":"eng"}],"isi":1,"external_id":{"isi":["000354789200002"]},"month":"02","_id":"1861","publist_id":"5238","abstract":[{"lang":"eng","text":"Continuous-time Markov chains are commonly used in practice for modeling biochemical reaction networks in which the inherent randomness of themolecular interactions cannot be ignored. This has motivated recent research effort into methods for parameter inference and experiment design for such models. The major difficulty is that such methods usually require one to iteratively solve the chemical master equation that governs the time evolution of the probability distribution of the system. This, however, is rarely possible, and even approximation techniques remain limited to relatively small and simple systems. An alternative explored in this article is to base methods on only some low-order moments of the entire probability distribution. We summarize the theory behind such moment-based methods for parameter inference and experiment design and provide new case studies where we investigate their performance."}],"type":"journal_article","scopus_import":"1","issue":"2","acknowledgement":"HYCON2; EC; European Commission\r\n","status":"public","year":"2015","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_status":"published","article_processing_charge":"No","day":"01","author":[{"last_name":"Ruess","orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","first_name":"Jakob","full_name":"Ruess, Jakob"},{"first_name":"John","full_name":"Lygeros, John","last_name":"Lygeros"}],"date_published":"2015-02-01T00:00:00Z","doi":"10.1145/2688906","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"title":"Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks"},{"department":[{"_id":"ToHe"}],"status":"public","title":"The equivalence problem for finite automata: Technical perspective","scopus_import":"1","issue":"2","_id":"1866","publist_id":"5232","type":"journal_article","doi":"10.1145/2701001","external_id":{"isi":["000349299600024"]},"isi":1,"language":[{"iso":"eng"}],"month":"01","day":"28","page":"86-86","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"publisher":"ACM","publication":"Communications of the ACM","date_published":"2015-01-28T00:00:00Z","date_created":"2018-12-11T11:54:26Z","intvolume":"        58","citation":{"apa":"Henzinger, T. A., &#38; Raskin, J. (2015). The equivalence problem for finite automata: Technical perspective. <i>Communications of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2701001\">https://doi.org/10.1145/2701001</a>","chicago":"Henzinger, Thomas A, and Jean Raskin. “The Equivalence Problem for Finite Automata: Technical Perspective.” <i>Communications of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2701001\">https://doi.org/10.1145/2701001</a>.","ista":"Henzinger TA, Raskin J. 2015. The equivalence problem for finite automata: Technical perspective. Communications of the ACM. 58(2), 86–86.","ieee":"T. A. Henzinger and J. Raskin, “The equivalence problem for finite automata: Technical perspective,” <i>Communications of the ACM</i>, vol. 58, no. 2. ACM, pp. 86–86, 2015.","ama":"Henzinger TA, Raskin J. The equivalence problem for finite automata: Technical perspective. <i>Communications of the ACM</i>. 2015;58(2):86-86. doi:<a href=\"https://doi.org/10.1145/2701001\">10.1145/2701001</a>","mla":"Henzinger, Thomas A., and Jean Raskin. “The Equivalence Problem for Finite Automata: Technical Perspective.” <i>Communications of the ACM</i>, vol. 58, no. 2, ACM, 2015, pp. 86–86, doi:<a href=\"https://doi.org/10.1145/2701001\">10.1145/2701001</a>.","short":"T.A. Henzinger, J. Raskin, Communications of the ACM 58 (2015) 86–86."},"article_processing_charge":"No","volume":58,"publication_status":"published","date_updated":"2025-09-23T13:49:40Z","year":"2015","oa_version":"None","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"publication_status":"published","year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"30","author":[{"full_name":"Fahrenberg, Uli","first_name":"Uli","last_name":"Fahrenberg"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"last_name":"Legay","full_name":"Legay, Axel","first_name":"Axel"},{"full_name":"Traonouez, Louis","first_name":"Louis","last_name":"Traonouez"}],"date_published":"2015-01-30T00:00:00Z","article_processing_charge":"No","arxiv":1,"corr_author":"1","doi":"10.1007/978-3-319-15317-9_19","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Compositionality for quantitative specifications","date_updated":"2025-06-11T07:22:00Z","oa":1,"oa_version":"Preprint","alternative_title":["LNCS"],"page":"306 - 324","ec_funded":1,"publisher":"Springer","intvolume":"      8997","date_created":"2018-12-11T11:54:31Z","citation":{"short":"U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324.","mla":"Fahrenberg, Uli, et al. <i>Compositionality for Quantitative Specifications</i>. Vol. 8997, Springer, 2015, pp. 306–24, doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>.","ieee":"U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.","ama":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative specifications. In: Vol 8997. Springer; 2015:306-324. doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>","ista":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.","apa":"Fahrenberg, U., Kretinsky, J., Legay, A., &#38; Traonouez, L. (2015). Compositionality for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>","chicago":"Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality for Quantitative Specifications,” 8997:306–24. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>."},"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1408.1256"}],"volume":8997,"_id":"1882","abstract":[{"lang":"eng","text":"We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations."}],"publist_id":"5216","type":"conference","external_id":{"arxiv":["1408.1256"]},"language":[{"iso":"eng"}],"month":"01","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.","status":"public","scopus_import":"1","conference":{"end_date":"2014-09-12","location":"Bertinoro, Italy","start_date":"2014-09-10","name":"FACS: Formal Aspects of Component Software"}},{"related_material":{"record":[{"relation":"later_version","status":"public","id":"1659"}]},"date_updated":"2025-04-15T08:11:50Z","oa":1,"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["IST Austria Technical Report"],"year":"2015","oa_version":"Published Version","date_published":"2015-05-18T00:00:00Z","publisher":"IST Austria","ddc":["004","512","513"],"date_created":"2018-12-12T11:39:20Z","citation":{"short":"U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST Austria, 2015.","mla":"Boker, Udi, et al. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>.","ieee":"U. Boker, T. A. Henzinger, and J. Otop, <i>The target discounted-sum problem</i>. IST Austria, 2015.","ama":"Boker U, Henzinger TA, Otop J. <i>The Target Discounted-Sum Problem</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">10.15479/AT:IST-2015-335-v1-1</a>","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST Austria, 20p.","chicago":"Boker, Udi, Thomas A Henzinger, and Jan Otop. <i>The Target Discounted-Sum Problem</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>.","apa":"Boker, U., Henzinger, T. A., &#38; Otop, J. (2015). <i>The target discounted-sum problem</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-335-v1-1\">https://doi.org/10.15479/AT:IST-2015-335-v1-1</a>"},"day":"18","pubrep_id":"335","author":[{"last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","full_name":"Boker, Udi"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","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"}],"page":"20","publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2015-335-v1-1","type":"technical_report","has_accepted_license":"1","_id":"5439","abstract":[{"text":"The target discounted-sum problem is the following: Given a rational discount factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata. ","lang":"eng"}],"month":"05","language":[{"iso":"eng"}],"status":"public","title":"The target discounted-sum problem","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:46:55Z","file":[{"date_updated":"2020-07-14T12:46:55Z","creator":"system","access_level":"open_access","file_id":"5517","file_name":"IST-2015-335-v1+1_report.pdf","date_created":"2018-12-12T11:53:55Z","relation":"main_file","checksum":"40405907aa012acece1bc26cf0be554d","content_type":"application/pdf","file_size":589619}]},{"year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"13","author":[{"full_name":"Fellner, Andreas","first_name":"Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","last_name":"Fellner"}],"tmp":{"name":"Creative Commons Public Domain Dedication (CC0 1.0)","short":"CC0 (1.0)","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","image":"/images/cc_0.png"},"date_published":"2015-08-13T00:00:00Z","article_processing_charge":"No","license":"https://creativecommons.org/publicdomain/zero/1.0/","project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"doi":"10.15479/AT:ISTA:28","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","file":[{"file_size":49557109,"content_type":"application/zip","checksum":"b8bcb43c0893023cda66c1b69c16ac62","relation":"main_file","date_created":"2018-12-12T13:02:31Z","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","file_id":"5597","access_level":"open_access","creator":"system","date_updated":"2020-07-14T12:47:00Z"}],"related_material":{"record":[{"status":"public","relation":"popular_science","id":"1603"}]},"date_updated":"2025-09-23T08:23:15Z","oa":1,"oa_version":"Published Version","contributor":[{"last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"ec_funded":1,"publisher":"Institute of Science and Technology Austria","date_created":"2018-12-12T12:31:29Z","citation":{"ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>.","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>","ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015.","mla":"Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute of Science and Technology Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","short":"A. Fellner, (2015)."},"ddc":["004"],"datarep_id":"28","_id":"5549","has_accepted_license":"1","publist_id":"5564","abstract":[{"text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication.","lang":"eng"}],"type":"research_data","month":"08","status":"public","keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"file_date_updated":"2020-07-14T12:47:00Z"},{"publication_status":"published","year":"2015","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"15","pubrep_id":"317","author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","full_name":"Radhakrishna, Arjun"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","full_name":"Samanta, Roopsha","first_name":"Roopsha"},{"full_name":"Tarrach, Thorsten","first_name":"Thorsten","orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach"}],"date_published":"2015-01-15T00:00:00Z","article_processing_charge":"No","doi":"10.1145/2676726.2677008","quality_controlled":"1","department":[{"_id":"ToHe"}],"title":"Succinct representation of concurrent trace sets","file":[{"date_updated":"2020-07-14T12:45:22Z","creator":"system","file_id":"5314","access_level":"open_access","file_name":"IST-2015-317-v1+1_author_version.pdf","date_created":"2018-12-12T10:17:56Z","relation":"main_file","checksum":"f0d4395b600f410a191256ac0b73af32","content_type":"application/pdf","file_size":399462}],"date_updated":"2025-03-07T08:44:29Z","oa":1,"oa_version":"Submitted Version","page":"433 - 444","publisher":"ACM","ddc":["005"],"date_created":"2018-12-11T11:55:05Z","citation":{"ieee":"A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct representation of concurrent trace sets,” presented at the POPL: Principles of Programming Languages, Mumbai, India, 2015, pp. 433–444.","ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>","apa":"Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>.","ista":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct representation of concurrent trace sets. POPL: Principles of Programming Languages, 433–444.","short":"A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM, 2015, pp. 433–444.","mla":"Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>. ACM, 2015, pp. 433–44, doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>."},"publication_identifier":{"isbn":["978-1-4503-3300-9"]},"has_accepted_license":"1","_id":"1992","abstract":[{"lang":"eng","text":"We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.\r\n\r\nWe claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula."}],"publist_id":"5091","type":"conference","language":[{"iso":"eng"}],"month":"01","status":"public","scopus_import":"1","file_date_updated":"2020-07-14T12:45:22Z","conference":{"location":"Mumbai, India","end_date":"2015-01-17","start_date":"2015-01-15","name":"POPL: Principles of Programming Languages"}},{"keyword":["General Environmental Science"],"status":"public","acknowledgement":"The authors would like to acknowledge contributions from Baptiste Mottet who performed preliminary analysis regarding parameter inference for the considered case study in a student project (Mottet, 2014/2015).\r\nThe research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement No. [291734] and from SystemsX under the project SignalX.","scopus_import":"1","file_date_updated":"2022-02-25T11:55:26Z","type":"journal_article","abstract":[{"text":"Mathematical models are of fundamental importance in the understanding of complex population dynamics. For instance, they can be used to predict the population evolution starting from different initial conditions or to test how a system responds to external perturbations. For this analysis to be meaningful in real applications, however, it is of paramount importance to choose an appropriate model structure and to infer the model parameters from measured data. While many parameter inference methods are available for models based on deterministic ordinary differential equations, the same does not hold for more detailed individual-based models. Here we consider, in particular, stochastic models in which the time evolution of the species abundances is described by a continuous-time Markov chain. These models are governed by a master equation that is typically difficult to solve. Consequently, traditional inference methods that rely on iterative evaluation of parameter likelihoods are computationally intractable. The aim of this paper is to present recent advances in parameter inference for continuous-time Markov chain models, based on a moment closure approximation of the parameter likelihood, and to investigate how these results can help in understanding, and ultimately controlling, complex systems in ecology. Specifically, we illustrate through an agricultural pest case study how parameters of a stochastic individual-based model can be identified from measured data and how the resulting model can be used to solve an optimal control problem in a stochastic setting. In particular, we show how the matter of determining the optimal combination of two different pest control methods can be formulated as a chance constrained optimization problem where the control action is modeled as a state reset, leading to a hybrid system formulation.","lang":"eng"}],"has_accepted_license":"1","_id":"10794","month":"06","language":[{"iso":"eng"}],"article_number":"42","ddc":["000","570"],"intvolume":"         3","citation":{"short":"F. Parise, J. Lygeros, J. Ruess, Frontiers in Environmental Science 3 (2015).","mla":"Parise, Francesca, et al. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>, vol. 3, 42, Frontiers, 2015, doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>.","ieee":"F. Parise, J. Lygeros, and J. Ruess, “Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study,” <i>Frontiers in Environmental Science</i>, vol. 3. Frontiers, 2015.","ama":"Parise F, Lygeros J, Ruess J. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. 2015;3. doi:<a href=\"https://doi.org/10.3389/fenvs.2015.00042\">10.3389/fenvs.2015.00042</a>","chicago":"Parise, Francesca, John Lygeros, and Jakob Ruess. “Bayesian Inference for Stochastic Individual-Based Models of Ecological Systems: A Pest Control Simulation Study.” <i>Frontiers in Environmental Science</i>. Frontiers, 2015. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>.","apa":"Parise, F., Lygeros, J., &#38; Ruess, J. (2015). Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. <i>Frontiers in Environmental Science</i>. Frontiers. <a href=\"https://doi.org/10.3389/fenvs.2015.00042\">https://doi.org/10.3389/fenvs.2015.00042</a>","ista":"Parise F, Lygeros J, Ruess J. 2015. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. Frontiers in Environmental Science. 3, 42."},"date_created":"2022-02-25T11:42:25Z","publisher":"Frontiers","publication":"Frontiers in Environmental Science","ec_funded":1,"publication_identifier":{"issn":["2296-665X"]},"volume":3,"article_type":"original","date_updated":"2025-04-15T06:50:01Z","oa":1,"oa_version":"Published Version","title":"Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"file":[{"success":1,"file_size":1371201,"relation":"main_file","date_created":"2022-02-25T11:55:26Z","content_type":"application/pdf","checksum":"26c222487564e1be02a11d688d6f769d","file_name":"2015_FrontiersEnvironmScience_Parise.pdf","file_id":"10795","access_level":"open_access","date_updated":"2022-02-25T11:55:26Z","creator":"dernst"}],"quality_controlled":"1","project":[{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"doi":"10.3389/fenvs.2015.00042","date_published":"2015-06-10T00:00:00Z","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"author":[{"last_name":"Parise","full_name":"Parise, Francesca","first_name":"Francesca"},{"full_name":"Lygeros, John","first_name":"John","last_name":"Lygeros"},{"last_name":"Ruess","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282","first_name":"Jakob","full_name":"Ruess, Jakob"}],"day":"10","license":"https://creativecommons.org/licenses/by/4.0/","corr_author":"1","article_processing_charge":"No","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2015"},{"status":"public","conference":{"start_date":"2015-07-18","end_date":"2015-07-24","location":"San Francisco, CA, United States","name":"CAV: Computer Aided Verification"},"file_date_updated":"2025-06-26T07:12:35Z","scopus_import":"1","type":"conference","_id":"1729","has_accepted_license":"1","OA_place":"repository","publist_id":"5398","abstract":[{"text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of such sequences produced under a non-preemptive scheduler. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and rules for inserting synchronization. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient, and, since it does not require explicit specifications, is more practical than the conventional approach based on user-provided assertions.","lang":"eng"}],"month":"07","series_title":"Lecture Notes in Computer Science","isi":1,"external_id":{"isi":["000491470400011"]},"language":[{"iso":"eng"}],"OA_type":"green","publisher":"Springer","ddc":["000"],"citation":{"ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. 2015;9207:180-197. doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</a>","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” vol. 9207. Springer, pp. 180–197, 2015.","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>.","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2015). From non-preemptive to preemptive scheduling using synchronization synthesis. Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2015. From non-preemptive to preemptive scheduling using synchronization synthesis. 9207, 180–197.","short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, 9207 (2015) 180–197.","mla":"Cerny, Pavol, et al. <i>From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis</i>. Vol. 9207, Springer, 2015, pp. 180–97, doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</a>."},"intvolume":"      9207","date_created":"2018-12-11T11:53:42Z","ec_funded":1,"page":"180 - 197","volume":9207,"related_material":{"record":[{"id":"1338","status":"public","relation":"later_version"},{"status":"public","relation":"dissertation_contains","id":"1130"}]},"date_updated":"2026-04-09T10:54:00Z","oa":1,"alternative_title":["LNCS"],"oa_version":"Submitted Version","title":"From non-preemptive to preemptive scheduling using synchronization synthesis","department":[{"_id":"ToHe"}],"file":[{"relation":"main_file","date_created":"2018-12-12T10:08:53Z","content_type":"application/pdf","checksum":"6ff58ac220e2f20cb001ba35d4924495","file_size":481922,"date_updated":"2025-06-26T07:12:35Z","creator":"system","file_name":"IST-2015-336-v1+1_long_version.pdf","access_level":"open_access","file_id":"4715"}],"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"doi":"10.1007/978-3-319-21668-3_11","quality_controlled":"1","date_published":"2015-07-01T00:00:00Z","day":"01","author":[{"first_name":"Pavol","full_name":"Cerny, Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Clarke","first_name":"Edmund","full_name":"Clarke, Edmund"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Radhakrishna, Arjun","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","last_name":"Radhakrishna"},{"last_name":"Ryzhyk","first_name":"Leonid","full_name":"Ryzhyk, Leonid"},{"full_name":"Samanta, Roopsha","first_name":"Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta"},{"orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach","full_name":"Tarrach, Thorsten","first_name":"Thorsten"}],"pubrep_id":"336","article_processing_charge":"No","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2015"},{"oa":1,"date_updated":"2025-09-23T10:32:00Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3856"}]},"oa_version":"Preprint","date_created":"2018-12-11T11:53:42Z","citation":{"short":"K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation 245 (2015) 3–16.","mla":"Chatterjee, Krishnendu, et al. “Randomness for Free.” <i>Information and Computation</i>, vol. 245, no. 12, Elsevier, 2015, pp. 3–16, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>.","ama":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. <i>Information and Computation</i>. 2015;245(12):3-16. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>","ieee":"K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for free,” <i>Information and Computation</i>, vol. 245, no. 12. Elsevier, pp. 3–16, 2015.","ista":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free. Information and Computation. 245(12), 3–16.","apa":"Chatterjee, K., Doyen, L., Gimbert, H., &#38; Henzinger, T. A. (2015). Randomness for free. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger. “Randomness for Free.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">https://doi.org/10.1016/j.ic.2015.06.003</a>."},"intvolume":"       245","publisher":"Elsevier","publication":"Information and Computation","page":"3 - 16","ec_funded":1,"volume":245,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1006.0673"}],"type":"journal_article","publist_id":"5395","abstract":[{"text":"We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (both players interact simultaneously); and (b) turn-based (both players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. In this work we present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games. ","lang":"eng"}],"_id":"1731","month":"12","isi":1,"external_id":{"arxiv":["1006.0673"],"isi":["000368899100002"]},"language":[{"iso":"eng"}],"status":"public","issue":"12","scopus_import":"1","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2015","date_published":"2015-12-01T00:00:00Z","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"last_name":"Gimbert","first_name":"Hugo","full_name":"Gimbert, Hugo"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"day":"01","corr_author":"1","article_processing_charge":"No","arxiv":1,"quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543"},{"name":"Design for Embedded Systems","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"doi":"10.1016/j.ic.2015.06.003","title":"Randomness for free","department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"publication_status":"published","date_updated":"2025-09-23T09:11:51Z","oa_version":"None","year":"2015","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","day":"01","author":[{"last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"publication":"ACM Transactions on Modeling and Computer Simulation","publisher":"ACM","date_published":"2015-05-01T00:00:00Z","date_created":"2018-12-11T11:54:07Z","citation":{"short":"A. Gupta, T.A. Henzinger, ACM Transactions on Modeling and Computer Simulation 25 (2015).","mla":"Gupta, Ashutosh, and Thomas A. Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 7, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>.","ama":"Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>","ieee":"A. Gupta and T. A. Henzinger, “Guest editors’ introduction to special issue on computational methods in systems biology,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","apa":"Gupta, A., &#38; Henzinger, T. A. (2015). Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>","chicago":"Gupta, Ashutosh, and Thomas A Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>.","ista":"Gupta A, Henzinger TA. 2015. Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. 25(2), 7."},"intvolume":"        25","article_processing_charge":"No","volume":25,"_id":"1808","publist_id":"5302","type":"journal_article","doi":"10.1145/2745799","quality_controlled":"1","article_number":"7","external_id":{"isi":["000354789200001"]},"isi":1,"language":[{"iso":"eng"}],"month":"05","department":[{"_id":"ToHe"}],"title":"Guest editors' introduction to special issue on computational methods in systems biology","status":"public","scopus_import":"1","issue":"2"},{"volume":9035,"main_file_link":[{"url":"http://arxiv.org/abs/1410.7704","open_access":"1"}],"citation":{"ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking gene regulatory networks. 2015;9035:469-483. doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking gene regulatory networks,” vol. 9035. Springer, pp. 469–483, 2015.","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model checking gene regulatory networks. 9035, 469–483.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2015). Model checking gene regulatory networks. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking Gene Regulatory Networks.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>.","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483.","mla":"Giacobbe, Mirco, et al. <i>Model Checking Gene Regulatory Networks</i>. Vol. 9035, Springer, 2015, pp. 469–83, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>."},"intvolume":"      9035","date_created":"2018-12-11T11:54:16Z","publisher":"Springer","ec_funded":1,"page":"469 - 483","alternative_title":["LNCS"],"oa_version":"Preprint","oa":1,"date_updated":"2025-07-10T11:50:42Z","related_material":{"record":[{"id":"1351","status":"public","relation":"later_version"}]},"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2015-04-18","location":"London, United Kingdom","start_date":"2015-04-11"},"scopus_import":"1","status":"public","acknowledgement":"SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2 148797.\r\n","month":"04","external_id":{"arxiv":["1410.7704"]},"language":[{"iso":"eng"}],"series_title":"Lecture Notes in Computer Science","type":"conference","abstract":[{"text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs –an important problem of interest in evolutionary biology– more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.","lang":"eng"}],"publist_id":"5267","_id":"1835","arxiv":1,"article_processing_charge":"No","date_published":"2015-04-01T00:00:00Z","author":[{"last_name":"Giacobbe","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","full_name":"Giacobbe, Mirco"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-6220-2052","last_name":"Guet","full_name":"Guet, Calin C","first_name":"Calin C"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2361-3953","last_name":"Paixao","full_name":"Paixao, Tiago","first_name":"Tiago"},{"first_name":"Tatjana","full_name":"Petrov, Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2015","publication_status":"published","title":"Model checking gene regulatory networks","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"quality_controlled":"1","doi":"10.1007/978-3-662-46681-0_47","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"call_identifier":"FP7","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","grant_number":"618091"},{"call_identifier":"FP7","name":"Limits to selection in biology and in evolutionary computation","_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152"},{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}]}]