[{"scopus_import":1,"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"date_updated":"2021-01-12T06:51:28Z","date_created":"2018-12-11T11:52:36Z","year":"2015","quality_controlled":"1","file":[{"file_size":605355,"creator":"system","relation":"main_file","checksum":"838657118ae286463a2b7737319f35ce","content_type":"application/pdf","date_created":"2018-12-12T10:07:43Z","file_id":"4641","access_level":"open_access","date_updated":"2020-07-14T12:45:01Z","file_name":"IST-2016-593-v1+1_Minimal_moment_equations.pdf"}],"volume":143,"date_published":"2015-12-22T00:00:00Z","oa_version":"Published Version","author":[{"id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282","full_name":"Ruess, Jakob","first_name":"Jakob","last_name":"Ruess"}],"ddc":["000"],"publist_id":"5632","issue":"24","publication":"Journal of Chemical Physics","publisher":"American Institute of Physics","doi":"10.1063/1.4937937","type":"journal_article","file_date_updated":"2020-07-14T12:45:01Z","language":[{"iso":"eng"}],"has_accepted_license":"1","day":"22","intvolume":"       143","citation":{"short":"J. Ruess, Journal of Chemical Physics 143 (2015).","ama":"Ruess J. Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. <i>Journal of Chemical Physics</i>. 2015;143(24). doi:<a href=\"https://doi.org/10.1063/1.4937937\">10.1063/1.4937937</a>","chicago":"Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical Reaction Networks with Partially Finite State Space.” <i>Journal of Chemical Physics</i>. American Institute of Physics, 2015. <a href=\"https://doi.org/10.1063/1.4937937\">https://doi.org/10.1063/1.4937937</a>.","ista":"Ruess J. 2015. Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. Journal of Chemical Physics. 143(24), 244103.","apa":"Ruess, J. (2015). Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. <i>Journal of Chemical Physics</i>. American Institute of Physics. <a href=\"https://doi.org/10.1063/1.4937937\">https://doi.org/10.1063/1.4937937</a>","ieee":"J. Ruess, “Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space,” <i>Journal of Chemical Physics</i>, vol. 143, no. 24. American Institute of Physics, 2015.","mla":"Ruess, Jakob. “Minimal Moment Equations for Stochastic Models of Biochemical Reaction Networks with Partially Finite State Space.” <i>Journal of Chemical Physics</i>, vol. 143, no. 24, 244103, American Institute of Physics, 2015, doi:<a href=\"https://doi.org/10.1063/1.4937937\">10.1063/1.4937937</a>."},"ec_funded":1,"abstract":[{"lang":"eng","text":"Many stochastic models of biochemical reaction networks contain some chemical species for which the number of molecules that are present in the system can only be finite (for instance due to conservation laws), but also other species that can be present in arbitrarily large amounts. The prime example of such networks are models of gene expression, which typically contain a small and finite number of possible states for the promoter but an infinite number of possible states for the amount of mRNA and protein. One of the main approaches to analyze such models is through the use of equations for the time evolution of moments of the chemical species. Recently, a new approach based on conditional moments of the species with infinite state space given all the different possible states of the finite species has been proposed. It was argued that this approach allows one to capture more details about the full underlying probability distribution with a smaller number of equations. Here, I show that the result that less moments provide more information can only stem from an unnecessarily complicated description of the system in the classical formulation. The foundation of this argument will be the derivation of moment equations that describe the complete probability distribution over the finite state space but only low-order moments over the infinite state space. I will show that the number of equations that is needed is always less than what was previously claimed and always less than the number of conditional moment equations up to the same order. To support these arguments, a symbolic algorithm is provided that can be used to derive minimal systems of unconditional moment equations for models with partially finite state space. "}],"status":"public","article_number":"244103","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"pubrep_id":"593","_id":"1539","month":"12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","title":"Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space","oa":1},{"ec_funded":1,"abstract":[{"lang":"eng","text":"We present XSpeed a parallel state-space exploration algorithm for continuous systems with linear dynamics and nondeterministic inputs. The motivation of having parallel algorithms is to exploit the computational power of multi-core processors to speed-up performance. The parallelization is achieved on two fronts. First, we propose a parallel implementation of the support function algorithm by sampling functions in parallel. Second, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input. A GP-GPU implementation is also presented following a lazy evaluation strategy on support functions. The parallel algorithms are implemented in the tool XSpeed. We evaluated the performance on two benchmarks including an 28 dimension Helicopter model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experiments illustrate that our parallel algorithm with time slicing not only speeds-up performance but also improves precision."}],"status":"public","day":"28","citation":{"chicago":"Ray, Rajarshi, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov, and Radu Grosu. “XSpeed: Accelerating Reachability Analysis on Multi-Core Processors.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">https://doi.org/10.1007/978-3-319-26287-1_1</a>.","ista":"Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. 2015. XSpeed: Accelerating reachability analysis on multi-core processors. 9434, 3–18.","apa":"Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., &#38; Grosu, R. (2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">https://doi.org/10.1007/978-3-319-26287-1_1</a>","ieee":"R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, and R. Grosu, “XSpeed: Accelerating reachability analysis on multi-core processors,” vol. 9434. Springer, pp. 3–18, 2015.","mla":"Ray, Rajarshi, et al. <i>XSpeed: Accelerating Reachability Analysis on Multi-Core Processors</i>. Vol. 9434, Springer, 2015, pp. 3–18, doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">10.1007/978-3-319-26287-1_1</a>.","short":"R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, R. Grosu, 9434 (2015) 3–18.","ama":"Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. XSpeed: Accelerating reachability analysis on multi-core processors. 2015;9434:3-18. doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_1\">10.1007/978-3-319-26287-1_1</a>"},"intvolume":"      9434","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"11","_id":"1541","title":"XSpeed: Accelerating reachability analysis on multi-core processors","publication_status":"published","department":[{"_id":"ToHe"}],"acknowledgement":"This work was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","alternative_title":["LNCS"],"date_updated":"2020-08-11T10:09:17Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"page":"3 - 18","quality_controlled":"1","date_created":"2018-12-11T11:52:37Z","series_title":"Lecture Notes in Computer Science","year":"2015","volume":9434,"scopus_import":1,"publisher":"Springer","doi":"10.1007/978-3-319-26287-1_1","type":"conference","language":[{"iso":"eng"}],"date_published":"2015-11-28T00:00:00Z","conference":{"start_date":"2015-11-17","name":"HVC: Haifa Verification Conference","end_date":"2015-11-19","location":"Haifa, Israel"},"oa_version":"None","author":[{"last_name":"Ray","first_name":"Rajarshi","full_name":"Ray, Rajarshi"},{"last_name":"Gurung","full_name":"Gurung, Amit","first_name":"Amit"},{"last_name":"Das","full_name":"Das, Binayak","first_name":"Binayak"},{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"last_name":"Grosu","full_name":"Grosu, Radu","first_name":"Radu"}],"publist_id":"5630"},{"type":"conference","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-662-48899-7_12","author":[{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"last_name":"Krčál","full_name":"Krčál, Jan","first_name":"Jan"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5577","date_published":"2015-11-22T00:00:00Z","conference":{"start_date":"2015-11-24","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","end_date":"2015-11-28","location":"Suva, Fiji"},"oa_version":"None","volume":9450,"project":[{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"date_updated":"2021-01-12T06:51:50Z","year":"2015","date_created":"2018-12-11T11:52:55Z","page":"162 - 177","quality_controlled":"1","scopus_import":1,"publication_status":"published","title":"Controller synthesis for MDPs and frequency LTL\\GU","_id":"1594","month":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"acknowledgement":"This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).\r\n","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"abstract":[{"text":"Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.","lang":"eng"}],"status":"public","ec_funded":1,"intvolume":"      9450","citation":{"ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>","short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.","ieee":"V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.","mla":"Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\\GU</i>. Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>.","ista":"Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450, 162–177.","apa":"Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>."},"day":"22"},{"date_updated":"2021-01-12T06:51:54Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"quality_controlled":"1","page":"479 - 486","year":"2015","date_created":"2018-12-11T11:52:57Z","volume":9206,"file":[{"file_name":"2015_CAV_Babiak.pdf","date_updated":"2020-07-14T12:45:04Z","access_level":"open_access","content_type":"application/pdf","date_created":"2020-05-15T08:38:12Z","file_id":"7850","checksum":"5885236fa88a439baba9ac6f3e801e93","relation":"main_file","creator":"dernst","file_size":1651779}],"article_processing_charge":"No","scopus_import":1,"publisher":"Springer","doi":"10.1007/978-3-319-21690-4_31","file_date_updated":"2020-07-14T12:45:04Z","type":"conference","language":[{"iso":"eng"}],"date_published":"2015-07-16T00:00:00Z","oa_version":"Submitted Version","conference":{"start_date":"2015-07-18","name":"CAV: Computer Aided Verification","end_date":"2015-07-24","location":"San Francisco, CA, United States"},"ddc":["000"],"author":[{"first_name":"Tomáš","full_name":"Babiak, Tomáš","last_name":"Babiak"},{"last_name":"Blahoudek","first_name":"František","full_name":"Blahoudek, František"},{"last_name":"Duret Lutz","full_name":"Duret Lutz, Alexandre","first_name":"Alexandre"},{"last_name":"Klein","first_name":"Joachim","full_name":"Klein, Joachim"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"full_name":"Mueller, Daniel","first_name":"Daniel","last_name":"Mueller"},{"last_name":"Parker","first_name":"David","full_name":"Parker, David"},{"full_name":"Strejček, Jan","first_name":"Jan","last_name":"Strejček"}],"publist_id":"5566","ec_funded":1,"abstract":[{"text":"We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.","lang":"eng"}],"status":"public","has_accepted_license":"1","day":"16","citation":{"ieee":"T. Babiak <i>et al.</i>, “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.","mla":"Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer, 2015, pp. 479–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>.","chicago":"Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein, Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata Format,” 9206:479–86. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>.","apa":"Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>","ista":"Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification, LNCS, vol. 9206, 479–486.","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>","short":"T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486."},"intvolume":"      9206","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07","_id":"1601","title":"The Hanoi omega-automata format","oa":1,"publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"alternative_title":["LNCS"]},{"acknowledgement":"This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734.","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"alternative_title":["LNCS"],"month":"07","_id":"1603","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","related_material":{"record":[{"id":"5549","relation":"research_paper","status":"public"}]},"title":"Counterexample explanation by learning small strategies in Markov decision processes","oa":1,"day":"16","citation":{"ama":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.","mla":"Brázdil, Tomáš, et al. <i>Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Vol. 9206, Springer, 2015, pp. 158–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>.","ista":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &#38; Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>"},"intvolume":"      9206","ec_funded":1,"status":"public","abstract":[{"lang":"eng","text":"For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour."}],"conference":{"end_date":"2015-07-24","location":"San Francisco, CA, United States","start_date":"2015-07-18","name":"CAV: Computer Aided Verification"},"oa_version":"Preprint","date_published":"2015-07-16T00:00:00Z","publist_id":"5564","author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","full_name":"Fellner, Andreas","last_name":"Fellner","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"}],"doi":"10.1007/978-3-319-21690-4_10","publisher":"Springer","language":[{"iso":"eng"}],"type":"conference","publication_identifier":{"eisbn":["978-3-319-21690-4"]},"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.02834"}],"scopus_import":1,"date_created":"2018-12-11T11:52:58Z","year":"2015","quality_controlled":"1","page":"158 - 177","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"date_updated":"2024-02-21T13:52:07Z","volume":9206},{"type":"conference","file_date_updated":"2020-07-14T12:45:05Z","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-319-26287-1_2","author":[{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov"},{"first_name":"Christian","full_name":"Schilling, Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"first_name":"Grégory","full_name":"Batt, Grégory","last_name":"Batt"},{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","last_name":"Kong","first_name":"Hui","full_name":"Kong, Hui"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"}],"ddc":["000"],"publist_id":"5561","date_published":"2015-11-28T00:00:00Z","oa_version":"Submitted Version","conference":{"location":"Haifa, Israel","end_date":"2015-11-19","name":"HVC: Haifa Verification Conference","start_date":"2015-11-17"},"file":[{"access_level":"open_access","date_updated":"2020-07-14T12:45:05Z","date_created":"2020-05-15T08:43:19Z","content_type":"application/pdf","file_id":"7851","file_name":"2015_LNCS_Bogomolov.pdf","creator":"dernst","file_size":1053207,"checksum":"3aab260f3f34641d622030ba22645b3e","relation":"main_file"}],"volume":9434,"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"date_updated":"2021-01-12T06:51:56Z","year":"2015","date_created":"2018-12-11T11:52:59Z","page":"19 - 35","quality_controlled":"1","scopus_import":1,"article_processing_charge":"No","publication_status":"published","title":"Abstraction-based parameter synthesis for multiaffine systems","oa":1,"_id":"1605","month":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"acknowledgement":"This work was partly supported by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/).","abstract":[{"lang":"eng","text":"Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model."}],"status":"public","ec_funded":1,"intvolume":"      9434","citation":{"short":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:, Springer, 2015, pp. 19–35.","ama":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35. doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>","ista":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference, LNCS, vol. 9434, 19–35.","chicago":"Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,” 9434:19–35. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>.","apa":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., &#38; Grosu, R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol. 9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>","mla":"Bogomolov, Sergiy, et al. <i>Abstraction-Based Parameter Synthesis for Multiaffine Systems</i>. Vol. 9434, Springer, 2015, pp. 19–35, doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>.","ieee":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu, “Abstraction-based parameter synthesis for multiaffine systems,” presented at the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35."},"has_accepted_license":"1","day":"28"},{"alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"title":"Runtime verification for hybrid analysis tools","publication_status":"published","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","month":"11","_id":"1606","citation":{"short":"L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, in:, 6th International Conference, Springer Nature, 2015, pp. 281–286.","ama":"Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid analysis tools. In: <i>6th International Conference</i>. Vol 9333. Springer Nature; 2015:281-286. doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>","ista":"Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Runtime verification for hybrid analysis tools. 6th International Conference. RV: Runtime Verification, LNCS, vol. 9333, 281–286.","chicago":"Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson. “Runtime Verification for Hybrid Analysis Tools.” In <i>6th International Conference</i>, 9333:281–86. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>.","apa":"Nguyen, L., Schilling, C., Bogomolov, S., &#38; Johnson, T. (2015). Runtime verification for hybrid analysis tools. In <i>6th International Conference</i> (Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>","ieee":"L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, “Runtime verification for hybrid analysis tools,” in <i>6th International Conference</i>, Vienna, Austria, 2015, vol. 9333, pp. 281–286.","mla":"Nguyen, Luan, et al. “Runtime Verification for Hybrid Analysis Tools.” <i>6th International Conference</i>, vol. 9333, Springer Nature, 2015, pp. 281–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>."},"intvolume":"      9333","day":"15","status":"public","abstract":[{"text":"In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.","lang":"eng"}],"ec_funded":1,"publist_id":"5562","publication":"6th International Conference","author":[{"first_name":"Luan","full_name":"Nguyen, Luan","last_name":"Nguyen"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"last_name":"Johnson","full_name":"Johnson, Taylor","first_name":"Taylor"}],"conference":{"name":"RV: Runtime Verification","start_date":"2015-09-22","location":"Vienna, Austria","end_date":"2015-09-25"},"oa_version":"None","date_published":"2015-11-15T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","doi":"10.1007/978-3-319-23820-3_19","publisher":"Springer Nature","publication_identifier":{"isbn":["978-3-319-23819-7"]},"scopus_import":"1","article_processing_charge":"No","volume":9333,"page":"281 - 286","quality_controlled":"1","year":"2015","date_created":"2018-12-11T11:52:59Z","date_updated":"2022-02-01T14:52:59Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}]},{"volume":9135,"quality_controlled":"1","page":"121 - 133","date_created":"2018-12-11T11:53:01Z","year":"2015","date_updated":"2023-02-23T12:26:24Z","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"publication_identifier":{"isbn":["978-3-662-47665-9"]},"scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/1504.08259","open_access":"1"}],"article_processing_charge":"No","arxiv":1,"language":[{"iso":"eng"}],"type":"conference","doi":"10.1007/978-3-662-47666-6_10","publisher":"Springer Nature","publication":"42nd International Colloquium","publist_id":"5556","issue":"Part II","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"conference":{"start_date":"2015-07-06","name":"ICALP: Automata, Languages and Programming","end_date":"2015-07-10","location":"Kyoto, Japan"},"external_id":{"arxiv":["1504.08259"]},"oa_version":"None","date_published":"2015-07-01T00:00:00Z","status":"public","abstract":[{"lang":"eng","text":"The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k."}],"ec_funded":1,"citation":{"ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd International Colloquium</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 121–133.","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>"},"intvolume":"      9135","day":"01","title":"Edit distance for pushdown automata","related_material":{"record":[{"id":"465","status":"public","relation":"later_version"},{"id":"5438","status":"public","relation":"earlier_version"}]},"oa":1,"publication_status":"published","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"1610","month":"07","alternative_title":["LNCS"],"pubrep_id":"321","department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.\r\nA Technical Report of the paper is available at: \r\nhttps://repository.ist.ac.at/331/\r\n","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"related_material":{"record":[{"id":"467","relation":"later_version","status":"public"},{"id":"5415","relation":"earlier_version","status":"public"},{"relation":"earlier_version","status":"public","id":"5436"}]},"title":"Nested weighted automata","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07","_id":"1656","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174926.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). Nested weighted automata. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174926, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>."},"day":"31","article_number":"7174926","status":"public","abstract":[{"text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.","lang":"eng"}],"ec_funded":1,"publication":"Proceedings - Symposium on Logic in Computer Science","publist_id":"5494","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"}],"conference":{"start_date":"2015-07-06","name":"LICS: Logic in Computer Science","end_date":"2015-07-10","location":"Kyoto, Japan"},"external_id":{"arxiv":["1606.03598"]},"oa_version":"None","date_published":"2015-07-31T00:00:00Z","arxiv":1,"language":[{"iso":"eng"}],"type":"conference","doi":"10.1109/LICS.2015.72","publisher":"IEEE","scopus_import":1,"volume":"2015-July","quality_controlled":"1","date_created":"2018-12-11T11:53:17Z","year":"2015","date_updated":"2023-02-23T12:26:19Z","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1657","month":"07","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","related_material":{"record":[{"id":"466","status":"public","relation":"later_version"},{"id":"5429","relation":"earlier_version","status":"public"},{"id":"5435","relation":"earlier_version","status":"public"}]},"publication_status":"published","acknowledgement":"A Technical Report of this paper is available at:  https://repository.ist.ac.at/327\r\n","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"alternative_title":["LICS"],"ec_funded":1,"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"status":"public","day":"01","citation":{"short":"K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.","ama":"Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>","apa":"Chatterjee, K., Komárková, Z., &#38; Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>","ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.","chicago":"Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>.","ieee":"K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.","mla":"Chatterjee, Krishnendu, et al. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IEEE, 2015, pp. 244–56, doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>."},"publisher":"IEEE","doi":"10.1109/LICS.2015.32","type":"conference","language":[{"iso":"eng"}],"date_published":"2015-07-01T00:00:00Z","conference":{"start_date":"2015-07-06","name":"LICS: Logic in Computer Science","end_date":"2015-07-10","location":"Kyoto, Japan"},"oa_version":"None","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Komárková, Zuzana","first_name":"Zuzana","last_name":"Komárková"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5493","date_updated":"2023-02-23T12:26:16Z","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7"}],"page":"244 - 256","quality_controlled":"1","series_title":"LICS","year":"2015","date_created":"2018-12-11T11:53:18Z","scopus_import":1},{"type":"conference","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-319-23401-4_8","author":[{"first_name":"Sergiy","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Andreas","full_name":"Podelski, Andreas","last_name":"Podelski"},{"orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","last_name":"Ruess","full_name":"Ruess, Jakob","first_name":"Jakob"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"}],"publist_id":"5492","date_published":"2015-09-01T00:00:00Z","oa_version":"None","conference":{"name":"CMSB: Computational Methods in Systems Biology","start_date":"2015-09-16","location":"Nantes, France","end_date":"2015-09-18"},"volume":9308,"date_updated":"2023-02-21T16:17:24Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"page":"77 - 89","quality_controlled":"1","date_created":"2018-12-11T11:53:18Z","year":"2015","series_title":"Lecture Notes in Computer Science","scopus_import":1,"title":"Adaptive moment closure for parameter inference of biochemical reaction networks","related_material":{"record":[{"id":"1148","status":"public","relation":"later_version"}]},"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1658","month":"09","alternative_title":["LNCS"],"department":[{"_id":"ToHe"},{"_id":"GaTk"}],"abstract":[{"lang":"eng","text":"Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space."}],"status":"public","ec_funded":1,"citation":{"mla":"Bogomolov, Sergiy, et al. <i>Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks</i>. Vol. 9308, Springer, 2015, pp. 77–89, doi:<a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">10.1007/978-3-319-23401-4_8</a>.","ieee":"S. Bogomolov, T. A. Henzinger, A. Podelski, J. Ruess, and C. Schilling, “Adaptive moment closure for parameter inference of biochemical reaction networks,” vol. 9308. Springer, pp. 77–89, 2015.","apa":"Bogomolov, S., Henzinger, T. A., Podelski, A., Ruess, J., &#38; Schilling, C. (2015). Adaptive moment closure for parameter inference of biochemical reaction networks. Presented at the CMSB: Computational Methods in Systems Biology, Nantes, France: Springer. <a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">https://doi.org/10.1007/978-3-319-23401-4_8</a>","chicago":"Bogomolov, Sergiy, Thomas A Henzinger, Andreas Podelski, Jakob Ruess, and Christian Schilling. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">https://doi.org/10.1007/978-3-319-23401-4_8</a>.","ista":"Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. 2015. Adaptive moment closure for parameter inference of biochemical reaction networks. 9308, 77–89.","ama":"Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. Adaptive moment closure for parameter inference of biochemical reaction networks. 2015;9308:77-89. doi:<a href=\"https://doi.org/10.1007/978-3-319-23401-4_8\">10.1007/978-3-319-23401-4_8</a>","short":"S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, C. Schilling, 9308 (2015) 77–89."},"intvolume":"      9308","day":"01"},{"ec_funded":1,"status":"public","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."}],"day":"01","has_accepted_license":"1","citation":{"short":"U. Boker, T.A. Henzinger, J. Otop, in:, LICS, IEEE, 2015, pp. 750–761.","ama":"Boker U, Henzinger TA, Otop J. The target discounted-sum problem. In: <i>LICS</i>. Logic in Computer Science. IEEE; 2015:750-761. doi:<a href=\"https://doi.org/10.1109/LICS.2015.74\">10.1109/LICS.2015.74</a>","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>.","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>","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem. LICS. LICS: Logic in Computer ScienceLogic in Computer Science, 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>.","ieee":"U. Boker, T. A. Henzinger, and J. Otop, “The target discounted-sum problem,” in <i>LICS</i>, Kyoto, Japan, 2015, pp. 750–761."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07","_id":"1659","related_material":{"record":[{"id":"5439","status":"public","relation":"earlier_version"}]},"title":"The target discounted-sum problem","oa":1,"publication_status":"published","acknowledgement":"A technical report of the article is available at: https://research-explorer.app.ist.ac.at/record/5439","department":[{"_id":"ToHe"}],"quality_controlled":"1","page":"750 - 761","year":"2015","date_created":"2018-12-11T11:53:19Z","series_title":"Logic in Computer Science","date_updated":"2023-02-23T12:26:27Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"file":[{"creator":"dernst","file_size":340215,"checksum":"6abebca9c1a620e9e103a8f9222befac","relation":"main_file","date_updated":"2020-07-14T12:45:10Z","access_level":"open_access","file_id":"7852","date_created":"2020-05-15T08:53:29Z","content_type":"application/pdf","file_name":"2015_LICS_Boker.pdf"}],"article_processing_charge":"No","publication_identifier":{"eisbn":["978-1-4799-8875-4 "],"issn":["1043-6871 "]},"scopus_import":1,"doi":"10.1109/LICS.2015.74","publisher":"IEEE","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:45:10Z","type":"conference","oa_version":"Submitted Version","conference":{"location":"Kyoto, Japan","end_date":"2015-07-10","name":"LICS: Logic in Computer Science","start_date":"2015-007-06"},"date_published":"2015-07-01T00:00:00Z","publication":"LICS","publist_id":"5491","ddc":["000"],"author":[{"first_name":"Udi","full_name":"Boker, Udi","last_name":"Boker","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}]},{"author":[{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov"},{"full_name":"Magazzeni, Daniele","first_name":"Daniele","last_name":"Magazzeni"},{"last_name":"Minopoli","full_name":"Minopoli, Stefano","first_name":"Stefano"},{"last_name":"Wehrle","first_name":"Martin","full_name":"Wehrle, Martin"}],"publist_id":"5479","date_published":"2015-06-01T00:00:00Z","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)”.","department":[{"_id":"ToHe"}],"conference":{"start_date":"2015-06-07","name":"ICAPS: International Conference on Automated Planning and Scheduling","end_date":"2015-06-11","location":"Jerusalem, Israel"},"oa_version":"None","type":"conference","title":"PDDL+ planning with hybrid automata: Foundations of translating must behavior","language":[{"iso":"eng"}],"publication_status":"published","publisher":"AAAI Press","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1670","month":"06","scopus_import":1,"main_file_link":[{"url":"https://www.aaai.org/ocs/index.php/ICAPS/ICAPS15/paper/view/10606/10394"}],"citation":{"short":"S. Bogomolov, D. Magazzeni, S. Minopoli, M. Wehrle, in:, AAAI Press, 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.","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.","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.","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.","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.","mla":"Bogomolov, Sergiy, et al. <i>PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior</i>. AAAI Press, 2015, pp. 42–46."},"day":"01","abstract":[{"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.","lang":"eng"}],"status":"public","date_updated":"2021-01-12T06:52:25Z","ec_funded":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"quality_controlled":"1","page":"42 - 46","year":"2015","date_created":"2018-12-11T11:53:23Z"},{"date_updated":"2021-01-12T06:52:29Z","ec_funded":1,"project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","date_created":"2018-12-11T11:53:26Z","year":"2015","abstract":[{"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.","lang":"eng"}],"volume":17,"article_number":"2","status":"public","day":"01","intvolume":"        17","citation":{"ista":"Michaliszyn J, Otop J, Kieroňski E. 2015. On the decidability of elementary modal logics. ACM Transactions on Computational Logic. 17(1), 2.","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>","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>.","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>.","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.","short":"J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational Logic 17 (2015).","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>"},"publisher":"ACM","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1680","month":"09","doi":"10.1145/2817825","type":"journal_article","title":"On the decidability of elementary modal logics","publication_status":"published","language":[{"iso":"eng"}],"date_published":"2015-09-01T00:00:00Z","department":[{"_id":"ToHe"}],"oa_version":"None","author":[{"last_name":"Michaliszyn","full_name":"Michaliszyn, Jakub","first_name":"Jakub"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kieroňski","first_name":"Emanuel","full_name":"Kieroňski, Emanuel"}],"publist_id":"5468","issue":"1","publication":"ACM Transactions on Computational Logic"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_published":"2015-04-14T00:00:00Z","conference":{"end_date":"2015-04-16","location":"Seattle, WA, United States","start_date":"2015-04-14","name":"HSCC: Hybrid Systems - Computation and Control"},"oa_version":"Preprint","author":[{"full_name":"Svoreňová, Mária","first_name":"Mária","last_name":"Svoreňová"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Cěrná","first_name":"Ivana","full_name":"Cěrná, Ivana"},{"first_name":"Cǎlin","full_name":"Belta, Cǎlin","last_name":"Belta"}],"publist_id":"5456","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","publisher":"ACM","_id":"1689","month":"04","doi":"10.1145/2728606.2728608","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","publication_status":"published","language":[{"iso":"eng"}],"oa":1,"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","related_material":{"record":[{"relation":"later_version","status":"public","id":"1407"}]},"day":"14","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"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.","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>","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.","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>","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."},"scopus_import":1,"project":[{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2023-09-20T09:43:09Z","ec_funded":1,"date_created":"2018-12-11T11:53:29Z","year":"2015","page":"259 - 268","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."}],"status":"public"},{"year":"2015","date_created":"2018-12-11T11:53:29Z","quality_controlled":"1","page":"128 - 133","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"date_updated":"2021-01-12T06:52:33Z","ec_funded":1,"status":"public","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."}],"day":"14","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>","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>.","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.","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>","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>."},"doi":"10.1145/2728606.2728630","_id":"1690","month":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","language":[{"iso":"eng"}],"publication_status":"published","title":"HYST: A source transformation and translation tool for hybrid automaton models","type":"conference","conference":{"end_date":"2015-04-16","location":"Seattle, WA, United States","start_date":"2015-04-14","name":"HSCC: Hybrid Systems - Computation and Control"},"oa_version":"None","department":[{"_id":"ToHe"}],"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).","date_published":"2015-04-14T00:00:00Z","publist_id":"5454","author":[{"first_name":"Stanley","full_name":"Bak, Stanley","last_name":"Bak"},{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"last_name":"Johnson","full_name":"Johnson, Taylor","first_name":"Taylor"}]},{"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2021-01-12T06:52:33Z","ec_funded":1,"date_created":"2018-12-11T11:53:30Z","year":"2015","quality_controlled":"1","page":"149 - 158","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"}],"status":"public","day":"14","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>.","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.","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.","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>.","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>","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."},"scopus_import":1,"publication_identifier":{"isbn":["978-1-4503-3433-4"]},"publisher":"ACM","month":"04","_id":"1692","doi":"10.1145/2728606.2728622","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","language":[{"iso":"eng"}],"publication_status":"published","title":"Eliminating spurious transitions in reachability with support functions","department":[{"_id":"ToHe"}],"date_published":"2015-04-14T00:00:00Z","oa_version":"None","conference":{"end_date":"2015-04-16","location":"Seattle, WA, United States","start_date":"2015-04-14","name":"HSCC: Hybrid Systems - Computation and Control"},"author":[{"last_name":"Frehse","full_name":"Frehse, Goran","first_name":"Goran"},{"full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Greitschus","first_name":"Marius","full_name":"Greitschus, Marius"},{"first_name":"Thomas","full_name":"Strump, Thomas","last_name":"Strump"},{"first_name":"Andreas","full_name":"Podelski, Andreas","last_name":"Podelski"}],"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","publist_id":"5452"},{"publisher":"Elsevier","doi":"10.1016/j.ic.2015.03.001","type":"journal_article","language":[{"iso":"eng"}],"date_published":"2015-04-01T00:00:00Z","oa_version":"Preprint","author":[{"first_name":"Yaron","full_name":"Velner, Yaron","last_name":"Velner"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Rabinovich","first_name":"Alexander","full_name":"Rabinovich, Alexander"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"}],"publist_id":"5443","issue":"4","publication":"Information and Computation","date_updated":"2021-01-12T06:52:36Z","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"page":"177 - 196","quality_controlled":"1","date_created":"2018-12-11T11:53:32Z","year":"2015","volume":241,"scopus_import":1,"main_file_link":[{"url":"http://arxiv.org/abs/1209.3234","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1698","month":"04","title":"The complexity of multi-mean-payoff and multi-energy games","oa":1,"publication_status":"published","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).","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ec_funded":1,"abstract":[{"lang":"eng","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."}],"status":"public","day":"01","intvolume":"       241","citation":{"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>","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>.","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.","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>","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.","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>."}},{"author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol"},{"last_name":"Clarke","first_name":"Edmund","full_name":"Clarke, Edmund"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid","first_name":"Leonid"},{"full_name":"Samanta, Roopsha","first_name":"Roopsha","last_name":"Samanta","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach","first_name":"Thorsten","full_name":"Tarrach, Thorsten"}],"ddc":["000"],"publist_id":"5398","date_published":"2015-07-01T00:00:00Z","conference":{"start_date":"2015-07-18","name":"CAV: Computer Aided Verification","end_date":"2015-07-24","location":"San Francisco, CA, United States"},"oa_version":"Submitted Version","type":"conference","file_date_updated":"2020-07-14T12:45:13Z","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-319-21668-3_11","scopus_import":1,"file":[{"checksum":"6ff58ac220e2f20cb001ba35d4924495","relation":"main_file","creator":"system","file_size":481922,"file_name":"IST-2015-336-v1+1_long_version.pdf","access_level":"local","date_updated":"2020-07-14T12:45:13Z","file_id":"4715","date_created":"2018-12-12T10:08:53Z","content_type":"application/pdf"}],"volume":9207,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2023-09-20T11:13:50Z","series_title":"Lecture Notes in Computer Science","date_created":"2018-12-11T11:53:42Z","year":"2015","page":"180 - 197","quality_controlled":"1","alternative_title":["LNCS"],"pubrep_id":"336","department":[{"_id":"ToHe"}],"publication_status":"published","title":"From non-preemptive to preemptive scheduling using synchronization synthesis","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1130"},{"id":"1338","relation":"later_version","status":"public"}]},"month":"07","_id":"1729","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"      9207","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>","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>.","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."},"has_accepted_license":"1","day":"01","abstract":[{"lang":"eng","text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of 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."}],"status":"public","ec_funded":1},{"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"last_name":"Gimbert","first_name":"Hugo","full_name":"Gimbert, Hugo"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5395","issue":"12","publication":"Information and Computation","date_published":"2015-12-01T00:00:00Z","oa_version":"Preprint","type":"journal_article","language":[{"iso":"eng"}],"publisher":"Elsevier","doi":"10.1016/j.ic.2015.06.003","main_file_link":[{"url":"http://arxiv.org/abs/1006.0673","open_access":"1"}],"scopus_import":1,"volume":245,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"},{"grant_number":"214373","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_updated":"2023-02-23T11:45:42Z","date_created":"2018-12-11T11:53:42Z","year":"2015","page":"3 - 16","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","oa":1,"related_material":{"record":[{"id":"3856","relation":"earlier_version","status":"public"}]},"title":"Randomness for free","_id":"1731","month":"12","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"short":"K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation 245 (2015) 3–16.","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>","ista":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free. Information and Computation. 245(12), 3–16.","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>.","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>","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>.","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."},"intvolume":"       245","day":"01","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"}],"status":"public","ec_funded":1}]