[{"quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","publisher":"AAAI Press","publication_status":"published","main_file_link":[{"url":"https://www.aaai.org/ocs/index.php/ICAPS/ICAPS15/paper/view/10606/10394"}],"month":"06","_id":"1670","date_published":"2015-06-01T00:00:00Z","abstract":[{"lang":"eng","text":"Planning in hybrid domains poses a special challenge due to the involved mixed discrete-continuous dynamics. A recent solving approach for such domains is based on applying model checking techniques on a translation of PDDL+ planning problems to hybrid automata. However, the proposed translation is limited because must behavior is only overapproximated, and hence, processes and events are not reflected exactly. In this paper, we present the theoretical foundation of an exact PDDL+ translation. We propose a schema to convert a hybrid automaton with must transitions into an equivalent hybrid automaton featuring only may transitions."}],"date_created":"2018-12-11T11:53:23Z","page":"42 - 46","language":[{"iso":"eng"}],"date_updated":"2021-01-12T06:52:25Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"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)”.","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"day":"01","publist_id":"5479","year":"2015","oa_version":"None","author":[{"full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Magazzeni, Daniele","first_name":"Daniele","last_name":"Magazzeni"},{"full_name":"Minopoli, Stefano","first_name":"Stefano","last_name":"Minopoli"},{"last_name":"Wehrle","first_name":"Martin","full_name":"Wehrle, Martin"}],"type":"conference","ec_funded":1,"citation":{"short":"S. Bogomolov, D. Magazzeni, S. Minopoli, M. Wehrle, in:, AAAI Press, 2015, pp. 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.","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.","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.","ista":"Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. 2015. PDDL+ planning with hybrid automata: Foundations of translating must behavior. ICAPS: International Conference on Automated Planning and Scheduling, 42–46.","chicago":"Bogomolov, Sergiy, Daniele Magazzeni, Stefano Minopoli, and Martin Wehrle. “PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior,” 42–46. AAAI Press, 2015.","mla":"Bogomolov, Sergiy, et al. <i>PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior</i>. AAAI Press, 2015, pp. 42–46."},"conference":{"location":"Jerusalem, Israel","start_date":"2015-06-07","end_date":"2015-06-11","name":"ICAPS: International Conference on Automated Planning and Scheduling"},"title":"PDDL+ planning with hybrid automata: Foundations of translating must behavior"},{"publisher":"ACM","publication_status":"published","quality_controlled":"1","department":[{"_id":"ToHe"}],"publication":"ACM Transactions on Computational Logic","volume":17,"intvolume":"        17","status":"public","issue":"1","article_number":"2","month":"09","_id":"1680","date_published":"2015-09-01T00:00:00Z","date_created":"2018-12-11T11:53:26Z","abstract":[{"lang":"eng","text":"We consider the satisfiability problem for modal logic over first-order definable classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008] that modal logic is decidable over classes definable by universal Horn formulae. We provide a full classification of Horn formulae with respect to the complexity of the corresponding satisfiability problem. It turns out, that except for the trivial case of inconsistent formulae, local satisfiability is eitherNP-complete or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete, or ExpTime-complete. We also show that the finite satisfiability problem for modal logic over Horn definable classes of frames is decidable. On the negative side, we show undecidability of two related problems. First, we exhibit a simple universal three-variable formula defining the class of frames over which modal logic is undecidable. Second, we consider the satisfiability problem of bimodal logic over Horn definable classes of frames, and also present a formula leading to undecidability."}],"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:52:29Z","doi":"10.1145/2817825","ec_funded":1,"citation":{"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>","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>","short":"J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational Logic 17 (2015).","mla":"Michaliszyn, Jakub, et al. “On the Decidability of Elementary Modal Logics.” <i>ACM Transactions on Computational Logic</i>, vol. 17, no. 1, 2, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2817825\">10.1145/2817825</a>.","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>.","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.","ista":"Michaliszyn J, Otop J, Kieroňski E. 2015. On the decidability of elementary modal logics. ACM Transactions on Computational Logic. 17(1), 2."},"title":"On the decidability of elementary modal logics","day":"01","publist_id":"5468","oa_version":"None","year":"2015","type":"journal_article","author":[{"full_name":"Michaliszyn, Jakub","first_name":"Jakub","last_name":"Michaliszyn"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"},{"full_name":"Kieroňski, Emanuel","first_name":"Emanuel","last_name":"Kieroňski"}]},{"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"oa":1,"publication_status":"published","publisher":"ACM","status":"public","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"page":"259 - 268","_id":"1689","date_published":"2015-04-14T00:00:00Z","abstract":[{"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.","lang":"eng"}],"date_created":"2018-12-11T11:53:29Z","month":"04","related_material":{"record":[{"status":"public","id":"1407","relation":"later_version"}]},"project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","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"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"doi":"10.1145/2728606.2728608","scopus_import":1,"date_updated":"2023-09-20T09:43:09Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","conference":{"location":"Seattle, WA, United States","end_date":"2015-04-16","start_date":"2015-04-14","name":"HSCC: Hybrid Systems - Computation and Control"},"citation":{"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>.","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.","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.","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>.","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>","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>"},"ec_funded":1,"author":[{"last_name":"Svoreňová","full_name":"Svoreňová, Mária","first_name":"Mária"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik"},{"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"},{"last_name":"Belta","full_name":"Belta, Cǎlin","first_name":"Cǎlin"}],"type":"conference","year":"2015","oa_version":"Preprint","day":"14","publist_id":"5456"},{"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"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).","doi":"10.1145/2728606.2728630","date_updated":"2021-01-12T06:52:33Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"HYST: A source transformation and translation tool for hybrid automaton models","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","start_date":"2015-04-14","end_date":"2015-04-16","location":"Seattle, WA, United States"},"citation":{"short":"S. Bak, S. Bogomolov, T. Johnson, in:, Springer, 2015, pp. 128–133.","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>","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>","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>.","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.","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.","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>."},"ec_funded":1,"type":"conference","author":[{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"full_name":"Johnson, Taylor","first_name":"Taylor","last_name":"Johnson"}],"year":"2015","oa_version":"None","publist_id":"5454","day":"14","publisher":"Springer","publication_status":"published","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"}],"page":"128 - 133","date_created":"2018-12-11T11:53:29Z","_id":"1690","abstract":[{"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.","lang":"eng"}],"date_published":"2015-04-14T00:00:00Z","month":"04"},{"title":"Eliminating spurious transitions in reachability with support functions","conference":{"location":"Seattle, WA, United States","start_date":"2015-04-14","end_date":"2015-04-16","name":"HSCC: Hybrid Systems - Computation and Control"},"citation":{"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>.","ista":"Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. 2015. Eliminating spurious transitions in reachability with support functions. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 149–158.","ieee":"G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, and A. Podelski, “Eliminating spurious transitions in reachability with support functions,” in <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, Seattle, WA, United States, 2015, pp. 149–158.","mla":"Frehse, Goran, et al. “Eliminating Spurious Transitions in Reachability with Support Functions.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 149–58, doi:<a href=\"https://doi.org/10.1145/2728606.2728622\">10.1145/2728606.2728622</a>.","short":"G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, A. Podelski, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 149–158.","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>","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>"},"ec_funded":1,"author":[{"last_name":"Frehse","full_name":"Frehse, Goran","first_name":"Goran"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov"},{"last_name":"Greitschus","full_name":"Greitschus, Marius","first_name":"Marius"},{"first_name":"Thomas","full_name":"Strump, Thomas","last_name":"Strump"},{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski, Andreas"}],"type":"conference","oa_version":"None","year":"2015","day":"14","publist_id":"5452","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publication_identifier":{"isbn":["978-1-4503-3433-4"]},"doi":"10.1145/2728606.2728622","scopus_import":1,"date_updated":"2021-01-12T06:52:33Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"page":"149 - 158","date_published":"2015-04-14T00:00:00Z","_id":"1692","date_created":"2018-12-11T11:53:30Z","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"}],"month":"04","publication_status":"published","publisher":"ACM","status":"public","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","quality_controlled":"1","department":[{"_id":"ToHe"}]},{"year":"2015","oa_version":"Preprint","publist_id":"5443","scopus_import":1,"date_updated":"2021-01-12T06:52:36Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2015-04-01T00:00:00Z","_id":"1698","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."}],"issue":"4","volume":241,"main_file_link":[{"url":"http://arxiv.org/abs/1209.3234","open_access":"1"}],"oa":1,"publication_status":"published","author":[{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Rabinovich","first_name":"Alexander","full_name":"Rabinovich, Alexander"},{"last_name":"Raskin","first_name":"Jean","full_name":"Raskin, Jean"}],"type":"journal_article","day":"01","title":"The complexity of multi-mean-payoff and multi-energy games","citation":{"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>.","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>.","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.","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.","ama":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. 2015;241(4):177-196. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>","apa":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &#38; Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>","short":"Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196."},"ec_funded":1,"doi":"10.1016/j.ic.2015.03.001","language":[{"iso":"eng"}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"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":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"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).","date_created":"2018-12-11T11:53:32Z","month":"04","page":"177 - 196","intvolume":"       241","status":"public","publication":"Information and Computation","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Elsevier"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"1130","status":"public"},{"status":"public","id":"1338","relation":"later_version"}]},"doi":"10.1007/978-3-319-21668-3_11","ddc":["000"],"language":[{"iso":"eng"}],"title":"From non-preemptive to preemptive scheduling using synchronization synthesis","conference":{"start_date":"2015-07-18","end_date":"2015-07-24","name":"CAV: Computer Aided Verification","location":"San Francisco, CA, United States"},"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>","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>","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>.","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>.","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” vol. 9207. Springer, pp. 180–197, 2015.","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."},"ec_funded":1,"type":"conference","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","full_name":"Cerny, Pavol","first_name":"Pavol"},{"last_name":"Clarke","full_name":"Clarke, Edmund","first_name":"Edmund"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ryzhyk","first_name":"Leonid","full_name":"Ryzhyk, Leonid"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta","first_name":"Roopsha","full_name":"Samanta, Roopsha"},{"full_name":"Tarrach, Thorsten","first_name":"Thorsten","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487"}],"alternative_title":["LNCS"],"day":"01","publisher":"Springer","status":"public","intvolume":"      9207","department":[{"_id":"ToHe"}],"quality_controlled":"1","page":"180 - 197","series_title":"Lecture Notes in Computer Science","date_created":"2018-12-11T11:53:42Z","month":"07","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-20T11:13:50Z","oa_version":"Submitted Version","has_accepted_license":"1","year":"2015","publist_id":"5398","publication_status":"published","pubrep_id":"336","volume":9207,"file_date_updated":"2020-07-14T12:45:13Z","_id":"1729","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."}],"date_published":"2015-07-01T00:00:00Z","file":[{"checksum":"6ff58ac220e2f20cb001ba35d4924495","access_level":"local","date_updated":"2020-07-14T12:45:13Z","file_size":481922,"creator":"system","file_name":"IST-2015-336-v1+1_long_version.pdf","date_created":"2018-12-12T10:08:53Z","file_id":"4715","relation":"main_file","content_type":"application/pdf"}]},{"day":"01","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, 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"},{"full_name":"Gimbert, Hugo","first_name":"Hugo","last_name":"Gimbert"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"type":"journal_article","ec_funded":1,"citation":{"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>","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>","short":"K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation 245 (2015) 3–16.","mla":"Chatterjee, Krishnendu, et al. “Randomness for Free.” <i>Information and Computation</i>, vol. 245, no. 12, Elsevier, 2015, pp. 3–16, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.06.003\">10.1016/j.ic.2015.06.003</a>.","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>.","ista":"Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2015. Randomness for free. Information and Computation. 245(12), 3–16.","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."},"title":"Randomness for free","language":[{"iso":"eng"}],"doi":"10.1016/j.ic.2015.06.003","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_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"},{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"grant_number":"214373","name":"Design for Embedded Systems","_id":"25F1337C-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"}],"related_material":{"record":[{"id":"3856","relation":"earlier_version","status":"public"}]},"month":"12","date_created":"2018-12-11T11:53:42Z","page":"3 - 16","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","publication":"Information and Computation","status":"public","intvolume":"       245","publisher":"Elsevier","publist_id":"5395","oa_version":"Preprint","year":"2015","date_updated":"2023-02-23T11:45:42Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"_id":"1731","abstract":[{"lang":"eng","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. "}],"date_published":"2015-12-01T00:00:00Z","issue":"12","volume":245,"publication_status":"published","main_file_link":[{"url":"http://arxiv.org/abs/1006.0673","open_access":"1"}],"oa":1},{"issue":"2","month":"05","article_number":"7","_id":"1808","date_created":"2018-12-11T11:54:07Z","date_published":"2015-05-01T00:00:00Z","publisher":"ACM","publication_status":"published","publication":"ACM Transactions on Modeling and Computer Simulation","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","intvolume":"        25","volume":25,"citation":{"mla":"Gupta, Ashutosh, and Thomas A. Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 7, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>.","ista":"Gupta A, Henzinger TA. 2015. Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. 25(2), 7.","ieee":"A. Gupta and T. A. Henzinger, “Guest editors’ introduction to special issue on computational methods in systems biology,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","chicago":"Gupta, Ashutosh, and Thomas A Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>.","apa":"Gupta, A., &#38; Henzinger, T. A. (2015). Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>","ama":"Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>","short":"A. Gupta, T.A. Henzinger, ACM Transactions on Modeling and Computer Simulation 25 (2015)."},"title":"Guest editors' introduction to special issue on computational methods in systems biology","day":"01","publist_id":"5302","author":[{"first_name":"Ashutosh","full_name":"Gupta, Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"type":"journal_article","year":"2015","oa_version":"None","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"date_updated":"2021-01-12T06:53:20Z","doi":"10.1145/2745799"},{"tmp":{"name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","short":"CC BY-ND (4.0)"},"pubrep_id":"390","volume":11,"file_date_updated":"2020-07-14T12:45:17Z","oa":1,"license":"https://creativecommons.org/licenses/by-nd/4.0/","publication_status":"published","_id":"1832","abstract":[{"text":"Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. ","lang":"eng"}],"date_published":"2015-04-01T00:00:00Z","article_number":"20","file":[{"creator":"system","file_size":380203,"file_name":"IST-2015-390-v1+1_1502.07639.pdf","checksum":"7370e164d0a731f442424a92669efc34","access_level":"open_access","date_updated":"2020-07-14T12:45:17Z","file_id":"4881","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:11:27Z"}],"article_processing_charge":"No","issue":"1","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:38:13Z","has_accepted_license":"1","oa_version":"Published Version","year":"2015","article_type":"original","publist_id":"5271","status":"public","intvolume":"        11","publication":"Logical Methods in Computer Science","quality_controlled":"1","department":[{"_id":"ToHe"}],"publisher":"International Federation of Computational Logic","date_created":"2018-12-11T11:54:15Z","month":"04","doi":"10.2168/LMCS-11(1:20)2015","ddc":["000"],"language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"related_material":{"record":[{"relation":"earlier_version","id":"2328","status":"public"}]},"author":[{"first_name":"Soham","full_name":"Chakraborty, Soham","last_name":"Chakraborty"},{"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":"Ali","full_name":"Sezgin, Ali","last_name":"Sezgin"},{"first_name":"Viktor","full_name":"Vafeiadis, Viktor","last_name":"Vafeiadis"}],"type":"journal_article","day":"01","title":"Aspect-oriented linearizability proofs","citation":{"short":"S. Chakraborty, T.A. Henzinger, A. Sezgin, V. Vafeiadis, Logical Methods in Computer Science 11 (2015).","ama":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. <i>Logical Methods in Computer Science</i>. 2015;11(1). doi:<a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">10.2168/LMCS-11(1:20)2015</a>","apa":"Chakraborty, S., Henzinger, T. A., Sezgin, A., &#38; Vafeiadis, V. (2015). Aspect-oriented linearizability proofs. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">https://doi.org/10.2168/LMCS-11(1:20)2015</a>","chicago":"Chakraborty, Soham, Thomas A Henzinger, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2015. <a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">https://doi.org/10.2168/LMCS-11(1:20)2015</a>.","ieee":"S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” <i>Logical Methods in Computer Science</i>, vol. 11, no. 1. International Federation of Computational Logic, 2015.","ista":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 11(1), 20.","mla":"Chakraborty, Soham, et al. “Aspect-Oriented Linearizability Proofs.” <i>Logical Methods in Computer Science</i>, vol. 11, no. 1, 20, International Federation of Computational Logic, 2015, doi:<a href=\"https://doi.org/10.2168/LMCS-11(1:20)2015\">10.2168/LMCS-11(1:20)2015</a>."},"ec_funded":1},{"main_file_link":[{"url":"http://arxiv.org/abs/1410.7704","open_access":"1"}],"oa":1,"publication_status":"published","volume":9035,"_id":"1835","abstract":[{"lang":"eng","text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs –an important problem of interest in evolutionary biology– more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights."}],"date_published":"2015-04-01T00:00:00Z","date_updated":"2025-05-28T11:57:04Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"year":"2015","oa_version":"Preprint","publist_id":"5267","publisher":"Springer","status":"public","intvolume":"      9035","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"page":"469 - 483","series_title":"Lecture Notes in Computer Science","date_created":"2018-12-11T11:54:16Z","month":"04","acknowledgement":"SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2 148797.\r\n","related_material":{"record":[{"status":"public","id":"1351","relation":"later_version"}]},"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"618091","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"doi":"10.1007/978-3-662-46681-0_47","language":[{"iso":"eng"}],"conference":{"end_date":"2015-04-18","start_date":"2015-04-11","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"London, United Kingdom"},"title":"Model checking gene regulatory networks","ec_funded":1,"citation":{"mla":"Giacobbe, Mirco, et al. <i>Model Checking Gene Regulatory Networks</i>. Vol. 9035, Springer, 2015, pp. 469–83, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>.","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model checking gene regulatory networks. 9035, 469–483.","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking gene regulatory networks,” vol. 9035. Springer, pp. 469–483, 2015.","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking Gene Regulatory Networks.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2015). Model checking gene regulatory networks. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking gene regulatory networks. 2015;9035:469-483. doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483."},"alternative_title":["LNCS"],"type":"conference","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","first_name":"Mirco","full_name":"Giacobbe, Mirco","last_name":"Giacobbe"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-6220-2052","full_name":"Guet, Calin C","first_name":"Calin C","last_name":"Guet"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"orcid":"0000-0003-2361-3953","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","full_name":"Paixao, Tiago","first_name":"Tiago","last_name":"Paixao"},{"last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"day":"01"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2020-08-11T10:09:32Z","scopus_import":1,"oa_version":"None","year":"2015","publist_id":"5266","publication_status":"published","volume":9032,"abstract":[{"text":"In the standard framework for worst-case execution time (WCET) analysis of programs, the main data structure is a single instance of integer linear programming (ILP) that represents the whole program. The instance of this NP-hard problem must be solved to find an estimate forWCET, and it must be refined if the estimate is not tight.We propose a new framework for WCET analysis, based on abstract segment trees (ASTs) as the main data structure. The ASTs have two advantages. First, they allow computing WCET by solving a number of independent small ILP instances. Second, ASTs store more expressive constraints, thus enabling a more efficient and precise refinement procedure. In order to realize our framework algorithmically, we develop an algorithm for WCET estimation on ASTs, and we develop an interpolation-based counterexample-guided refinement scheme for ASTs. Furthermore, we extend our framework to obtain parametric estimates of WCET. We experimentally evaluate our approach on a set of examples from WCET benchmark suites and linear-algebra packages. We show that our analysis, with comparable effort, provides WCET estimates that in many cases significantly improve those computed by existing tools.","lang":"eng"}],"_id":"1836","date_published":"2015-04-01T00:00:00Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"doi":"10.1007/978-3-662-46669-8_5","language":[{"iso":"eng"}],"conference":{"location":"London, United Kingdom","start_date":"2015-04-11","end_date":"2015-04-18","name":"ESOP: European Symposium on Programming"},"title":"Segment abstraction for worst-case execution time analysis","ec_funded":1,"citation":{"mla":"Cerny, Pavol, et al. <i>Segment Abstraction for Worst-Case Execution Time Analysis</i>. Vol. 9032, Springer, 2015, pp. 105–31, doi:<a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">10.1007/978-3-662-46669-8_5</a>.","ieee":"P. Cerny, T. A. Henzinger, L. Kovács, A. Radhakrishna, and J. Zwirchmayr, “Segment abstraction for worst-case execution time analysis,” vol. 9032. Springer, pp. 105–131, 2015.","ista":"Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. 2015. Segment abstraction for worst-case execution time analysis. 9032, 105–131.","chicago":"Cerny, Pavol, Thomas A Henzinger, Laura Kovács, Arjun Radhakrishna, and Jakob Zwirchmayr. “Segment Abstraction for Worst-Case Execution Time Analysis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">https://doi.org/10.1007/978-3-662-46669-8_5</a>.","apa":"Cerny, P., Henzinger, T. A., Kovács, L., Radhakrishna, A., &#38; Zwirchmayr, J. (2015). Segment abstraction for worst-case execution time analysis. Presented at the ESOP: European Symposium on Programming, London, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">https://doi.org/10.1007/978-3-662-46669-8_5</a>","ama":"Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. Segment abstraction for worst-case execution time analysis. 2015;9032:105-131. doi:<a href=\"https://doi.org/10.1007/978-3-662-46669-8_5\">10.1007/978-3-662-46669-8_5</a>","short":"P. Cerny, T.A. Henzinger, L. Kovács, A. Radhakrishna, J. Zwirchmayr, 9032 (2015) 105–131."},"alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Laura","full_name":"Kovács, Laura","last_name":"Kovács"},{"last_name":"Radhakrishna","first_name":"Arjun","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zwirchmayr","full_name":"Zwirchmayr, Jakob","first_name":"Jakob"}],"day":"01","publisher":"Springer","status":"public","intvolume":"      9032","department":[{"_id":"ToHe"}],"quality_controlled":"1","page":"105 - 131","series_title":"Lecture Notes in Computer Science","date_created":"2018-12-11T11:54:16Z","month":"04"},{"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:53:33Z","publication_identifier":{"issn":["0018-9286"]},"publist_id":"5262","year":"2015","oa_version":"Preprint","publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1304.6603"}],"volume":60,"issue":"4","_id":"1840","abstract":[{"text":"In this paper, we present a method for reducing a regular, discrete-time Markov chain (DTMC) to another DTMC with a given, typically much smaller number of states. The cost of reduction is defined as the Kullback-Leibler divergence rate between a projection of the original process through a partition function and a DTMC on the correspondingly partitioned state space. Finding the reduced model with minimal cost is computationally expensive, as it requires an exhaustive search among all state space partitions, and an exact evaluation of the reduction cost for each candidate partition. Our approach deals with the latter problem by minimizing an upper bound on the reduction cost instead of minimizing the exact cost. The proposed upper bound is easy to compute and it is tight if the original chain is lumpable with respect to the partition. Then, we express the problem in the form of information bottleneck optimization, and propose using the agglomerative information bottleneck algorithm for searching a suboptimal partition greedily, rather than exhaustively. The theory is illustrated with examples and one application scenario in the context of modeling bio-molecular interactions.","lang":"eng"}],"date_published":"2015-04-01T00:00:00Z","acknowledgement":"This work was supported by the Austrian Research Association under Project 06/12684, by the Swiss National Science Foundation (SNSF) under Grant PP00P2 128503/1, by the SystemsX.ch (the Swiss Inititative for Systems Biology), and by a SNSF Early Postdoc.Mobility Fellowship grant P2EZP2_148797.\r\n","language":[{"iso":"eng"}],"doi":"10.1109/TAC.2014.2364971","citation":{"short":"B. Geiger, T. Petrov, G. Kubin, H. Koeppl, IEEE Transactions on Automatic Control 60 (2015) 1010–1022.","ama":"Geiger B, Petrov T, Kubin G, Koeppl H. Optimal Kullback-Leibler aggregation via information bottleneck. <i>IEEE Transactions on Automatic Control</i>. 2015;60(4):1010-1022. doi:<a href=\"https://doi.org/10.1109/TAC.2014.2364971\">10.1109/TAC.2014.2364971</a>","apa":"Geiger, B., Petrov, T., Kubin, G., &#38; Koeppl, H. (2015). Optimal Kullback-Leibler aggregation via information bottleneck. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/TAC.2014.2364971\">https://doi.org/10.1109/TAC.2014.2364971</a>","chicago":"Geiger, Bernhard, Tatjana Petrov, Gernot Kubin, and Heinz Koeppl. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 2015. <a href=\"https://doi.org/10.1109/TAC.2014.2364971\">https://doi.org/10.1109/TAC.2014.2364971</a>.","ieee":"B. Geiger, T. Petrov, G. Kubin, and H. Koeppl, “Optimal Kullback-Leibler aggregation via information bottleneck,” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 4. IEEE, pp. 1010–1022, 2015.","ista":"Geiger B, Petrov T, Kubin G, Koeppl H. 2015. Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. 60(4), 1010–1022.","mla":"Geiger, Bernhard, et al. “Optimal Kullback-Leibler Aggregation via Information Bottleneck.” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 4, IEEE, 2015, pp. 1010–22, doi:<a href=\"https://doi.org/10.1109/TAC.2014.2364971\">10.1109/TAC.2014.2364971</a>."},"title":"Optimal Kullback-Leibler aggregation via information bottleneck","day":"01","type":"journal_article","author":[{"first_name":"Bernhard","full_name":"Geiger, Bernhard","last_name":"Geiger"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana","first_name":"Tatjana","last_name":"Petrov"},{"last_name":"Kubin","first_name":"Gernot","full_name":"Kubin, Gernot"},{"last_name":"Koeppl","full_name":"Koeppl, Heinz","first_name":"Heinz"}],"publisher":"IEEE","publication":"IEEE Transactions on Automatic Control","quality_controlled":"1","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"intvolume":"        60","status":"public","page":"1010 - 1022","month":"04","date_created":"2018-12-11T11:54:18Z"},{"publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:45:19Z","volume":52,"article_processing_charge":"No","issue":"2-3","file":[{"checksum":"fb4037ddc4fc05f33080dd3547ede350","access_level":"open_access","date_updated":"2020-07-14T12:45:19Z","creator":"dernst","file_size":488482,"file_name":"2015_ActaInfo_Benes.pdf","date_created":"2020-05-15T08:57:44Z","file_id":"7854","relation":"main_file","content_type":"application/pdf"}],"abstract":[{"lang":"eng","text":"Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS."}],"_id":"1846","date_published":"2015-04-01T00:00:00Z","scopus_import":1,"date_updated":"2021-01-12T06:53:35Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_type":"original","publist_id":"5255","has_accepted_license":"1","year":"2015","oa_version":"Submitted Version","publisher":"Springer","publication":"Acta Informatica","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","status":"public","intvolume":"        52","page":"269 - 297","month":"04","date_created":"2018-12-11T11:54:20Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"language":[{"iso":"eng"}],"ddc":["000"],"doi":"10.1007/s00236-015-0215-4","citation":{"short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. 2015;52(2-3):269-297. doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>","apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., &#38; Srba, J. (2015). Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>","chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>.","ista":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.","ieee":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” <i>Acta Informatica</i>, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.","mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>."},"ec_funded":1,"title":"Refinement checking on parametric modal transition systems","day":"01","type":"journal_article","author":[{"full_name":"Beneš, Nikola","first_name":"Nikola","last_name":"Beneš"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Larsen","first_name":"Kim","full_name":"Larsen, Kim"},{"last_name":"Möller","first_name":"Mikael","full_name":"Möller, Mikael"},{"full_name":"Sickert, Salomon","first_name":"Salomon","last_name":"Sickert"},{"full_name":"Srba, Jiří","first_name":"Jiří","last_name":"Srba"}]},{"issue":"1","article_number":"9","_id":"1856","date_published":"2015-02-01T00:00:00Z","abstract":[{"lang":"eng","text":"The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε &gt; 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way."}],"publication_status":"published","main_file_link":[{"url":"https://arxiv.org/abs/1004.0739","open_access":"1"}],"oa":1,"volume":62,"publist_id":"5244","oa_version":"Preprint","year":"2015","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T11:46:04Z","month":"02","date_created":"2018-12-11T11:54:23Z","publisher":"ACM","publication":"Journal of the ACM","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"status":"public","intvolume":"        62","citation":{"apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2015). Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. 2015;62(1). doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM 62 (2015).","mla":"Chatterjee, Krishnendu, et al. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>, vol. 62, no. 1, 9, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>.","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and synthesizing systems in probabilistic environments,” <i>Journal of the ACM</i>, vol. 62, no. 1. ACM, 2015.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2015. Measuring and synthesizing systems in probabilistic environments. Journal of the ACM. 62(1), 9.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>."},"ec_funded":1,"title":"Measuring and synthesizing systems in probabilistic environments","day":"01","type":"journal_article","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jobstmann, Barbara","first_name":"Barbara","last_name":"Jobstmann"},{"first_name":"Rohit","full_name":"Singh, Rohit","last_name":"Singh"}],"related_material":{"record":[{"status":"public","id":"3864","relation":"earlier_version"}]},"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"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"}],"language":[{"iso":"eng"}],"doi":"10.1145/2699430"},{"status":"public","intvolume":"        25","volume":25,"publication":"ACM Transactions on Modeling and Computer Simulation","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"publisher":"ACM","publication_status":"published","date_published":"2015-02-01T00:00:00Z","_id":"1861","abstract":[{"lang":"eng","text":"Continuous-time Markov chains are commonly used in practice for modeling biochemical reaction networks in which the inherent randomness of themolecular interactions cannot be ignored. This has motivated recent research effort into methods for parameter inference and experiment design for such models. The major difficulty is that such methods usually require one to iteratively solve the chemical master equation that governs the time evolution of the probability distribution of the system. This, however, is rarely possible, and even approximation techniques remain limited to relatively small and simple systems. An alternative explored in this article is to base methods on only some low-order moments of the entire probability distribution. We summarize the theory behind such moment-based methods for parameter inference and experiment design and provide new case studies where we investigate their performance."}],"date_created":"2018-12-11T11:54:25Z","month":"02","article_number":"8","issue":"2","doi":"10.1145/2688906","scopus_import":1,"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:53:41Z","acknowledgement":"HYCON2; EC; European Commission\r\n","type":"journal_article","author":[{"orcid":"0000-0003-1615-3282","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","full_name":"Ruess, Jakob","first_name":"Jakob","last_name":"Ruess"},{"first_name":"John","full_name":"Lygeros, John","last_name":"Lygeros"}],"year":"2015","oa_version":"None","publist_id":"5238","day":"01","title":"Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks","citation":{"short":"J. Ruess, J. Lygeros, ACM Transactions on Modeling and Computer Simulation 25 (2015).","ama":"Ruess J, Lygeros J. Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2688906\">10.1145/2688906</a>","apa":"Ruess, J., &#38; Lygeros, J. (2015). Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2688906\">https://doi.org/10.1145/2688906</a>","chicago":"Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference and Experiment Design for Stochastic Biochemical Reaction Networks.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2688906\">https://doi.org/10.1145/2688906</a>.","ieee":"J. Ruess and J. Lygeros, “Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","ista":"Ruess J, Lygeros J. 2015. Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. ACM Transactions on Modeling and Computer Simulation. 25(2), 8.","mla":"Ruess, Jakob, and John Lygeros. “Moment-Based Methods for Parameter Inference and Experiment Design for Stochastic Biochemical Reaction Networks.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 8, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2688906\">10.1145/2688906</a>."}},{"publisher":"ACM","publication_status":"published","status":"public","intvolume":"        58","volume":58,"publication":"Communications of the ACM","department":[{"_id":"ToHe"}],"issue":"2","page":"86-86","date_created":"2018-12-11T11:54:26Z","_id":"1866","date_published":"2015-01-28T00:00:00Z","month":"01","doi":"10.1145/2701001","scopus_import":1,"language":[{"iso":"eng"}],"date_updated":"2021-01-12T06:53:43Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"The equivalence problem for finite automata: Technical perspective","citation":{"short":"T.A. Henzinger, J. Raskin, Communications of the ACM 58 (2015) 86–86.","ama":"Henzinger TA, Raskin J. The equivalence problem for finite automata: Technical perspective. <i>Communications of the ACM</i>. 2015;58(2):86-86. doi:<a href=\"https://doi.org/10.1145/2701001\">10.1145/2701001</a>","apa":"Henzinger, T. A., &#38; Raskin, J. (2015). The equivalence problem for finite automata: Technical perspective. <i>Communications of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2701001\">https://doi.org/10.1145/2701001</a>","chicago":"Henzinger, Thomas A, and Jean Raskin. “The Equivalence Problem for Finite Automata: Technical Perspective.” <i>Communications of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2701001\">https://doi.org/10.1145/2701001</a>.","ista":"Henzinger TA, Raskin J. 2015. The equivalence problem for finite automata: Technical perspective. Communications of the ACM. 58(2), 86–86.","ieee":"T. A. Henzinger and J. Raskin, “The equivalence problem for finite automata: Technical perspective,” <i>Communications of the ACM</i>, vol. 58, no. 2. ACM, pp. 86–86, 2015.","mla":"Henzinger, Thomas A., and Jean Raskin. “The Equivalence Problem for Finite Automata: Technical Perspective.” <i>Communications of the ACM</i>, vol. 58, no. 2, ACM, 2015, pp. 86–86, doi:<a href=\"https://doi.org/10.1145/2701001\">10.1145/2701001</a>."},"type":"journal_article","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"year":"2015","oa_version":"None","day":"28","publist_id":"5232"},{"volume":8997,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1408.1256"}],"oa":1,"publication_status":"published","_id":"1882","date_published":"2015-01-30T00:00:00Z","abstract":[{"text":"We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.","lang":"eng"}],"date_updated":"2021-01-12T06:53:49Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"year":"2015","oa_version":"Preprint","publist_id":"5216","intvolume":"      8997","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Springer","date_created":"2018-12-11T11:54:31Z","month":"01","page":"306 - 324","doi":"10.1007/978-3-319-15317-9_19","language":[{"iso":"eng"}],"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Fahrenberg","full_name":"Fahrenberg, Uli","first_name":"Uli"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Axel","full_name":"Legay, Axel","last_name":"Legay"},{"first_name":"Louis","full_name":"Traonouez, Louis","last_name":"Traonouez"}],"day":"30","conference":{"start_date":"2014-09-10","end_date":"2014-09-12","name":"FACS: Formal Aspects of Component Software","location":"Bertinoro, Italy"},"title":"Compositionality for quantitative specifications","ec_funded":1,"citation":{"short":"U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324.","apa":"Fahrenberg, U., Kretinsky, J., Legay, A., &#38; Traonouez, L. (2015). Compositionality for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>","ama":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative specifications. In: Vol 8997. Springer; 2015:306-324. doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>","ista":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.","ieee":"U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.","chicago":"Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality for Quantitative Specifications,” 8997:306–24. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>.","mla":"Fahrenberg, Uli, et al. <i>Compositionality for Quantitative Specifications</i>. Vol. 8997, Springer, 2015, pp. 306–24, doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>."}},{"publisher":"ACM","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","page":"433 - 444","month":"01","date_created":"2018-12-11T11:55:05Z","language":[{"iso":"eng"}],"doi":"10.1145/2676726.2677008","ddc":["005"],"citation":{"mla":"Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>. ACM, 2015, pp. 433–44, doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>.","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>.","ista":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct representation of concurrent trace sets. POPL: Principles of Programming Languages, 433–444.","ieee":"A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct representation of concurrent trace sets,” presented at the POPL: Principles of Programming Languages, Mumbai, India, 2015, pp. 433–444.","ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>","apa":"Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>","short":"A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM, 2015, pp. 433–444."},"conference":{"location":"Mumbai, India","name":"POPL: Principles of Programming Languages","start_date":"2015-01-15","end_date":"2015-01-17"},"title":"Succinct representation of concurrent trace sets","day":"15","type":"conference","author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","first_name":"Roopsha","last_name":"Samanta"},{"last_name":"Tarrach","first_name":"Thorsten","full_name":"Tarrach, Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487"}],"publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:45:22Z","pubrep_id":"317","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:45:22Z","checksum":"f0d4395b600f410a191256ac0b73af32","file_size":399462,"creator":"system","file_name":"IST-2015-317-v1+1_author_version.pdf","date_created":"2018-12-12T10:17:56Z","relation":"main_file","file_id":"5314","content_type":"application/pdf"}],"date_published":"2015-01-15T00:00:00Z","_id":"1992","abstract":[{"lang":"eng","text":"We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.\r\n\r\nWe claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:54:33Z","scopus_import":1,"publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publist_id":"5091","oa_version":"Submitted Version","year":"2015","has_accepted_license":"1"},{"file_date_updated":"2020-07-14T12:46:54Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"pubrep_id":"331","status":"public","publication_status":"published","publisher":"IST Austria","oa":1,"month":"04","file":[{"relation":"main_file","file_id":"5541","content_type":"application/pdf","date_created":"2018-12-12T11:54:19Z","creator":"system","file_size":569991,"file_name":"IST-2015-170-v2+2_report.pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:54Z","checksum":"3c402f47d3669c28d04d1af405a08e3f"}],"abstract":[{"lang":"eng","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.\r\nIn 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."}],"_id":"5436","date_created":"2018-12-12T11:39:19Z","date_published":"2015-04-24T00:00:00Z","page":"29","date_updated":"2023-02-23T12:25:21Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["2664-1690"]},"ddc":["000"],"doi":"10.15479/AT:IST-2015-170-v2-2","related_material":{"record":[{"status":"public","id":"1656","relation":"later_version"},{"relation":"later_version","id":"467","status":"public"},{"relation":"earlier_version","id":"5415","status":"public"}]},"day":"24","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, 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","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"type":"technical_report","has_accepted_license":"1","year":"2015","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>.","ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria, 29p.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2015.","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">10.15479/AT:IST-2015-170-v2-2</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-170-v2-2\">https://doi.org/10.15479/AT:IST-2015-170-v2-2</a>"},"title":"Nested weighted automata"}]