[{"citation":{"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. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.04.006","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.","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.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.04.006.","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,” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253."},"ec_funded":1,"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","day":"01","type":"journal_article","author":[{"first_name":"Mária","full_name":"Svoreňová, Mária","last_name":"Svoreňová"},{"first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"},{"first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Cěrná","first_name":"Ivana","full_name":"Cěrná, Ivana"},{"last_name":"Belta","full_name":"Belta, Cǎlin","first_name":"Cǎlin"}],"related_material":{"record":[{"status":"public","id":"1689","relation":"earlier_version"}]},"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","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"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_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"}],"language":[{"iso":"eng"}],"doi":"10.1016/j.nahs.2016.04.006","page":"230 - 253","month":"02","date_created":"2018-12-11T11:51:50Z","publisher":"Elsevier","isi":1,"publication":"Nonlinear Analysis: Hybrid Systems","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"intvolume":" 23","status":"public","publist_id":"5800","oa_version":"Preprint","year":"2017","scopus_import":"1","external_id":{"isi":["000390637000014"],"arxiv":["1410.5387"]},"date_updated":"2023-09-20T09:43:09Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","arxiv":1,"article_processing_charge":"No","issue":"2","date_published":"2017-02-01T00:00:00Z","_id":"1407","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 all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.","lang":"eng"}],"publication_status":"published","main_file_link":[{"url":"http://arxiv.org/abs/1410.5387","open_access":"1"}],"oa":1,"volume":23},{"publication":"Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","publisher":"ACM","publication_status":"published","month":"07","date_created":"2018-12-11T11:49:19Z","_id":"941","date_published":"2017-07-10T00:00:00Z","abstract":[{"lang":"eng","text":"Recently there has been a proliferation of automated program repair (APR) techniques, targeting various programming languages. Such techniques can be generally classified into two families: syntactic- and semantics-based. Semantics-based APR, on which we focus, typically uses symbolic execution to infer semantic constraints and then program synthesis to construct repairs conforming to them. While syntactic-based APR techniques have been shown successful on bugs in real-world programs written in both C and Java, semantics-based APR techniques mostly target C programs. This leaves empirical comparisons of the APR families not fully explored, and developers without a Java-based semantics APR technique. We present JFix, a semantics-based APR framework that targets Java, and an associated Eclipse plugin. JFix is implemented atop Symbolic PathFinder, a well-known symbolic execution engine for Java programs. It extends one particular APR technique (Angelix), and is designed to be sufficiently generic to support a variety of such techniques. We demonstrate that semantics-based APR can indeed efficiently and effectively repair a variety of classes of bugs in large real-world Java programs. This supports our claim that the framework can both support developers seeking semantics-based repair of bugs in Java programs, as well as enable larger scale empirical studies comparing syntactic- and semantics-based APR targeting Java. The demonstration of our tool is available via the project website at: https://xuanbachle.github.io/semanticsrepair/ "}],"page":"376 - 379 ","scopus_import":1,"language":[{"iso":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T08:22:05Z","doi":"10.1145/3092703.3098225","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publist_id":"6478","day":"10","type":"conference","author":[{"last_name":"Le","full_name":"Le, Xuan","first_name":"Xuan"},{"id":"3598E630-F248-11E8-B48F-1D18A9856A87","first_name":"Duc Hiep","full_name":"Chu, Duc Hiep","last_name":"Chu"},{"last_name":"Lo","first_name":"David","full_name":"Lo, David"},{"last_name":"Le Goues","full_name":"Le Goues, Claire","first_name":"Claire"},{"full_name":"Visser, Willem","first_name":"Willem","last_name":"Visser"}],"year":"2017","oa_version":"None","citation":{"chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder.” In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, 376–79. ACM, 2017. https://doi.org/10.1145/3092703.3098225.","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. JFIX: Semantics-based repair of Java programs via symbolic PathFinder. Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA: International Symposium on Software Testing and Analysis, 376–379.","ieee":"X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “JFIX: Semantics-based repair of Java programs via symbolic PathFinder,” in Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, United States, 2017, pp. 376–379.","mla":"Le, Xuan, et al. “JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder.” Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017, pp. 376–79, doi:10.1145/3092703.3098225.","short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017, pp. 376–379.","ama":"Le X, Chu DH, Lo D, Le Goues C, Visser W. JFIX: Semantics-based repair of Java programs via symbolic PathFinder. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM; 2017:376-379. doi:10.1145/3092703.3098225","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). JFIX: Semantics-based repair of Java programs via symbolic PathFinder. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 376–379). Santa Barbara, CA, United States: ACM. https://doi.org/10.1145/3092703.3098225"},"title":"JFIX: Semantics-based repair of Java programs via symbolic PathFinder","conference":{"location":"Santa Barbara, CA, United States","name":"ISSTA: International Symposium on Software Testing and Analysis","start_date":"2017-07-10","end_date":"2017-07-14"}},{"project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"doi":"10.1145/3106237.3106309","citation":{"short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, ACM, 2017, pp. 593–604.","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). S3: Syntax- and semantic-guided repair synthesis via programming by examples (Vol. F130154, pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn, Germany: ACM. https://doi.org/10.1145/3106237.3106309","ama":"Le X, Chu DH, Lo D, Le Goues C, Visser W. S3: Syntax- and semantic-guided repair synthesis via programming by examples. In: Vol F130154. ACM; 2017:593-604. doi:10.1145/3106237.3106309","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. S3: Syntax- and semantic-guided repair synthesis via programming by examples. FSE: Foundations of Software Engineering vol. F130154, 593–604.","ieee":"X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “S3: Syntax- and semantic-guided repair synthesis via programming by examples,” presented at the FSE: Foundations of Software Engineering, Paderborn, Germany, 2017, vol. F130154, pp. 593–604.","chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples,” F130154:593–604. ACM, 2017. https://doi.org/10.1145/3106237.3106309.","mla":"Le, Xuan, et al. S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples. Vol. F130154, ACM, 2017, pp. 593–604, doi:10.1145/3106237.3106309."},"title":"S3: Syntax- and semantic-guided repair synthesis via programming by examples","conference":{"name":"FSE: Foundations of Software Engineering","end_date":"2017-09-08","start_date":"2017-09-04","location":"Paderborn, Germany"},"day":"01","type":"conference","author":[{"full_name":"Le, Xuan","first_name":"Xuan","last_name":"Le"},{"id":"3598E630-F248-11E8-B48F-1D18A9856A87","first_name":"Duc Hiep","full_name":"Chu, Duc Hiep","last_name":"Chu"},{"first_name":"David","full_name":"Lo, David","last_name":"Lo"},{"last_name":"Le Goues","full_name":"Le Goues, Claire","first_name":"Claire"},{"last_name":"Visser","full_name":"Visser, Willem","first_name":"Willem"}],"publisher":"ACM","isi":1,"department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","page":"593 - 604","month":"09","date_created":"2018-12-11T11:49:19Z","external_id":{"isi":["000414279300055"]},"scopus_import":"1","date_updated":"2023-09-26T15:38:36Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"isbn":["978-145035105-8"]},"publist_id":"6477","oa_version":"None","year":"2017","publication_status":"published","volume":"F130154","article_processing_charge":"No","abstract":[{"lang":"eng","text":"A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration-based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs. "}],"_id":"942","date_published":"2017-09-01T00:00:00Z"},{"arxiv":1,"date_published":"2017-09-01T00:00:00Z","_id":"950","abstract":[{"text":"Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. \r\n","lang":"eng"}],"file":[{"creator":"system","file_size":335170,"file_name":"IST-2017-844-v1+1_concur-cr.pdf","checksum":"6d5cccf755207b91ccbef95d8275b013","access_level":"open_access","date_updated":"2020-07-14T12:48:16Z","relation":"main_file","file_id":"5318","content_type":"application/pdf","date_created":"2018-12-12T10:18:00Z"}],"article_number":"17","oa":1,"publication_status":"published","volume":85,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"pubrep_id":"844","file_date_updated":"2020-07-14T12:48:16Z","has_accepted_license":"1","year":"2017","oa_version":"Published Version","publist_id":"6466","publication_identifier":{"issn":["1868-8969"]},"date_updated":"2023-08-29T07:02:13Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"external_id":{"arxiv":["1705.01433"]},"date_created":"2018-12-11T11:49:22Z","month":"09","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","intvolume":" 85","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"conference":{"location":"Berlin, Germany","name":"CONCUR: Concurrency Theory","end_date":"2017-09-07","start_date":"2017-09-05"},"title":"Infinite-duration bidding games","citation":{"short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21","apa":"Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.","ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17.","mla":"Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21."},"alternative_title":["LIPIcs"],"type":"conference","author":[{"last_name":"Avni","full_name":"Avni, Guy","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","last_name":"Chonev","first_name":"Ventsislav K","full_name":"Chonev, Ventsislav K"}],"day":"01","related_material":{"record":[{"status":"public","id":"6752","relation":"later_version"}]},"project":[{"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","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"doi":"10.4230/LIPIcs.CONCUR.2017.21","ddc":["000"],"language":[{"iso":"eng"}]},{"project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"doi":"10.1007/978-3-319-63390-9_21","language":[{"iso":"eng"}],"title":"Model counting for recursively-defined strings","conference":{"start_date":"2017-07-24","end_date":"2017-07-28","name":"CAV: Computer Aided Verification","location":"Heidelberg, Germany"},"citation":{"short":"M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 399–418.","ama":"Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21","apa":"Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21","chicago":"Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer, 2017. https://doi.org/10.1007/978-3-319-63390-9_21.","ista":"Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.","ieee":"M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 399–418.","mla":"Trinh, Minh, et al. Model Counting for Recursively-Defined Strings. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418, doi:10.1007/978-3-319-63390-9_21."},"author":[{"full_name":"Trinh, Minh","first_name":"Minh","last_name":"Trinh"},{"full_name":"Chu, Duc Hiep","first_name":"Duc Hiep","last_name":"Chu","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Joxan","full_name":"Jaffar, Joxan","last_name":"Jaffar"}],"type":"conference","alternative_title":["LNCS"],"day":"01","isi":1,"publisher":"Springer","status":"public","intvolume":" 10427","department":[{"_id":"ToHe"}],"quality_controlled":"1","page":"399 - 418","date_created":"2018-12-11T11:49:26Z","month":"01","publication_identifier":{"issn":["03029743"]},"external_id":{"isi":["000431900900021"]},"scopus_import":"1","date_updated":"2023-09-22T09:58:02Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","editor":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"last_name":"Kunčak","full_name":"Kunčak, Viktor","first_name":"Viktor"}],"year":"2017","oa_version":"None","publist_id":"6443","publication_status":"published","volume":10427,"article_processing_charge":"No","date_published":"2017-01-01T00:00:00Z","_id":"962","abstract":[{"lang":"eng","text":"We present a new algorithm for model counting of a class of string constraints. In addition to the classic operation of concatenation, our class includes some recursively defined operations such as Kleene closure, and replacement of substrings. Additionally, our class also includes length constraints on the string expressions, which means, by requiring reasoning about numbers, that we face a multi-sorted logic. In the end, our string constraints are motivated by their use in programming for web applications. Our algorithm comprises two novel features: the ability to use a technique of (1) partial derivatives for constraints that are already in a solved form, i.e. a form where its (string) satisfiability is clearly displayed, and (2) non-progression, where cyclic reasoning in the reduction process may be terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally compare our model counter with two recent works on model counting of similar constraints, SMC [18] and ABC [5], to demonstrate its superior performance."}]},{"publication_identifier":{"issn":["18688969"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:35:50Z","scopus_import":1,"has_accepted_license":"1","oa_version":"Published Version","year":"2017","publist_id":"6438","oa":1,"publication_status":"published","volume":83,"pubrep_id":"829","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"file_date_updated":"2020-07-14T12:48:18Z","date_published":"2017-06-01T00:00:00Z","_id":"963","abstract":[{"text":"Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertex. The cost of traversing an edge depends on the number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in defining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, the traversal of the network involves an inherent delay, and so sharing and congestion of resources crucially depends on time. We study timed network games , which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. In addition, each edge has a guard, describing time intervals in which the edge can be traversed, forcing the players to spend time on vertices. Unlike earlier work that add a time component to network games, the time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We study properties of timed network games with cost-sharing or congestion cost functions: their stability, equilibrium inefficiency, and complexity. In particular, we show that the answer to the question whether we can restrict attention to boundary strategies, namely ones in which edges are traversed only at the boundaries of guards, is mixed. ","lang":"eng"}],"file":[{"file_id":"5059","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:14:10Z","file_size":369730,"creator":"system","file_name":"IST-2017-829-v1+1_mfcs-cr.pdf","access_level":"open_access","date_updated":"2020-07-14T12:48:18Z","checksum":"f55eaf7f3c36ea07801112acfedd17d5"}],"article_number":"37","related_material":{"record":[{"status":"public","relation":"later_version","id":"6005"}]},"project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"doi":"10.4230/LIPIcs.MFCS.2017.37","ddc":["004"],"language":[{"iso":"eng"}],"conference":{"location":"Aalborg, Denmark","end_date":"2017-08-25","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"title":"Timed network games with clocks","citation":{"mla":"Avni, Guy, et al. Timed Network Games with Clocks. Vol. 83, 37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.37.","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark, 2017, vol. 83.","ista":"Avni G, Guha S, Kupferman O. 2017. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 37.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.37.","apa":"Avni, G., Guha, S., & Kupferman, O. (2017). Timed network games with clocks (Vol. 83). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.37","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.37","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017."},"alternative_title":["LIPIcs"],"type":"conference","author":[{"first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"last_name":"Guha","full_name":"Guha, Shibashis","first_name":"Shibashis"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","status":"public","intvolume":" 83","department":[{"_id":"ToHe"}],"quality_controlled":"1","date_created":"2018-12-11T11:49:26Z","month":"06"},{"oa":1,"publication_status":"published","pubrep_id":"818","file_date_updated":"2018-12-12T10:16:58Z","article_processing_charge":"No","_id":"1003","date_published":"2017-05-30T00:00:00Z","abstract":[{"text":"Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology.","lang":"eng"}],"file":[{"content_type":"application/pdf","file_id":"5249","relation":"main_file","date_created":"2018-12-12T10:16:58Z","file_name":"IST-2017-818-v1+1_allIJCAI_CR.pdf","creator":"system","file_size":365172,"date_updated":"2018-12-12T10:16:58Z","access_level":"open_access"}],"publication_identifier":{"issn":["10450823"]},"date_updated":"2023-09-22T09:49:00Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","external_id":{"isi":["000764137500011"]},"scopus_import":"1","year":"2017","oa_version":"Submitted Version","has_accepted_license":"1","publist_id":"6395","isi":1,"publisher":"AAAI Press","status":"public","department":[{"_id":"ToHe"}],"quality_controlled":"1","page":"70 - 76","date_created":"2018-12-11T11:49:38Z","month":"05","project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"6006"}]},"ddc":["004"],"doi":"10.24963/ijcai.2017/11","language":[{"iso":"eng"}],"conference":{"end_date":"2017-08-25","start_date":"2017-08-19","name":"IJCAI: International Joint Conference on Artificial Intelligence ","location":"Melbourne, Australia"},"title":"An abstraction-refinement methodology for reasoning about network games","citation":{"ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. In: AAAI Press; 2017:70-76. doi:10.24963/ijcai.2017/11","apa":"Avni, G., Guha, S., & Kupferman, O. (2017). An abstraction-refinement methodology for reasoning about network games (pp. 70–76). Presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia: AAAI Press. https://doi.org/10.24963/ijcai.2017/11","short":"G. Avni, S. Guha, O. Kupferman, in:, AAAI Press, 2017, pp. 70–76.","mla":"Avni, Guy, et al. An Abstraction-Refinement Methodology for Reasoning about Network Games. AAAI Press, 2017, pp. 70–76, doi:10.24963/ijcai.2017/11.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games,” 70–76. AAAI Press, 2017. https://doi.org/10.24963/ijcai.2017/11.","ista":"Avni G, Guha S, Kupferman O. 2017. An abstraction-refinement methodology for reasoning about network games. IJCAI: International Joint Conference on Artificial Intelligence , 70–76.","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia, 2017, pp. 70–76."},"author":[{"first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"type":"conference","day":"30"},{"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-54434-1_11","project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"day":"19","type":"conference","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl","orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mishra, Samarth","first_name":"Samarth","last_name":"Mishra"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"}],"alternative_title":["LNCS"],"citation":{"apa":"Chatterjee, K., Kragl, B., Mishra, S., & Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54434-1_11","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:10.1007/978-3-662-54434-1_11.","ieee":"K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms for weighted recursive state machines,” presented at the ESOP: European Symposium on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.","ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","chicago":"Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis. “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok Yang, 10201:287–313. Springer, 2017. https://doi.org/10.1007/978-3-662-54434-1_11."},"ec_funded":1,"title":"Faster algorithms for weighted recursive state machines","conference":{"location":"Uppsala, Sweden","start_date":"2017-04-22","end_date":"2017-04-29","name":"ESOP: European Symposium on Programming"},"quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"intvolume":" 10201","status":"public","publisher":"Springer","isi":1,"month":"03","date_created":"2018-12-11T11:49:41Z","page":"287 - 313","scopus_import":"1","external_id":{"isi":["000681702400011"]},"date_updated":"2023-09-22T09:44:50Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"issn":["03029743"]},"publist_id":"6384","year":"2017","oa_version":"Submitted Version","editor":[{"last_name":"Yang","first_name":"Hongseok","full_name":"Yang, Hongseok"}],"volume":10201,"publication_status":"published","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.04914"}],"oa":1,"date_published":"2017-03-19T00:00:00Z","_id":"1011","abstract":[{"lang":"eng","text":"Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project."}],"article_processing_charge":"No"},{"publisher":"Association for Computing Machinery","publication":"Proceedings of the ACM on Programming Languages","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"intvolume":" 2","status":"public","month":"12","date_created":"2021-12-05T23:01:49Z","acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","language":[{"iso":"eng"}],"doi":"10.1145/3158121","citation":{"short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","apa":"Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158121","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158121","ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.","chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121.","mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:10.1145/3158121."},"title":"A new proof rule for almost-sure termination","conference":{"location":"Los Angeles, CA, United States","end_date":"2018-01-13","start_date":"2018-01-07","name":"POPL: Programming Languages"},"day":"07","type":"journal_article","author":[{"full_name":"Mciver, Annabelle","first_name":"Annabelle","last_name":"Mciver"},{"last_name":"Morgan","first_name":"Carroll","full_name":"Morgan, Carroll"},{"last_name":"Kaminski","first_name":"Benjamin Lucien","full_name":"Kaminski, Benjamin Lucien"},{"id":"4524F760-F248-11E8-B48F-1D18A9856A87","last_name":"Katoen","first_name":"Joost P","full_name":"Katoen, Joost P"}],"publication_status":"published","oa":1,"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158121","open_access":"1"}],"volume":2,"arxiv":1,"article_processing_charge":"No","issue":"POPL","article_number":"33","date_published":"2017-12-07T00:00:00Z","_id":"10418","abstract":[{"lang":"eng","text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains."}],"external_id":{"arxiv":["1711.03588"]},"scopus_import":"1","date_updated":"2021-12-07T08:04:14Z","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication_identifier":{"eissn":["2475-1421"]},"article_type":"original","oa_version":"Published Version","year":"2017"},{"external_id":{"isi":["000390637000011"]},"scopus_import":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2023-09-20T11:18:50Z","publist_id":"6154","oa_version":"None","year":"2017","volume":23,"publication_status":"published","_id":"1196","abstract":[{"text":"We define the . model-measuring problem: given a model . M and specification . ϕ, what is the maximal distance . ρ such that all models . M' within distance . ρ from . M satisfy (or violate) . ϕ. The model-measuring problem presupposes a distance function on models. We concentrate on . automatic distance functions, which are defined by weighted automata. The model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification; robustness problems that measure how much a model can be perturbed without violating the specification; and parameter synthesis for hybrid systems. We show that for automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular branching-time, and (c) hybrid specifications, the model-measuring problem can be solved.We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for word, tree, and hybrid automata by the . optimal-value question for the weighted versions of these automata. For automata over words and trees, we consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. For hybrid automata, we consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete) weighted automata.We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications. Further, we propose the modeling framework for model measuring to ease the specification and reduce the likelihood of errors in modeling.Finally, we present a variant of the model-measuring problem, called the . model-repair problem. The model-repair problem applies to models that do not satisfy the specification; it can be used to derive restrictions, under which the model satisfies the specification, i.e., to repair the model.","lang":"eng"}],"date_published":"2017-02-01T00:00:00Z","article_processing_charge":"No","language":[{"iso":"eng"}],"doi":"10.1016/j.nahs.2016.09.001","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"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund1 (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.\r\nA Technical Report of this article is available via: https://repository.ist.ac.at/171/","day":"01","type":"journal_article","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"citation":{"short":"T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.","apa":"Henzinger, T. A., & Otop, J. (2017). Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.09.001","ama":"Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 2017;23:166-190. doi:10.1016/j.nahs.2016.09.001","ieee":"T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,” Nonlinear Analysis: Hybrid Systems, vol. 23. Elsevier, pp. 166–190, 2017.","ista":"Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 23, 166–190.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.09.001.","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” Nonlinear Analysis: Hybrid Systems, vol. 23, Elsevier, 2017, pp. 166–90, doi:10.1016/j.nahs.2016.09.001."},"ec_funded":1,"title":"Model measuring for discrete and hybrid systems","publication":"Nonlinear Analysis: Hybrid Systems","quality_controlled":"1","department":[{"_id":"ToHe"}],"status":"public","intvolume":" 23","publisher":"Elsevier","isi":1,"month":"02","date_created":"2018-12-11T11:50:39Z","page":"166 - 190"},{"intvolume":" 58","status":"public","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2018-12-11T11:50:05Z","month":"08","doi":"10.4230/LIPIcs.MFCS.2016.24","ddc":["004"],"language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under grant 2014/15/D/ST6/04543.","project":[{"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"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"alternative_title":["LIPIcs"],"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"type":"conference","day":"01","conference":{"name":"MFCS: Mathematical Foundations of Computer Science (SG)","end_date":"2016-08-26","start_date":"2016-08-22","location":"Krakow; Poland"},"title":"Nested weighted limit-average automata of bounded width","ec_funded":1,"citation":{"ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.MFCS.2016.24","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.24","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Chatterjee, Krishnendu, et al. Nested Weighted Limit-Average Automata of Bounded Width. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.MFCS.2016.24.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.24.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average automata of bounded width,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland, 2016, vol. 58.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 58, 24."},"volume":58,"pubrep_id":"795","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"file_date_updated":"2018-12-12T10:17:31Z","oa":1,"publication_status":"published","abstract":[{"text":" While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.","lang":"eng"}],"_id":"1090","date_published":"2016-08-01T00:00:00Z","file":[{"creator":"system","file_size":564560,"file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf","access_level":"open_access","date_updated":"2018-12-12T10:17:31Z","file_id":"5286","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:17:31Z"}],"article_number":"24","date_updated":"2021-01-12T06:48:12Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"has_accepted_license":"1","year":"2016","oa_version":"Published Version","publist_id":"6286"},{"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","intvolume":" 59","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"date_created":"2018-12-11T11:50:06Z","month":"08","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"related_material":{"record":[{"id":"1155","relation":"dissertation_contains","status":"public"}]},"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","ddc":["004"],"doi":"10.4230/LIPIcs.CONCUR.2016.20","language":[{"iso":"eng"}],"title":"Linear distances between Markov chains","conference":{"name":"CONCUR: Concurrency Theory","end_date":"2016-08-26","start_date":"2016-08-23","location":"Quebec City; Canada"},"citation":{"ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59."},"ec_funded":1,"type":"conference","author":[{"last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"alternative_title":["LIPIcs"],"day":"01","oa":1,"publication_status":"published","pubrep_id":"794","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"volume":59,"file_date_updated":"2018-12-12T10:11:39Z","_id":"1093","date_published":"2016-08-01T00:00:00Z","abstract":[{"text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. ","lang":"eng"}],"file":[{"creator":"system","file_size":501827,"file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","access_level":"open_access","date_updated":"2018-12-12T10:11:39Z","relation":"main_file","file_id":"4895","content_type":"application/pdf","date_created":"2018-12-12T10:11:39Z"}],"article_number":"20","scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T11:58:33Z","has_accepted_license":"1","oa_version":"Published Version","year":"2016","publist_id":"6283"},{"scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:48:14Z","has_accepted_license":"1","oa_version":"Published Version","year":"2016","publist_id":"6280","pubrep_id":"793","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"volume":59,"file_date_updated":"2018-12-12T10:10:10Z","oa":1,"publication_status":"published","_id":"1095","date_published":"2016-08-01T00:00:00Z","abstract":[{"lang":"eng","text":" The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. "}],"file":[{"file_name":"IST-2017-793-v1+1_LIPIcs-CONCUR-2016-6.pdf","file_size":589747,"creator":"system","date_updated":"2018-12-12T10:10:10Z","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_id":"4795","date_created":"2018-12-12T10:10:10Z"}],"article_number":"6","ddc":["004"],"doi":"10.4230/LIPIcs.CONCUR.2016.6","language":[{"iso":"eng"}],"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"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","name":"The Wittgenstein Prize","grant_number":"Z211"}],"acknowledgement":"This work has been supported by the National Research Network RiSE on Rigorous Systems Engineering\r\n(Austrian Science Fund (FWF): S11402-N23, S11403-N23, S11404-N23, S11411-N23), a Google\r\nPhD Fellowship, an Erwin Schrödinger Fellowship (Austrian Science Fund (FWF): J3696-N26), EPSRC\r\ngrants EP/H005633/1 and EP/K008528/1, the Vienna Science and Technology Fund (WWTF) trough\r\ngrant PROSEED, the European Research Council (ERC) under grant 267989 (QUAREM) and by the\r\nAustrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","type":"conference","author":[{"full_name":"Haas, Andreas","first_name":"Andreas","last_name":"Haas"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Holzer","full_name":"Holzer, Andreas","first_name":"Andreas"},{"last_name":"Kirsch","first_name":"Christoph","full_name":"Kirsch, Christoph"},{"first_name":"Michael","full_name":"Lippautz, Michael","last_name":"Lippautz"},{"full_name":"Payer, Hannes","first_name":"Hannes","last_name":"Payer"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","full_name":"Sezgin, Ali","last_name":"Sezgin"},{"first_name":"Ana","full_name":"Sokolova, Ana","last_name":"Sokolova"},{"full_name":"Veith, Helmut","first_name":"Helmut","last_name":"Veith"}],"alternative_title":["LIPIcs"],"day":"01","title":"Local linearizability for concurrent container-type data structures","conference":{"location":"Quebec City; Canada","end_date":"2016-08-26","start_date":"2016-08-23","name":"CONCUR: Concurrency Theory"},"citation":{"apa":"Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H., … Veith, H. (2016). Local linearizability for concurrent container-type data structures. In Leibniz International Proceedings in Informatics (Vol. 59). Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6","ama":"Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent container-type data structures. In: Leibniz International Proceedings in Informatics. Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.6","short":"A. Haas, T.A. Henzinger, A. Holzer, C. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova, H. Veith, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Haas, Andreas, et al. “Local Linearizability for Concurrent Container-Type Data Structures.” Leibniz International Proceedings in Informatics, vol. 59, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.6.","ieee":"A. Haas et al., “Local linearizability for concurrent container-type data structures,” in Leibniz International Proceedings in Informatics, Quebec City; Canada, 2016, vol. 59.","ista":"Haas A, Henzinger TA, Holzer A, Kirsch C, Lippautz M, Payer H, Sezgin A, Sokolova A, Veith H. 2016. Local linearizability for concurrent container-type data structures. Leibniz International Proceedings in Informatics. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 6.","chicago":"Haas, Andreas, Thomas A Henzinger, Andreas Holzer, Christoph Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. “Local Linearizability for Concurrent Container-Type Data Structures.” In Leibniz International Proceedings in Informatics, Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6."},"ec_funded":1,"intvolume":" 59","status":"public","publication":"Leibniz International Proceedings in Informatics","quality_controlled":"1","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_created":"2018-12-11T11:50:07Z","month":"08"},{"scopus_import":1,"language":[{"iso":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:48:18Z","doi":"10.1109/MEMCOD.2016.7797741","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","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"This work was supported in part by DST-SERB, GoI under Project No. YSS/2014/000623 and by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","publist_id":"6272","day":"27","author":[{"last_name":"Gurung","first_name":"Amit","full_name":"Gurung, Amit"},{"first_name":"Arup","full_name":"Deka, Arup","last_name":"Deka"},{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"},{"last_name":"Ray","full_name":"Ray, Rajarshi","first_name":"Rajarshi"}],"type":"conference","year":"2016","oa_version":"Preprint","citation":{"mla":"Gurung, Amit, et al. Parallel Reachability Analysis for Hybrid Systems. 7797741, IEEE, 2016, doi:10.1109/MEMCOD.2016.7797741.","chicago":"Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016. https://doi.org/10.1109/MEMCOD.2016.7797741.","ista":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel reachability analysis for hybrid systems. MEMOCODE: International Conference on Formal Methods and Models for System Design, 7797741.","ieee":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel reachability analysis for hybrid systems,” presented at the MEMOCODE: International Conference on Formal Methods and Models for System Design, Kanpur, India , 2016.","ama":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability analysis for hybrid systems. In: IEEE; 2016. doi:10.1109/MEMCOD.2016.7797741","apa":"Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., & Ray, R. (2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE: International Conference on Formal Methods and Models for System Design, Kanpur, India : IEEE. https://doi.org/10.1109/MEMCOD.2016.7797741","short":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE, 2016."},"ec_funded":1,"title":"Parallel reachability analysis for hybrid systems","conference":{"name":"MEMOCODE: International Conference on Formal Methods and Models for System Design","end_date":"2016-11-20","start_date":"2016-11-18","location":"Kanpur, India "},"department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","publication_status":"published","publisher":"IEEE","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1606.05473"}],"month":"12","article_number":"7797741","_id":"1103","date_published":"2016-12-27T00:00:00Z","abstract":[{"lang":"eng","text":"We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA."}],"date_created":"2018-12-11T11:50:09Z"},{"file_date_updated":"2021-11-17T13:46:55Z","publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf"}],"file":[{"file_size":1523935,"creator":"dernst","file_name":"2016_Tarrach_Thesis.pdf","checksum":"319a506831650327e85376db41fc1094","access_level":"open_access","date_updated":"2021-02-22T11:39:32Z","file_id":"9179","relation":"main_file","content_type":"application/pdf","date_created":"2021-02-22T11:39:32Z","success":1},{"access_level":"closed","date_updated":"2021-11-17T13:46:55Z","checksum":"39efcd789f0ad859ff15652cb7afc412","file_size":1306068,"creator":"cchlebak","file_name":"2016_Tarrach_Thesispdfa.pdf","date_created":"2021-11-16T14:14:38Z","relation":"main_file","file_id":"10296","content_type":"application/pdf"}],"_id":"1130","date_published":"2016-07-07T00:00:00Z","abstract":[{"lang":"eng","text":"In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion\r\nstatements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency."}],"article_processing_charge":"No","date_updated":"2023-09-07T11:57:01Z","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"issn":["2663-337X"]},"publist_id":"6230","year":"2016","has_accepted_license":"1","oa_version":"Published Version","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"status":"public","publisher":"Institute of Science and Technology Austria","degree_awarded":"PhD","month":"07","date_created":"2018-12-11T11:50:19Z","supervisor":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"page":"151","language":[{"iso":"eng"}],"doi":"10.15479/at:ista:1130","ddc":["000"],"related_material":{"record":[{"id":"1729","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","id":"2218","status":"public"},{"relation":"part_of_dissertation","id":"2445","status":"public"}]},"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"day":"07","alternative_title":["ISTA Thesis"],"type":"dissertation","author":[{"full_name":"Tarrach, Thorsten","first_name":"Thorsten","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487"}],"ec_funded":1,"citation":{"ieee":"T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent programs,” Institute of Science and Technology Austria, 2016.","ista":"Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent programs. Institute of Science and Technology Austria.","chicago":"Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for Concurrent Programs.” Institute of Science and Technology Austria, 2016. https://doi.org/10.15479/at:ista:1130.","mla":"Tarrach, Thorsten. Automatic Synthesis of Synchronisation Primitives for Concurrent Programs. Institute of Science and Technology Austria, 2016, doi:10.15479/at:ista:1130.","short":"T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent Programs, Institute of Science and Technology Austria, 2016.","apa":"Tarrach, T. (2016). Automatic synthesis of synchronisation primitives for concurrent programs. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:1130","ama":"Tarrach T. Automatic synthesis of synchronisation primitives for concurrent programs. 2016. doi:10.15479/at:ista:1130"},"title":"Automatic synthesis of synchronisation primitives for concurrent programs"},{"month":"10","article_number":"7587948","abstract":[{"text":"Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.","lang":"eng"}],"_id":"1134","date_published":"2016-10-10T00:00:00Z","date_created":"2018-12-11T11:50:20Z","publication":"2016 IEEE Conference on Control Applications","department":[{"_id":"ToHe"}],"quality_controlled":"1","status":"public","publication_status":"published","publisher":"IEEE","day":"10","publist_id":"6224","type":"conference","author":[{"last_name":"Duggirala","full_name":"Duggirala, Parasara","first_name":"Parasara"},{"full_name":"Fan, Chuchu","first_name":"Chuchu","last_name":"Fan"},{"first_name":"Matthew","full_name":"Potok, Matthew","last_name":"Potok"},{"full_name":"Qi, Bolun","first_name":"Bolun","last_name":"Qi"},{"full_name":"Mitra, Sayan","first_name":"Sayan","last_name":"Mitra"},{"last_name":"Viswanathan","full_name":"Viswanathan, Mahesh","first_name":"Mahesh"},{"full_name":"Bak, Stanley","first_name":"Stanley","last_name":"Bak"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov"},{"first_name":"Taylor","full_name":"Johnson, Taylor","last_name":"Johnson"},{"last_name":"Nguyen","full_name":"Nguyen, Luan","first_name":"Luan"},{"orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"},{"last_name":"Sogokon","first_name":"Andrew","full_name":"Sogokon, Andrew"},{"full_name":"Tran, Hoang","first_name":"Hoang","last_name":"Tran"},{"full_name":"Xiang, Weiming","first_name":"Weiming","last_name":"Xiang"}],"oa_version":"None","year":"2016","citation":{"short":"P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang, in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.","ama":"Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In: 2016 IEEE Conference on Control Applications. IEEE; 2016. doi:10.1109/CCA.2016.7587948","apa":"Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In 2016 IEEE Conference on Control Applications. Buenos Aires, Argentina : IEEE. https://doi.org/10.1109/CCA.2016.7587948","chicago":"Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In 2016 IEEE Conference on Control Applications. IEEE, 2016. https://doi.org/10.1109/CCA.2016.7587948.","ieee":"P. Duggirala et al., “Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP,” in 2016 IEEE Conference on Control Applications, Buenos Aires, Argentina , 2016.","ista":"Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications , 7587948.","mla":"Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” 2016 IEEE Conference on Control Applications, 7587948, IEEE, 2016, doi:10.1109/CCA.2016.7587948."},"title":"Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP","conference":{"location":"Buenos Aires, Argentina ","name":"CCA: Control Applications ","start_date":"2016-09-19","end_date":"2016-09-22"},"scopus_import":1,"language":[{"iso":"eng"}],"date_updated":"2021-01-12T06:48:32Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","doi":"10.1109/CCA.2016.7587948"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"ddc":["000"],"doi":"10.1145/2968478.2968499","language":[{"iso":"eng"}],"conference":{"location":"Pittsburgh, PA, USA","name":"EMSOFT: Embedded Software ","end_date":"2016-10-07","start_date":"2016-10-01"},"title":"Synthesizing time triggered schedules for switched networks with faulty links","ec_funded":1,"citation":{"apa":"Avni, G., Guha, S., & Rodríguez Navas, G. (2016). Synthesizing time triggered schedules for switched networks with faulty links. In Proceedings of the 13th International Conference on Embedded Software . Pittsburgh, PA, USA: ACM. https://doi.org/10.1145/2968478.2968499","ama":"Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for switched networks with faulty links. In: Proceedings of the 13th International Conference on Embedded Software . ACM; 2016. doi:10.1145/2968478.2968499","short":"G. Avni, S. Guha, G. Rodríguez Navas, in:, Proceedings of the 13th International Conference on Embedded Software , ACM, 2016.","mla":"Avni, Guy, et al. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” Proceedings of the 13th International Conference on Embedded Software , 26, ACM, 2016, doi:10.1145/2968478.2968499.","ista":"Avni G, Guha S, Rodríguez Navas G. 2016. Synthesizing time triggered schedules for switched networks with faulty links. Proceedings of the 13th International Conference on Embedded Software . EMSOFT: Embedded Software , 26.","ieee":"G. Avni, S. Guha, and G. Rodríguez Navas, “Synthesizing time triggered schedules for switched networks with faulty links,” in Proceedings of the 13th International Conference on Embedded Software , Pittsburgh, PA, USA, 2016.","chicago":"Avni, Guy, Shibashis Guha, and Guillermo Rodríguez Navas. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” In Proceedings of the 13th International Conference on Embedded Software . ACM, 2016. https://doi.org/10.1145/2968478.2968499."},"type":"conference","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","full_name":"Avni, Guy","first_name":"Guy"},{"last_name":"Guha","first_name":"Shibashis","full_name":"Guha, Shibashis"},{"full_name":"Rodríguez Navas, Guillermo","first_name":"Guillermo","last_name":"Rodríguez Navas"}],"day":"01","publisher":"ACM","status":"public","quality_controlled":"1","department":[{"_id":"ToHe"}],"publication":"Proceedings of the 13th International Conference on Embedded Software ","date_created":"2018-12-11T11:50:20Z","month":"10","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:48:33Z","scopus_import":1,"oa_version":"Submitted Version","has_accepted_license":"1","year":"2016","publist_id":"6223","oa":1,"publication_status":"published","pubrep_id":"644","file_date_updated":"2018-12-12T10:09:31Z","_id":"1135","date_published":"2016-10-01T00:00:00Z","abstract":[{"text":"Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM.","lang":"eng"}],"article_number":"26","file":[{"content_type":"application/pdf","file_id":"4755","relation":"main_file","date_created":"2018-12-12T10:09:31Z","file_name":"IST-2016-644-v1+1_emsoft-no-format.pdf","creator":"system","file_size":279240,"date_updated":"2018-12-12T10:09:31Z","access_level":"open_access"}]},{"type":"conference","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"day":"05","conference":{"end_date":"2016-07-08","start_date":"2016-07-05","name":"LICS: Logic in Computer Science","location":"New York, NY, USA"},"title":"Quantitative automata under probabilistic semantics","ec_funded":1,"citation":{"ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE; 2016:76-85. doi:10.1145/2933575.2933588","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative automata under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium (pp. 76–85). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2933588","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.” Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85, doi:10.1145/2933575.2933588.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In Proceedings of the 31st Annual ACM/IEEE Symposium, 76–85. IEEE, 2016. https://doi.org/10.1145/2933575.2933588.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 76–85.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in Proceedings of the 31st Annual ACM/IEEE Symposium, New York, NY, USA, 2016, pp. 76–85."},"doi":"10.1145/2933575.2933588","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) projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S114","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"date_created":"2018-12-11T11:50:21Z","month":"07","page":"76 - 85","status":"public","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","publisher":"IEEE","oa_version":"Preprint","year":"2016","publist_id":"6220","date_updated":"2021-01-12T06:48:34Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"external_id":{"arxiv":["1604.06764"]},"_id":"1138","date_published":"2016-07-05T00:00:00Z","abstract":[{"text":"Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.","lang":"eng"}],"arxiv":1,"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"publication_status":"published"},{"day":"01","author":[{"first_name":"Christian","full_name":"Schilling, Christian","last_name":"Schilling"},{"first_name":"Sergiy","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","full_name":"Podelski, Andreas","last_name":"Podelski"},{"last_name":"Ruess","full_name":"Ruess, Jakob","first_name":"Jakob","id":"4A245D00-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1615-3282"}],"type":"journal_article","citation":{"short":"C. Schilling, S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, Biosystems 149 (2016) 15–25.","ama":"Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. Adaptive moment closure for parameter inference of biochemical reaction networks. Biosystems. 2016;149:15-25. doi:10.1016/j.biosystems.2016.07.005","apa":"Schilling, C., Bogomolov, S., Henzinger, T. A., Podelski, A., & Ruess, J. (2016). Adaptive moment closure for parameter inference of biochemical reaction networks. Biosystems. Elsevier. https://doi.org/10.1016/j.biosystems.2016.07.005","chicago":"Schilling, Christian, Sergiy Bogomolov, Thomas A Henzinger, Andreas Podelski, and Jakob Ruess. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” Biosystems. Elsevier, 2016. https://doi.org/10.1016/j.biosystems.2016.07.005.","ista":"Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. 2016. Adaptive moment closure for parameter inference of biochemical reaction networks. Biosystems. 149, 15–25.","ieee":"C. Schilling, S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess, “Adaptive moment closure for parameter inference of biochemical reaction networks,” Biosystems, vol. 149. Elsevier, pp. 15–25, 2016.","mla":"Schilling, Christian, et al. “Adaptive Moment Closure for Parameter Inference of Biochemical Reaction Networks.” Biosystems, vol. 149, Elsevier, 2016, pp. 15–25, doi:10.1016/j.biosystems.2016.07.005."},"ec_funded":1,"title":"Adaptive moment closure for parameter inference of biochemical reaction networks","language":[{"iso":"eng"}],"doi":"10.1016/j.biosystems.2016.07.005","related_material":{"record":[{"relation":"earlier_version","id":"1658","status":"public"}]},"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"acknowledgement":"This work is based on the CMSB 2015 paper “Adaptive moment closure for parameter inference of biochemical reaction networks” (Bogomolov et al., 2015). The 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 AVACS1), 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). J.R. acknowledges support from the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. 291734.","month":"11","date_created":"2018-12-11T11:50:24Z","page":"15 - 25","publication":"Biosystems","department":[{"_id":"ToHe"},{"_id":"GaTk"}],"quality_controlled":"1","status":"public","intvolume":" 149","publisher":"Elsevier","publist_id":"6210","oa_version":"None","year":"2016","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:08:46Z","_id":"1148","date_published":"2016-11-01T00:00:00Z","abstract":[{"text":"Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space. © 2016 Elsevier Ireland Ltd","lang":"eng"}],"volume":149,"publication_status":"published"},{"date_updated":"2023-02-23T12:26:41Z","language":[{"iso":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5443"}],"link":[{"relation":"table_of_contents","url":"https://dl.acm.org/citation.cfm?id=3016355"}]},"publist_id":"6191","day":"02","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"378E0060-F248-11E8-B48F-1D18A9856A87","first_name":"Jessica","full_name":"Davies, Jessica","last_name":"Davies"}],"type":"conference","year":"2016","oa_version":"None","citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016:3225–32. AAAI Press, 2016.","ista":"Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232.","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps,” in Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA, 2016, vol. 2016, pp. 3225–3232.","mla":"Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, vol. 2016, AAAI Press, 2016, pp. 3225–32.","short":"K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.","ama":"Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. Vol 2016. AAAI Press; 2016:3225-3232.","apa":"Chatterjee, K., Chmelik, M., & Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (Vol. 2016, pp. 3225–3232). Phoenix, AZ, USA: AAAI Press."},"ec_funded":1,"title":"A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps","conference":{"location":"Phoenix, AZ, USA","start_date":"2016-02-12","end_date":"2016-02-17","name":"AAAI: Conference on Artificial Intelligence"},"publication":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","intvolume":" 2016","status":"public","volume":2016,"publication_status":"published","publisher":"AAAI Press","month":"12","_id":"1166","abstract":[{"lang":"eng","text":"POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved."}],"date_created":"2018-12-11T11:50:30Z","date_published":"2016-12-02T00:00:00Z","page":"3225 - 3232"}]