[{"related_material":{"record":[{"status":"public","id":"1659","relation":"later_version"}]},"pubrep_id":"335","day":"18","year":"2015","status":"public","publication_identifier":{"issn":["2664-1690"]},"page":"20","doi":"10.15479/AT:IST-2015-335-v1-1","oa":1,"date_created":"2018-12-12T11:39:20Z","_id":"5439","type":"technical_report","date_published":"2015-05-18T00:00:00Z","file_date_updated":"2020-07-14T12:46:55Z","publisher":"IST Austria","language":[{"iso":"eng"}],"title":"The target discounted-sum problem","month":"05","publication_status":"published","has_accepted_license":"1","abstract":[{"text":"The target discounted-sum problem is the following: Given a rational discount factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata. ","lang":"eng"}],"ddc":["004","512","513"],"file":[{"file_name":"IST-2015-335-v1+1_report.pdf","date_updated":"2020-07-14T12:46:55Z","date_created":"2018-12-12T11:53:55Z","content_type":"application/pdf","file_size":589619,"access_level":"open_access","creator":"system","file_id":"5517","checksum":"40405907aa012acece1bc26cf0be554d","relation":"main_file"}],"author":[{"full_name":"Boker, Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}],"date_updated":"2023-02-23T10:08:48Z","oa_version":"Published Version","citation":{"short":"U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST Austria, 2015.","mla":"Boker, Udi, et al. The Target Discounted-Sum Problem. IST Austria, 2015, doi:10.15479/AT:IST-2015-335-v1-1.","apa":"Boker, U., Henzinger, T. A., & Otop, J. (2015). The target discounted-sum problem. IST Austria. https://doi.org/10.15479/AT:IST-2015-335-v1-1","ista":"Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST Austria, 20p.","ama":"Boker U, Henzinger TA, Otop J. The Target Discounted-Sum Problem. IST Austria; 2015. doi:10.15479/AT:IST-2015-335-v1-1","chicago":"Boker, Udi, Thomas A Henzinger, and Jan Otop. The Target Discounted-Sum Problem. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-335-v1-1.","ieee":"U. Boker, T. A. Henzinger, and J. Otop, The target discounted-sum problem. IST Austria, 2015."}},{"citation":{"mla":"Chatterjee, Krishnendu, et al. The Complexity of Evolutionary Games on Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-323-v2-2.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolutionary Games on Graphs, IST Austria, 2015.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2015). The complexity of evolutionary games on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-323-v2-2","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. The Complexity of Evolutionary Games on Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-323-v2-2","ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2015. The complexity of evolutionary games on graphs, IST Austria, 18p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity of Evolutionary Games on Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-323-v2-2.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolutionary games on graphs. IST Austria, 2015."},"oa_version":"Published Version","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:26:10Z","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"ddc":["005","576"],"file":[{"date_created":"2018-12-12T11:53:23Z","date_updated":"2020-07-14T12:46:56Z","content_type":"application/pdf","file_name":"IST-2015-323-v2+2_main.pdf","relation":"main_file","access_level":"open_access","file_size":466161,"checksum":"66aace7d367032af97c15e35c9be9636","file_id":"5484","creator":"system"}],"has_accepted_license":"1","month":"06","publication_status":"published","abstract":[{"lang":"eng","text":"Evolution occurs in populations of reproducing individuals. The structure of the population affects the outcome of the evolutionary process. Evolutionary graph theory is a powerful approach to study this phenomenon. There are two graphs. The interaction graph specifies who interacts with whom for payoff in the context of evolution. The replacement graph specifies who competes with whom for reproduction. The vertices of the two graphs are the same, and each vertex corresponds to an individual of the population. The fitness (or the reproductive rate) is a non-negative number, and depends on the payoff. A key quantity is the fixation probability of a new mutant. It is defined as the probability that a newly introduced mutant (on a single vertex) generates a lineage of offspring which eventually takes over the entire population of resident individuals. The basic computational questions are as follows: (i) the qualitative question asks whether the fixation probability is positive; and (ii) the quantitative approximation question asks for an approximation of the fixation probability. Our main results are as follows: First, we consider a special case of the general problem, where the residents do not reproduce. We show that the qualitative question is NP-complete, and the quantitative approximation question is #P-complete, and the hardness results hold even in the special case where the interaction and the replacement graphs coincide. Second, we show that in general both the qualitative and the quantitative approximation questions are PSPACE-complete. The PSPACE-hardness result for quantitative approximation holds even when the fitness is always positive."}],"title":"The complexity of evolutionary games on graphs","date_published":"2015-06-16T00:00:00Z","file_date_updated":"2020-07-14T12:46:56Z","publisher":"IST Austria","language":[{"iso":"eng"}],"_id":"5440","type":"technical_report","date_created":"2018-12-12T11:39:21Z","oa":1,"doi":"10.15479/AT:IST-2015-323-v2-2","page":"18","day":"16","publication_identifier":{"issn":["2664-1690"]},"year":"2015","status":"public","related_material":{"record":[{"id":"5421","relation":"earlier_version","status":"public"},{"relation":"earlier_version","id":"5432","status":"public"}]},"pubrep_id":"338"},{"date_created":"2018-12-12T11:39:21Z","oa":1,"type":"technical_report","_id":"5441","page":"24","publication_identifier":{"issn":["2664-1690"]},"day":"11","doi":"10.15479/AT:IST-2015-340-v1-1","status":"public","year":"2015","pubrep_id":"340","related_material":{"record":[{"relation":"later_version","id":"1437","status":"public"},{"relation":"earlier_version","id":"5442","status":"public"},{"status":"public","id":"6009","relation":"later_version"}]},"department":[{"_id":"KrCh"}],"date_updated":"2023-09-19T14:36:19Z","oa_version":"Published Version","citation":{"mla":"Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015, doi:10.15479/AT:IST-2015-340-v1-1.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria, 2015.","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria, 2015.","apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A. (2015). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria. https://doi.org/10.15479/AT:IST-2015-340-v1-1","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria; 2015. doi:10.15479/AT:IST-2015-340-v1-1","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2015. Algorithms for algebraic path properties in concurrent systems of constant treewidth components, IST Austria, 24p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-340-v1-1."},"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389"},{"first_name":"Amir","last_name":"Goharshady","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas"}],"alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","month":"07","publication_status":"published","abstract":[{"text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.","lang":"eng"}],"ddc":["000"],"file":[{"checksum":"df383dc62c94d7b2ea639aba088a76c6","file_id":"5531","creator":"system","access_level":"open_access","file_size":861396,"relation":"main_file","file_name":"IST-2015-340-v1+1_main.pdf","content_type":"application/pdf","date_created":"2018-12-12T11:54:09Z","date_updated":"2020-07-14T12:46:56Z"}],"language":[{"iso":"eng"}],"date_published":"2015-07-11T00:00:00Z","publisher":"IST Austria","file_date_updated":"2020-07-14T12:46:56Z","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components"},{"citation":{"chicago":"Anonymous, 1, 2 Anonymous, 3 Anonymous, and 4 Anonymous. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015.","ista":"Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. 2015. Algorithms for algebraic path properties in concurrent systems of constant treewidth components, IST Austria, 22p.","ama":"Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria; 2015.","apa":"Anonymous, 1, Anonymous, 2, Anonymous, 3, & Anonymous, 4. (2015). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria.","ieee":"1 Anonymous, 2 Anonymous, 3 Anonymous, and 4 Anonymous, Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria, 2015.","short":"1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria, 2015.","mla":"Anonymous, 1, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015."},"oa_version":"Published Version","date_updated":"2023-09-19T14:36:19Z","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Anonymous, 1","first_name":"1","last_name":"Anonymous"},{"full_name":"Anonymous, 2","last_name":"Anonymous","first_name":"2"},{"full_name":"Anonymous, 3","first_name":"3","last_name":"Anonymous"},{"first_name":"4","last_name":"Anonymous","full_name":"Anonymous, 4"}],"ddc":["000"],"file":[{"access_level":"open_access","file_size":658747,"checksum":"98fd936102f3e057fc321ef6d316001d","file_id":"5498","creator":"system","relation":"main_file","file_name":"IST-2015-343-v2+1_main.pdf","date_created":"2018-12-12T11:53:37Z","date_updated":"2020-07-14T12:46:57Z","content_type":"application/pdf"},{"relation":"main_file","file_id":"6316","checksum":"b31d09b1241b59c75e1f42dadf09d258","creator":"dernst","access_level":"closed","file_size":139,"content_type":"text/plain","date_created":"2019-04-16T12:36:08Z","date_updated":"2020-07-14T12:46:57Z","file_name":"IST-2015-343-v2+2_anonymous.txt"}],"has_accepted_license":"1","publication_status":"published","month":"07","abstract":[{"lang":"eng","text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural properties that arise in program analysis.\r\nWe consider that each component of the concurrent system is a graph with constant treewidth, and it is known that the controlflow graphs of most programs have constant treewidth. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis problems (e.g., alias analysis). The study of multiple queries allows us to consider the tradeoff between the resource usage of the \\emph{one-time} preprocessing and for \\emph{each individual} query. The traditional approaches construct the product graph of all components and apply the best-known graph algorithm on the product. In the traditional approach, even the answer to a single query requires the transitive closure computation (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\n\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, \r\neach subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results that show that the worst-case running times of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (such as improving \r\nthe worst-case bounds for the shortest path problem in general graphs whose current best-known bound has not been improved in five decades). Finally, we provide a prototype implementation of our algorithms which significantly outperforms the existing algorithmic methods on several benchmarks."}],"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","date_published":"2015-07-14T00:00:00Z","file_date_updated":"2020-07-14T12:46:57Z","publisher":"IST Austria","language":[{"iso":"eng"}],"type":"technical_report","_id":"5442","date_created":"2018-12-12T11:39:21Z","oa":1,"day":"14","status":"public","page":"22","year":"2015","publication_identifier":{"issn":["2664-1690"]},"scopus_import":1,"pubrep_id":"344","related_material":{"record":[{"id":"1437","relation":"later_version","status":"public"},{"status":"public","relation":"later_version","id":"5441"},{"status":"public","id":"6009","relation":"later_version"}]}},{"abstract":[{"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 EXPTIME-complete, 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.","lang":"eng"}],"publication_status":"published","month":"11","has_accepted_license":"1","file":[{"file_id":"5466","checksum":"f0fa31ad8161ed655137e94012123ef9","creator":"system","access_level":"open_access","file_size":412379,"relation":"main_file","file_name":"IST-2015-325-v2+1_main.pdf","content_type":"application/pdf","date_created":"2018-12-12T11:53:05Z","date_updated":"2020-07-14T12:46:57Z"}],"ddc":["000"],"file_date_updated":"2020-07-14T12:46:57Z","date_published":"2015-11-06T00:00:00Z","language":[{"iso":"eng"}],"publisher":"IST Austria","title":"A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs","date_updated":"2023-02-21T16:24:05Z","department":[{"_id":"KrCh"}],"oa_version":"Published Version","citation":{"short":"K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015, doi:10.15479/AT:IST-2015-325-v2-1.","apa":"Chatterjee, K., Chmelik, M., & Davies, J. (2015). A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria. https://doi.org/10.15479/AT:IST-2015-325-v2-1","ama":"Chatterjee K, Chmelik M, Davies J. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria; 2015. doi:10.15479/AT:IST-2015-325-v2-1","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-325-v2-1.","ista":"Chatterjee K, Chmelik M, Davies J. 2015. A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs, IST Austria, 23p.","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria, 2015."},"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin"},{"full_name":"Davies, Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87","last_name":"Davies","first_name":"Jessica"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["IST Austria Technical Report"],"pubrep_id":"362","related_material":{"record":[{"status":"public","id":"1166","relation":"later_version"}]},"oa":1,"date_created":"2018-12-12T11:39:22Z","type":"technical_report","_id":"5443","year":"2015","page":"23","doi":"10.15479/AT:IST-2015-325-v2-1","publication_identifier":{"issn":["2664-1690"]},"day":"06","status":"public"},{"file":[{"date_updated":"2020-07-14T12:46:58Z","date_created":"2018-12-12T11:53:24Z","content_type":"application/pdf","file_name":"IST-2015-399-v1+1_treeomics.pdf","relation":"main_file","file_size":3533200,"access_level":"open_access","creator":"system","checksum":"c47d33bdda06181753c0af36f16e7b5d","file_id":"5485"}],"ddc":["000","576"],"month":"12","has_accepted_license":"1","publication_status":"published","abstract":[{"text":"A comprehensive understanding of the clonal evolution of cancer is critical for understanding neoplasia. Genome-wide sequencing data enables evolutionary studies at unprecedented depth. However, classical phylogenetic methods often struggle with noisy sequencing data of impure DNA samples and fail to detect subclones that have different evolutionary trajectories. We have developed a tool, called Treeomics, that allows us to reconstruct the phylogeny of a cancer with commonly available sequencing technologies. Using Bayesian inference and Integer Linear Programming, robust phylogenies consistent with the biological processes underlying cancer evolution were obtained for pancreatic, ovarian, and prostate cancers. Furthermore, Treeomics correctly identified sequencing artifacts such as those resulting from low statistical power; nearly 7% of variants were misclassified by conventional statistical methods. These artifacts can skew phylogenies by creating illusory tumor heterogeneity among distinct samples. Importantly, we show that the evolutionary trees generated with Treeomics are mathematically optimal.","lang":"eng"}],"title":"Reconstructing robust phylogenies of metastatic cancers","file_date_updated":"2020-07-14T12:46:58Z","language":[{"iso":"eng"}],"publisher":"IST Austria","date_published":"2015-12-30T00:00:00Z","oa_version":"Published Version","citation":{"short":"J. Reiter, A. Makohon-Moore, J. Gerold, I. Bozic, K. Chatterjee, C. Iacobuzio-Donahue, B. Vogelstein, M. Nowak, Reconstructing Robust Phylogenies of Metastatic Cancers, IST Austria, 2015.","mla":"Reiter, Johannes, et al. Reconstructing Robust Phylogenies of Metastatic Cancers. IST Austria, 2015, doi:10.15479/AT:IST-2015-399-v1-1.","apa":"Reiter, J., Makohon-Moore, A., Gerold, J., Bozic, I., Chatterjee, K., Iacobuzio-Donahue, C., … Nowak, M. (2015). Reconstructing robust phylogenies of metastatic cancers. IST Austria. https://doi.org/10.15479/AT:IST-2015-399-v1-1","chicago":"Reiter, Johannes, Alvin Makohon-Moore, Jeffrey Gerold, Ivana Bozic, Krishnendu Chatterjee, Christine Iacobuzio-Donahue, Bert Vogelstein, and Martin Nowak. Reconstructing Robust Phylogenies of Metastatic Cancers. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-399-v1-1.","ista":"Reiter J, Makohon-Moore A, Gerold J, Bozic I, Chatterjee K, Iacobuzio-Donahue C, Vogelstein B, Nowak M. 2015. Reconstructing robust phylogenies of metastatic cancers, IST Austria, 25p.","ama":"Reiter J, Makohon-Moore A, Gerold J, et al. Reconstructing Robust Phylogenies of Metastatic Cancers. IST Austria; 2015. doi:10.15479/AT:IST-2015-399-v1-1","ieee":"J. Reiter et al., Reconstructing robust phylogenies of metastatic cancers. IST Austria, 2015."},"department":[{"_id":"KrCh"}],"date_updated":"2020-07-14T23:05:07Z","alternative_title":["IST Austria Technical Report"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","full_name":"Reiter, Johannes","first_name":"Johannes","last_name":"Reiter","orcid":"0000-0002-0170-7353"},{"first_name":"Alvin","last_name":"Makohon-Moore","full_name":"Makohon-Moore, Alvin"},{"first_name":"Jeffrey","last_name":"Gerold","full_name":"Gerold, Jeffrey"},{"last_name":"Bozic","first_name":"Ivana","full_name":"Bozic, Ivana"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Iacobuzio-Donahue, Christine","last_name":"Iacobuzio-Donahue","first_name":"Christine"},{"first_name":"Bert","last_name":"Vogelstein","full_name":"Vogelstein, Bert"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"pubrep_id":"399","_id":"5444","type":"technical_report","date_created":"2018-12-12T11:39:22Z","oa":1,"page":"25","day":"30","publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2015-399-v1-1","status":"public","year":"2015"},{"tmp":{"short":"CC0 (1.0)","name":"Creative Commons Public Domain Dedication (CC0 1.0)","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","image":"/images/cc_0.png"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"A. Fellner, (2015).","mla":"Fellner, Andreas. Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria, 2015, doi:10.15479/AT:ISTA:28.","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:28","ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, 10.15479/AT:ISTA:28.","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. https://doi.org/10.15479/AT:ISTA:28.","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:10.15479/AT:ISTA:28","ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015."},"date_updated":"2024-02-21T13:52:07Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","publisher":"Institute of Science and Technology Austria","file_date_updated":"2020-07-14T12:47:00Z","date_published":"2015-08-13T00:00:00Z","ddc":["004"],"abstract":[{"lang":"eng","text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication."}],"day":"13","year":"2015","doi":"10.15479/AT:ISTA:28","oa":1,"publist_id":"5564","related_material":{"record":[{"relation":"popular_science","id":"1603","status":"public"}]},"keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"author":[{"full_name":"Fellner, Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","last_name":"Fellner","first_name":"Andreas"}],"oa_version":"Published Version","contributor":[{"last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"project":[{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"article_processing_charge":"No","file":[{"content_type":"application/zip","date_updated":"2020-07-14T12:47:00Z","date_created":"2018-12-12T13:02:31Z","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","relation":"main_file","creator":"system","checksum":"b8bcb43c0893023cda66c1b69c16ac62","file_id":"5597","file_size":49557109,"access_level":"open_access"}],"has_accepted_license":"1","month":"08","status":"public","_id":"5549","type":"research_data","datarep_id":"28","date_created":"2018-12-12T12:31:29Z","ec_funded":1},{"date_created":"2019-03-19T14:15:50Z","type":"journal_article","_id":"6118","status":"public","publication_identifier":{"issn":["0027-8424","1091-6490"]},"has_accepted_license":"1","month":"07","issue":"27","file":[{"date_updated":"2020-07-14T12:47:20Z","date_created":"2019-03-19T14:21:07Z","content_type":"application/pdf","file_name":"2015_PNAS_Fenk.pdf","relation":"main_file","file_size":2822681,"access_level":"open_access","creator":"kschuh","file_id":"6119","checksum":"3d2da5af8d72467e382a565abc2e003d"}],"language":[{"iso":"eng"}],"volume":112,"quality_controlled":"1","oa_version":"Published Version","author":[{"full_name":"Fenk, Lorenz A.","first_name":"Lorenz A.","last_name":"Fenk"},{"first_name":"Mario","last_name":"de Bono","orcid":"0000-0001-8347-0443","id":"4E3FF80E-F248-11E8-B48F-1D18A9856A87","full_name":"de Bono, Mario"}],"intvolume":" 112","publication":"Proceedings of the National Academy of Sciences","oa":1,"year":"2015","page":"E3525-E3534","doi":"10.1073/pnas.1423808112","day":"07","abstract":[{"text":"Carbon dioxide (CO2) gradients are ubiquitous and provide animals with information about their environment, such as the potential presence of prey or predators. The nematode Caenorhabditis elegans avoids elevated CO2, and previous work identified three neuron pairs called “BAG,” “AFD,” and “ASE” that respond to CO2 stimuli. Using in vivo Ca2+ imaging and behavioral analysis, we show that C. elegans can detect CO2 independently of these sensory pathways. Many of the C. elegans sensory neurons we examined, including the AWC olfactory neurons, the ASJ and ASK gustatory neurons, and the ASH and ADL nociceptors, respond to a rise in CO2 with a rise in Ca2+. In contrast, glial sheath cells harboring the sensory endings of C. elegans’ major chemosensory neurons exhibit strong and sustained decreases in Ca2+ in response to high CO2. Some of these CO2 responses appear to be cell intrinsic. Worms therefore may couple detection of CO2 to that of other cues at the earliest stages of sensory processing. We show that C. elegans persistently suppresses oviposition at high CO2. Hermaphrodite-specific neurons (HSNs), the executive neurons driving egg-laying, are tonically inhibited when CO2 is elevated. CO2 modulates the egg-laying system partly through the AWC olfactory neurons: High CO2 tonically activates AWC by a cGMP-dependent mechanism, and AWC output inhibits the HSNs. Our work shows that CO2 is a more complex sensory cue for C. elegans than previously thought, both in terms of behavior and neural circuitry.","lang":"eng"}],"publication_status":"published","ddc":["570"],"date_published":"2015-07-07T00:00:00Z","file_date_updated":"2020-07-14T12:47:20Z","publisher":"National Academy of Sciences","pmid":1,"title":"Environmental CO2 inhibits Caenorhabditis elegans egg-laying by modulating olfactory neurons and evokes widespread changes in neural activity","date_updated":"2021-01-12T08:06:12Z","extern":"1","citation":{"ieee":"L. A. Fenk and M. de Bono, “Environmental CO2 inhibits Caenorhabditis elegans egg-laying by modulating olfactory neurons and evokes widespread changes in neural activity,” Proceedings of the National Academy of Sciences, vol. 112, no. 27. National Academy of Sciences, pp. E3525–E3534, 2015.","ama":"Fenk LA, de Bono M. Environmental CO2 inhibits Caenorhabditis elegans egg-laying by modulating olfactory neurons and evokes widespread changes in neural activity. Proceedings of the National Academy of Sciences. 2015;112(27):E3525-E3534. doi:10.1073/pnas.1423808112","ista":"Fenk LA, de Bono M. 2015. Environmental CO2 inhibits Caenorhabditis elegans egg-laying by modulating olfactory neurons and evokes widespread changes in neural activity. Proceedings of the National Academy of Sciences. 112(27), E3525–E3534.","chicago":"Fenk, Lorenz A., and Mario de Bono. “Environmental CO2 Inhibits Caenorhabditis Elegans Egg-Laying by Modulating Olfactory Neurons and Evokes Widespread Changes in Neural Activity.” Proceedings of the National Academy of Sciences. National Academy of Sciences, 2015. https://doi.org/10.1073/pnas.1423808112.","apa":"Fenk, L. A., & de Bono, M. (2015). Environmental CO2 inhibits Caenorhabditis elegans egg-laying by modulating olfactory neurons and evokes widespread changes in neural activity. Proceedings of the National Academy of Sciences. National Academy of Sciences. https://doi.org/10.1073/pnas.1423808112","short":"L.A. Fenk, M. de Bono, Proceedings of the National Academy of Sciences 112 (2015) E3525–E3534.","mla":"Fenk, Lorenz A., and Mario de Bono. “Environmental CO2 Inhibits Caenorhabditis Elegans Egg-Laying by Modulating Olfactory Neurons and Evokes Widespread Changes in Neural Activity.” Proceedings of the National Academy of Sciences, vol. 112, no. 27, National Academy of Sciences, 2015, pp. E3525–34, doi:10.1073/pnas.1423808112."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","external_id":{"pmid":["26100886"]}},{"intvolume":" 4","publication":"eLife","oa":1,"day":"11","doi":"10.7554/elife.04241","year":"2015","publication_status":"published","abstract":[{"lang":"eng","text":"Brains organize behavior and physiology to optimize the response to threats or opportunities. We dissect how 21% O2, an indicator of surface exposure, reprograms C. elegans' global state, inducing sustained locomotory arousal and altering expression of neuropeptides, metabolic enzymes, and other non-neural genes. The URX O2-sensing neurons drive arousal at 21% O2 by tonically activating the RMG interneurons. Stimulating RMG is sufficient to switch behavioral state. Ablating the ASH, ADL, or ASK sensory neurons connected to RMG by gap junctions does not disrupt arousal. However, disrupting cation currents in these neurons curtails RMG neurosecretion and arousal. RMG signals high O2 by peptidergic secretion. Neuropeptide reporters reveal neural circuit state, as neurosecretion stimulates neuropeptide expression. Neural imaging in unrestrained animals shows that URX and RMG encode O2 concentration rather than behavior, while the activity of downstream interneurons such as AVB and AIY reflect both O2 levels and the behavior being executed."}],"ddc":["570"],"pmid":1,"publisher":"eLife Sciences Publications","file_date_updated":"2020-07-14T12:47:20Z","date_published":"2015-03-11T00:00:00Z","title":"Decoding a neural circuit controlling global animal state in C. elegans","extern":"1","date_updated":"2021-01-12T08:06:13Z","citation":{"ieee":"P. Laurent et al., “Decoding a neural circuit controlling global animal state in C. elegans,” eLife, vol. 4. eLife Sciences Publications, 2015.","apa":"Laurent, P., Soltesz, Z., Nelson, G. M., Chen, C., Arellano-Carbajal, F., Levy, E., & de Bono, M. (2015). Decoding a neural circuit controlling global animal state in C. elegans. ELife. eLife Sciences Publications. https://doi.org/10.7554/elife.04241","chicago":"Laurent, Patrick, Zoltan Soltesz, Geoffrey M Nelson, Changchun Chen, Fausto Arellano-Carbajal, Emmanuel Levy, and Mario de Bono. “Decoding a Neural Circuit Controlling Global Animal State in C. Elegans.” ELife. eLife Sciences Publications, 2015. https://doi.org/10.7554/elife.04241.","ista":"Laurent P, Soltesz Z, Nelson GM, Chen C, Arellano-Carbajal F, Levy E, de Bono M. 2015. Decoding a neural circuit controlling global animal state in C. elegans. eLife. 4, e04241.","ama":"Laurent P, Soltesz Z, Nelson GM, et al. Decoding a neural circuit controlling global animal state in C. elegans. eLife. 2015;4. doi:10.7554/elife.04241","mla":"Laurent, Patrick, et al. “Decoding a Neural Circuit Controlling Global Animal State in C. Elegans.” ELife, vol. 4, e04241, eLife Sciences Publications, 2015, doi:10.7554/elife.04241.","short":"P. Laurent, Z. Soltesz, G.M. Nelson, C. Chen, F. Arellano-Carbajal, E. Levy, M. de Bono, ELife 4 (2015)."},"external_id":{"pmid":["25760081"]},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_created":"2019-03-19T14:23:51Z","type":"journal_article","_id":"6120","status":"public","publication_identifier":{"issn":["2050-084X"]},"has_accepted_license":"1","month":"03","article_number":"e04241","file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:47:20Z","date_created":"2019-03-19T14:29:43Z","file_name":"2015_elife_Laurent.pdf","relation":"main_file","creator":"kschuh","checksum":"cf641b7a363aecd0a101755d23dee7e0","file_id":"6121","file_size":6723528,"access_level":"open_access"}],"language":[{"iso":"eng"}],"volume":4,"quality_controlled":"1","oa_version":"Published Version","author":[{"first_name":"Patrick","last_name":"Laurent","full_name":"Laurent, Patrick"},{"last_name":"Soltesz","first_name":"Zoltan","full_name":"Soltesz, Zoltan"},{"last_name":"Nelson","first_name":"Geoffrey M","full_name":"Nelson, Geoffrey M"},{"first_name":"Changchun","last_name":"Chen","full_name":"Chen, Changchun"},{"full_name":"Arellano-Carbajal, Fausto","last_name":"Arellano-Carbajal","first_name":"Fausto"},{"first_name":"Emmanuel","last_name":"Levy","full_name":"Levy, Emmanuel"},{"full_name":"de Bono, Mario","id":"4E3FF80E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8347-0443","first_name":"Mario","last_name":"de Bono"}]},{"publication":"Asterisque","publist_id":"5723","intvolume":" 2015","page":"113 - 156","day":"01","main_file_link":[{"url":"http://arxiv.org/abs/1309.4914","open_access":"1"}],"year":"2015","status":"public","_id":"1473","type":"review","date_created":"2018-12-11T11:52:13Z","oa":1,"title":"Cohomology of large semiprojective hyperkähler varieties","volume":2015,"publisher":"Societe Mathematique de France","date_published":"2015-01-01T00:00:00Z","issue":"370","publication_status":"published","month":"01","abstract":[{"text":"In this paper we survey geometric and arithmetic techniques to study the cohomology of semiprojective hyperkähler manifolds including toric hyperkähler varieties, Nakajima quiver varieties and moduli spaces of Higgs bundles on Riemann surfaces. The resulting formulae for their Poincaré polynomials are combinatorial and representation theoretical in nature. In particular we will look at their Betti numbers and will establish some results and state some expectations on their asymptotic shape.","lang":"eng"}],"author":[{"full_name":"Tamas Hausel","id":"4A0666D8-F248-11E8-B48F-1D18A9856A87","first_name":"Tamas","last_name":"Hausel"},{"full_name":"Rodríguez Villegas, Fernando","first_name":"Fernando","last_name":"Rodríguez Villegas"}],"citation":{"apa":"Hausel, T., & Rodríguez Villegas, F. (2015). Cohomology of large semiprojective hyperkähler varieties. Asterisque. Societe Mathematique de France.","ama":"Hausel T, Rodríguez Villegas F. Cohomology of large semiprojective hyperkähler varieties. Asterisque. 2015;2015(370):113-156.","ista":"Hausel T, Rodríguez Villegas F. 2015. Cohomology of large semiprojective hyperkähler varieties. Asterisque. 2015(370), 113–156.","chicago":"Hausel, Tamás, and Fernando Rodríguez Villegas. “Cohomology of Large Semiprojective Hyperkähler Varieties.” Asterisque. Societe Mathematique de France, 2015.","ieee":"T. Hausel and F. Rodríguez Villegas, “Cohomology of large semiprojective hyperkähler varieties,” Asterisque, vol. 2015, no. 370. Societe Mathematique de France, pp. 113–156, 2015.","mla":"Hausel, Tamás, and Fernando Rodríguez Villegas. “Cohomology of Large Semiprojective Hyperkähler Varieties.” Asterisque, vol. 2015, no. 370, Societe Mathematique de France, 2015, pp. 113–56.","short":"T. Hausel, F. Rodríguez Villegas, Asterisque 2015 (2015) 113–156."},"quality_controlled":0,"extern":1,"date_updated":"2021-01-12T06:50:59Z"},{"date_updated":"2021-01-12T06:50:59Z","department":[{"_id":"KrPi"}],"quality_controlled":"1","project":[{"name":"Provable Security for Physical Cryptography","grant_number":"259668","_id":"258C570E-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa_version":"Submitted Version","citation":{"apa":"Ferrara, A., Fuchsbauer, G., Liu, B., & Warinschi, B. (2015). Policy privacy in cryptographic access control (pp. 46–60). Presented at the CSF: Computer Security Foundations, Verona, Italy: IEEE. https://doi.org/10.1109/CSF.2015.11","chicago":"Ferrara, Anna, Georg Fuchsbauer, Bin Liu, and Bogdan Warinschi. “Policy Privacy in Cryptographic Access Control,” 46–60. IEEE, 2015. https://doi.org/10.1109/CSF.2015.11.","ama":"Ferrara A, Fuchsbauer G, Liu B, Warinschi B. Policy privacy in cryptographic access control. In: IEEE; 2015:46-60. doi:10.1109/CSF.2015.11","ista":"Ferrara A, Fuchsbauer G, Liu B, Warinschi B. 2015. Policy privacy in cryptographic access control. CSF: Computer Security Foundations, 46–60.","ieee":"A. Ferrara, G. Fuchsbauer, B. Liu, and B. Warinschi, “Policy privacy in cryptographic access control,” presented at the CSF: Computer Security Foundations, Verona, Italy, 2015, pp. 46–60.","mla":"Ferrara, Anna, et al. Policy Privacy in Cryptographic Access Control. IEEE, 2015, pp. 46–60, doi:10.1109/CSF.2015.11.","short":"A. Ferrara, G. Fuchsbauer, B. Liu, B. Warinschi, in:, IEEE, 2015, pp. 46–60."},"author":[{"full_name":"Ferrara, Anna","last_name":"Ferrara","first_name":"Anna"},{"last_name":"Fuchsbauer","first_name":"Georg","full_name":"Fuchsbauer, Georg","id":"46B4C3EE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Bin","last_name":"Liu","full_name":"Liu, Bin"},{"first_name":"Bogdan","last_name":"Warinschi","full_name":"Warinschi, Bogdan"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"Cryptographic access control offers selective access to encrypted data via a combination of key management and functionality-rich cryptographic schemes, such as attribute-based encryption. Using this approach, publicly available meta-data may inadvertently leak information on the access policy that is enforced by cryptography, which renders cryptographic access control unusable in settings where this information is highly sensitive. We begin to address this problem by presenting rigorous definitions for policy privacy in cryptographic access control. For concreteness we set our results in the model of Role-Based Access Control (RBAC), where we identify and formalize several different flavors of privacy, however, our framework should serve as inspiration for other models of access control. Based on our insights we propose a new system which significantly improves on the privacy properties of state-of-the-art constructions. Our design is based on a novel type of privacy-preserving attribute-based encryption, which we introduce and show how to instantiate. We present our results in the context of a cryptographic RBAC system by Ferrara et al. (CSF'13), which uses cryptography to control read access to files, while write access is still delegated to trusted monitors. We give an extension of the construction that permits cryptographic control over write access. Our construction assumes that key management uses out-of-band channels between the policy enforcer and the users but eliminates completely the need for monitoring read/write access to the data.","lang":"eng"}],"publication_status":"published","month":"09","date_published":"2015-09-04T00:00:00Z","language":[{"iso":"eng"}],"publisher":"IEEE","article_processing_charge":"No","title":"Policy privacy in cryptographic access control","date_created":"2018-12-11T11:52:14Z","oa":1,"type":"conference","_id":"1474","main_file_link":[{"url":"http://epubs.surrey.ac.uk/808055/","open_access":"1"}],"page":"46-60","doi":"10.1109/CSF.2015.11","day":"04","status":"public","year":"2015","ec_funded":1,"publist_id":"5722","conference":{"start_date":"2015-07-13","end_date":"2015-07-17","name":"CSF: Computer Security Foundations","location":"Verona, Italy"}},{"publist_id":"5713","intvolume":" 2","publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence","scopus_import":1,"related_material":{"record":[{"status":"public","id":"5410","relation":"earlier_version"}]},"acknowledgement":"A Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/146.\r\n","page":"745 - 752","year":"2015","day":"01","oa":1,"publisher":"AAAI Press","date_published":"2015-01-01T00:00:00Z","title":"Automatic generation of alternative starting positions for simple traditional board games","publication_status":"published","abstract":[{"lang":"eng","text":"Simple board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in the development of mathematical and logical skills, but also in the emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. We present an approach that generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. The presence of such states for standard game variants like 4×4 Tic-Tac-Toe opens up new games to be played that have never been played as the default start state is heavily biased. "}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:25:07Z","citation":{"mla":"Ahmed, Umair, et al. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, vol. 2, AAAI Press, 2015, pp. 745–52.","short":"U. Ahmed, K. Chatterjee, S. Gulwani, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI Press, 2015, pp. 745–752.","apa":"Ahmed, U., Chatterjee, K., & Gulwani, S. (2015). Automatic generation of alternative starting positions for simple traditional board games. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (Vol. 2, pp. 745–752). Austin, TX, USA: AAAI Press.","ista":"Ahmed U, Chatterjee K, Gulwani S. 2015. Automatic generation of alternative starting positions for simple traditional board games. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2, 745–752.","ama":"Ahmed U, Chatterjee K, Gulwani S. Automatic generation of alternative starting positions for simple traditional board games. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. Vol 2. AAAI Press; 2015:745-752.","chicago":"Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2:745–52. AAAI Press, 2015.","ieee":"U. Ahmed, K. Chatterjee, and S. Gulwani, “Automatic generation of alternative starting positions for simple traditional board games,” in Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, Austin, TX, USA, 2015, vol. 2, pp. 745–752."},"conference":{"name":"AAAI: Conference on Artificial Intelligence","location":"Austin, TX, USA","start_date":"2015-01-25","end_date":"2015-01-30"},"ec_funded":1,"status":"public","main_file_link":[{"url":"https://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/download/9523/9300","open_access":"1"}],"date_created":"2018-12-11T11:52:16Z","_id":"1481","type":"conference","language":[{"iso":"eng"}],"volume":2,"article_processing_charge":"No","month":"01","author":[{"full_name":"Ahmed, Umair","last_name":"Ahmed","first_name":"Umair"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Gulwani, Sumit","first_name":"Sumit","last_name":"Gulwani"}],"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","oa_version":"None"},{"scopus_import":1,"conference":{"name":"CVPR: Computer Vision and Pattern Recognition","location":"Boston, MA, USA","end_date":"2015-06-12","start_date":"2015-06-07"},"publist_id":"5709","oa":1,"date_created":"2018-12-11T11:52:17Z","type":"conference","_id":"1483","status":"public","day":"14","year":"2015","publication_identifier":{"eisbn":["978-1-4673-6964-0 "]},"page":"4741 - 4748","main_file_link":[{"url":"http://arxiv.org/abs/1412.6821","open_access":"1"}],"doi":"10.1109/CVPR.2015.7299106","abstract":[{"lang":"eng","text":"Topological data analysis offers a rich source of valuable information to study vision problems. Yet, so far we lack a theoretically sound connection to popular kernel-based learning techniques, such as kernel SVMs or kernel PCA. In this work, we establish such a connection by designing a multi-scale kernel for persistence diagrams, a stable summary representation of topological features in data. We show that this kernel is positive definite and prove its stability with respect to the 1-Wasserstein distance. Experiments on two benchmark datasets for 3D shape classification/retrieval and texture recognition show considerable performance gains of the proposed method compared to an alternative approach that is based on the recently introduced persistence landscapes."}],"publication_status":"published","month":"10","date_published":"2015-10-14T00:00:00Z","publisher":"IEEE","language":[{"iso":"eng"}],"title":"A stable multi-scale kernel for topological machine learning","date_updated":"2021-01-12T06:51:03Z","department":[{"_id":"HeEd"}],"oa_version":"Preprint","citation":{"mla":"Reininghaus, Jan, et al. A Stable Multi-Scale Kernel for Topological Machine Learning. IEEE, 2015, pp. 4741–48, doi:10.1109/CVPR.2015.7299106.","short":"J. Reininghaus, S. Huber, U. Bauer, R. Kwitt, in:, IEEE, 2015, pp. 4741–4748.","ieee":"J. Reininghaus, S. Huber, U. Bauer, and R. Kwitt, “A stable multi-scale kernel for topological machine learning,” presented at the CVPR: Computer Vision and Pattern Recognition, Boston, MA, USA, 2015, pp. 4741–4748.","ama":"Reininghaus J, Huber S, Bauer U, Kwitt R. A stable multi-scale kernel for topological machine learning. In: IEEE; 2015:4741-4748. doi:10.1109/CVPR.2015.7299106","chicago":"Reininghaus, Jan, Stefan Huber, Ulrich Bauer, and Roland Kwitt. “A Stable Multi-Scale Kernel for Topological Machine Learning,” 4741–48. IEEE, 2015. https://doi.org/10.1109/CVPR.2015.7299106.","ista":"Reininghaus J, Huber S, Bauer U, Kwitt R. 2015. A stable multi-scale kernel for topological machine learning. CVPR: Computer Vision and Pattern Recognition, 4741–4748.","apa":"Reininghaus, J., Huber, S., Bauer, U., & Kwitt, R. (2015). A stable multi-scale kernel for topological machine learning (pp. 4741–4748). Presented at the CVPR: Computer Vision and Pattern Recognition, Boston, MA, USA: IEEE. https://doi.org/10.1109/CVPR.2015.7299106"},"author":[{"first_name":"Jan","last_name":"Reininghaus","full_name":"Reininghaus, Jan","id":"4505473A-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Stefan","last_name":"Huber","orcid":"0000-0002-8871-5814","id":"4700A070-F248-11E8-B48F-1D18A9856A87","full_name":"Huber, Stefan"},{"last_name":"Bauer","first_name":"Ulrich","orcid":"0000-0002-9683-0724","id":"2ADD483A-F248-11E8-B48F-1D18A9856A87","full_name":"Bauer, Ulrich"},{"first_name":"Roland","last_name":"Kwitt","full_name":"Kwitt, Roland"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"date_created":"2018-12-11T11:52:21Z","oa":1,"_id":"1495","type":"conference","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1505.03402"}],"year":"2015","page":"128-135","status":"public","day":"01","scopus_import":1,"ec_funded":1,"publist_id":"5684","conference":{"end_date":"2015-08-12","start_date":"2015-08-10","location":"Ontario, Canada","name":"CCCG: Canadian Conference on Computational Geometry"},"publication":"Proceedings of the 27th Canadian Conference on Computational Geometry","date_updated":"2021-01-12T06:51:09Z","quality_controlled":"1","department":[{"_id":"HeEd"}],"project":[{"call_identifier":"FP7","name":"Topological Complex Systems","_id":"255D761E-B435-11E9-9278-68D0E5697425","grant_number":"318493"}],"citation":{"short":"H. Edelsbrunner, M. Iglesias Ham, V. Kurlin, in:, Proceedings of the 27th Canadian Conference on Computational Geometry, Queen’s University, 2015, pp. 128–135.","mla":"Edelsbrunner, Herbert, et al. “Relaxed Disk Packing.” Proceedings of the 27th Canadian Conference on Computational Geometry, vol. 2015–August, Queen’s University, 2015, pp. 128–35.","apa":"Edelsbrunner, H., Iglesias Ham, M., & Kurlin, V. (2015). Relaxed disk packing. In Proceedings of the 27th Canadian Conference on Computational Geometry (Vol. 2015–August, pp. 128–135). Ontario, Canada: Queen’s University.","ista":"Edelsbrunner H, Iglesias Ham M, Kurlin V. 2015. Relaxed disk packing. Proceedings of the 27th Canadian Conference on Computational Geometry. CCCG: Canadian Conference on Computational Geometry vol. 2015–August, 128–135.","ama":"Edelsbrunner H, Iglesias Ham M, Kurlin V. Relaxed disk packing. In: Proceedings of the 27th Canadian Conference on Computational Geometry. Vol 2015-August. Queen’s University; 2015:128-135.","chicago":"Edelsbrunner, Herbert, Mabel Iglesias Ham, and Vitaliy Kurlin. “Relaxed Disk Packing.” In Proceedings of the 27th Canadian Conference on Computational Geometry, 2015–August:128–35. Queen’s University, 2015.","ieee":"H. Edelsbrunner, M. Iglesias Ham, and V. Kurlin, “Relaxed disk packing,” in Proceedings of the 27th Canadian Conference on Computational Geometry, Ontario, Canada, 2015, vol. 2015–August, pp. 128–135."},"oa_version":"Submitted Version","author":[{"id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","full_name":"Edelsbrunner, Herbert","last_name":"Edelsbrunner","first_name":"Herbert","orcid":"0000-0002-9823-6833"},{"full_name":"Iglesias Ham, Mabel","id":"41B58C0C-F248-11E8-B48F-1D18A9856A87","first_name":"Mabel","last_name":"Iglesias Ham"},{"last_name":"Kurlin","first_name":"Vitaliy","full_name":"Kurlin, Vitaliy"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Motivated by biological questions, we study configurations of equal-sized disks in the Euclidean plane that neither pack nor cover. Measuring the quality by the probability that a random point lies in exactly one disk, we show that the regular hexagonal grid gives the maximum among lattice configurations. "}],"publication_status":"published","month":"08","date_published":"2015-08-01T00:00:00Z","language":[{"iso":"eng"}],"publisher":"Queen's University","title":"Relaxed disk packing","volume":"2015-August"},{"oa_version":"Published Version","quality_controlled":"1","author":[{"first_name":"Daniel","last_name":"Andergassen","full_name":"Andergassen, Daniel"},{"id":"4C66542E-F248-11E8-B48F-1D18A9856A87","full_name":"Dotter, Christoph","last_name":"Dotter","first_name":"Christoph"},{"full_name":"Kulinski, Tomasz","last_name":"Kulinski","first_name":"Tomasz"},{"last_name":"Guenzl","first_name":"Philipp","full_name":"Guenzl, Philipp"},{"full_name":"Bammer, Philipp","last_name":"Bammer","first_name":"Philipp"},{"full_name":"Barlow, Denise","last_name":"Barlow","first_name":"Denise"},{"first_name":"Florian","last_name":"Pauler","full_name":"Pauler, Florian"},{"last_name":"Hudson","first_name":"Quanah","full_name":"Hudson, Quanah"}],"issue":"21","file":[{"relation":"main_file","checksum":"385b83854fd0eb2e4f386867da2823e2","file_id":"5768","creator":"dernst","access_level":"open_access","file_size":6863297,"content_type":"application/pdf","date_created":"2018-12-20T14:18:57Z","date_updated":"2020-07-14T12:44:58Z","file_name":"2015_NucleicAcidsRes_Andergassen.pdf"}],"article_number":"e146","month":"07","has_accepted_license":"1","volume":43,"language":[{"iso":"eng"}],"_id":"1497","type":"journal_article","date_created":"2018-12-11T11:52:22Z","status":"public","citation":{"apa":"Andergassen, D., Dotter, C., Kulinski, T., Guenzl, P., Bammer, P., Barlow, D., … Hudson, Q. (2015). Allelome.PRO, a pipeline to define allele-specific genomic features from high-throughput sequencing data. Nucleic Acids Research. Oxford University Press. https://doi.org/10.1093/nar/gkv727","chicago":"Andergassen, Daniel, Christoph Dotter, Tomasz Kulinski, Philipp Guenzl, Philipp Bammer, Denise Barlow, Florian Pauler, and Quanah Hudson. “Allelome.PRO, a Pipeline to Define Allele-Specific Genomic Features from High-Throughput Sequencing Data.” Nucleic Acids Research. Oxford University Press, 2015. https://doi.org/10.1093/nar/gkv727.","ama":"Andergassen D, Dotter C, Kulinski T, et al. Allelome.PRO, a pipeline to define allele-specific genomic features from high-throughput sequencing data. Nucleic Acids Research. 2015;43(21). doi:10.1093/nar/gkv727","ista":"Andergassen D, Dotter C, Kulinski T, Guenzl P, Bammer P, Barlow D, Pauler F, Hudson Q. 2015. Allelome.PRO, a pipeline to define allele-specific genomic features from high-throughput sequencing data. Nucleic Acids Research. 43(21), e146.","ieee":"D. Andergassen et al., “Allelome.PRO, a pipeline to define allele-specific genomic features from high-throughput sequencing data,” Nucleic Acids Research, vol. 43, no. 21. Oxford University Press, 2015.","short":"D. Andergassen, C. Dotter, T. Kulinski, P. Guenzl, P. Bammer, D. Barlow, F. Pauler, Q. Hudson, Nucleic Acids Research 43 (2015).","mla":"Andergassen, Daniel, et al. “Allelome.PRO, a Pipeline to Define Allele-Specific Genomic Features from High-Throughput Sequencing Data.” Nucleic Acids Research, vol. 43, no. 21, e146, Oxford University Press, 2015, doi:10.1093/nar/gkv727."},"date_updated":"2021-01-12T06:51:09Z","department":[{"_id":"GaNo"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["570"],"abstract":[{"text":"Detecting allelic biases from high-throughput sequencing data requires an approach that maximises sensitivity while minimizing false positives. Here, we present Allelome.PRO, an automated user-friendly bioinformatics pipeline, which uses high-throughput sequencing data from reciprocal crosses of two genetically distinct mouse strains to detect allele-specific expression and chromatin modifications. Allelome.PRO extends approaches used in previous studies that exclusively analyzed imprinted expression to give a complete picture of the ‘allelome’ by automatically categorising the allelic expression of all genes in a given cell type into imprinted, strain-biased, biallelic or non-informative. Allelome.PRO offers increased sensitivity to analyze lowly expressed transcripts, together with a robust false discovery rate empirically calculated from variation in the sequencing data. We used RNA-seq data from mouse embryonic fibroblasts from F1 reciprocal crosses to determine a biologically relevant allelic ratio cutoff, and define for the first time an entire allelome. Furthermore, we show that Allelome.PRO detects differential enrichment of H3K4me3 over promoters from ChIP-seq data validating the RNA-seq results. This approach can be easily extended to analyze histone marks of active enhancers, or transcription factor binding sites and therefore provides a powerful tool to identify candidate cis regulatory elements genome wide.","lang":"eng"}],"publication_status":"published","title":"Allelome.PRO, a pipeline to define allele-specific genomic features from high-throughput sequencing data","date_published":"2015-07-21T00:00:00Z","file_date_updated":"2020-07-14T12:44:58Z","publisher":"Oxford University Press","oa":1,"doi":"10.1093/nar/gkv727","year":"2015","day":"21","acknowledgement":"Austrian Science Fund [FWF P25185-B22, FWF F4302- B09, FWFW1207-B09]. Funding for open access charge: Austrian Science Fund.\r\nWe thank Florian Breitwieser for advice during the early stages of this project. High-throughput sequencing was conducted by the Biomedical Sequencing Facility (BSF) at CeMM in Vienna.","scopus_import":1,"publication":"Nucleic Acids Research","intvolume":" 43","publist_id":"5682"},{"file":[{"checksum":"cf5e94baa89a2dc4c5de01abc676eda8","file_id":"5050","creator":"system","access_level":"open_access","file_size":489362,"relation":"main_file","file_name":"IST-2016-499-v1+1_9.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:14:02Z","date_updated":"2020-07-14T12:44:58Z"}],"has_accepted_license":"1","month":"01","volume":32,"language":[{"iso":"eng"}],"oa_version":"Published Version","quality_controlled":"1","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_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"}],"author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","full_name":"Dragoi, Cezara","first_name":"Cezara","last_name":"Dragoi"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Damien","last_name":"Zufferey","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien"}],"pubrep_id":"499","ec_funded":1,"conference":{"end_date":"2015-05-06","start_date":"2015-05-03","location":"Asilomar, CA, United States","name":"SNAPL: Summit oN Advances in Programming Languages"},"type":"conference","_id":"1498","date_created":"2018-12-11T11:52:22Z","publication_identifier":{"isbn":["978-3-939897-80-4 "]},"status":"public","series_title":"Leibniz International Proceedings in Informatics","ddc":["005"],"abstract":[{"lang":"eng","text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea."}],"publication_status":"published","title":"The need for language support for fault-tolerant distributed systems","file_date_updated":"2020-07-14T12:44:58Z","date_published":"2015-01-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 90–102, 2015.","apa":"Dragoi, C., Henzinger, T. A., & Zufferey, D. (2015). The need for language support for fault-tolerant distributed systems. Presented at the SNAPL: Summit oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90","ista":"Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for fault-tolerant distributed systems. 32, 90–102.","ama":"Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:10.4230/LIPIcs.SNAPL.2015.90","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for Language Support for Fault-Tolerant Distributed Systems.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90.","mla":"Dragoi, Cezara, et al. The Need for Language Support for Fault-Tolerant Distributed Systems. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 90–102, doi:10.4230/LIPIcs.SNAPL.2015.90.","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102."},"date_updated":"2020-08-11T10:09:14Z","department":[{"_id":"ToHe"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LIPIcs"],"scopus_import":1,"intvolume":" 32","publist_id":"5681","oa":1,"day":"01","year":"2015","page":"90 - 102","doi":"10.4230/LIPIcs.SNAPL.2015.90"},{"status":"public","type":"conference","_id":"1499","date_created":"2018-12-11T11:52:22Z","ec_funded":1,"conference":{"location":"Madrid, Spain","name":"CONCUR: Concurrency Theory","end_date":"2015-09-04","start_date":"2015-09-01"},"pubrep_id":"498","author":[{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky"},{"full_name":"Larsen, Kim","last_name":"Larsen","first_name":"Kim"},{"last_name":"Laursen","first_name":"Simon","full_name":"Laursen, Simon"},{"first_name":"Jiří","last_name":"Srba","full_name":"Srba, Jiří"}],"oa_version":"Published Version","project":[{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","volume":42,"language":[{"iso":"eng"}],"file":[{"file_size":623563,"access_level":"open_access","creator":"system","checksum":"49eb5021caafaabe5356c65b9c5f8c9c","file_id":"4672","relation":"main_file","file_name":"IST-2016-498-v1+1_32.pdf","date_updated":"2020-07-14T12:44:58Z","date_created":"2018-12-12T10:08:12Z","content_type":"application/pdf"}],"month":"01","has_accepted_license":"1","page":"142 - 154","year":"2015","doi":"10.4230/LIPIcs.CONCUR.2015.142","day":"01","acknowledgement":"The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement 601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Czech Science Foundation under grant agreement P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734.","oa":1,"intvolume":" 42","publist_id":"5680","scopus_import":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LIPIcs"],"citation":{"ama":"Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:10.4230/LIPIcs.CONCUR.2015.142","ista":"Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability of weighted synchronization under partial observability. CONCUR: Concurrency Theory, LIPIcs, vol. 42, 142–154.","chicago":"Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time Decidability of Weighted Synchronization under Partial Observability,” 42:142–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.","apa":"Kretinsky, J., Larsen, K., Laursen, S., & Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142","ieee":"J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability of weighted synchronization under partial observability,” presented at the CONCUR: Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","mla":"Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142."},"date_updated":"2021-01-12T06:51:10Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"title":"Polynomial time decidability of weighted synchronization under partial observability","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2020-07-14T12:44:58Z","date_published":"2015-01-01T00:00:00Z","ddc":["000","003"],"abstract":[{"text":"We consider weighted automata with both positive and negative integer weights on edges and\r\nstudy the problem of synchronization using adaptive strategies that may only observe whether\r\nthe current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.","lang":"eng"}],"publication_status":"published"},{"oa_version":"Preprint","quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","last_name":"Daca"}],"issue":"2","month":"10","volume":47,"language":[{"iso":"eng"}],"_id":"1501","type":"journal_article","date_created":"2018-12-11T11:52:23Z","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1405.0835"}],"status":"public","ec_funded":1,"citation":{"mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” Formal Methods in System Design, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:10.1007/s10703-015-0235-2.","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264.","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” Formal Methods in System Design, vol. 47, no. 2. Springer, pp. 230–264, 2015.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” Formal Methods in System Design. Springer, 2015. https://doi.org/10.1007/s10703-015-0235-2.","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 2015;47(2):230-264. doi:10.1007/s10703-015-0235-2","apa":"Chatterjee, K., Chmelik, M., & Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-015-0235-2"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2023-09-07T11:58:33Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","abstract":[{"text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. ","lang":"eng"}],"title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","date_published":"2015-10-01T00:00:00Z","publisher":"Springer","oa":1,"day":"01","page":"230 - 264","year":"2015","doi":"10.1007/s10703-015-0235-2","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","scopus_import":1,"related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"publication":"Formal Methods in System Design","publist_id":"5677","intvolume":" 47"},{"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23(RiSE) and Z211-N23 (Wittgestein Award), by People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373 (nSafeCer). Jan Křetínský has been partially supported by the Czech Science Foundation, grant No. P202/12/G061. Nikola Beneš has been supported by the\r\nMEYS project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.","day":"01","page":"101 - 110","year":"2015","doi":"10.1145/2737166.2737175","oa":1,"publist_id":"5676","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1155"}]},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"date_updated":"2023-09-07T11:58:33Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"citation":{"short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","mla":"Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory. ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.","ieee":"N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.","chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. https://doi.org/10.1145/2737166.2737175.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175","ista":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition operators for IOCO-testing theory. CBSE: Component-Based Software Engineering , Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering , , 101–110.","apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., & Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. https://doi.org/10.1145/2737166.2737175"},"date_published":"2015-05-01T00:00:00Z","file_date_updated":"2020-07-14T12:44:59Z","publisher":"ACM","title":"Complete composition operators for IOCO-testing theory","abstract":[{"text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system.","lang":"eng"}],"publication_status":"published","ddc":["000"],"publication_identifier":{"isbn":["978-1-4503-3471-6"]},"status":"public","date_created":"2018-12-11T11:52:24Z","_id":"1502","type":"conference","ec_funded":1,"conference":{"start_date":"2015-05-04","end_date":"2015-05-08","location":"Montreal, QC, Canada","name":"CBSE: Component-Based Software Engineering "},"pubrep_id":"625","author":[{"full_name":"Beneš, Nikola","first_name":"Nikola","last_name":"Beneš"},{"full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","first_name":"Przemyslaw"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","last_name":"Kretinsky","first_name":"Jan","orcid":"0000-0002-8122-2881"},{"full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic"}],"quality_controlled":"1","project":[{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"oa_version":"Submitted Version","language":[{"iso":"eng"}],"month":"05","has_accepted_license":"1","file":[{"relation":"main_file","file_id":"5303","checksum":"c6ce681035c163a158751f240cb7d389","creator":"system","access_level":"open_access","file_size":467561,"content_type":"application/pdf","date_created":"2018-12-12T10:17:46Z","date_updated":"2020-07-14T12:44:59Z","file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf"}]},{"status":"public","year":"2015","page":"1582 - 1591","day":"14","doi":"10.1017/etds.2013.103","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1307.8414"}],"_id":"1503","type":"journal_article","date_created":"2018-12-11T11:52:24Z","oa":1,"publication":"Ergodic Theory and Dynamical Systems","intvolume":" 35","publist_id":"5675","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Sadel, Christian","id":"4760E9F8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8255-3968","first_name":"Christian","last_name":"Sadel"}],"oa_version":"Preprint","citation":{"short":"C. Sadel, Ergodic Theory and Dynamical Systems 35 (2015) 1582–1591.","mla":"Sadel, Christian. “A Herman-Avila-Bochi Formula for Higher-Dimensional Pseudo-Unitary and Hermitian-Symplectic-Cocycles.” Ergodic Theory and Dynamical Systems, vol. 35, no. 5, Cambridge University Press, 2015, pp. 1582–91, doi:10.1017/etds.2013.103.","ieee":"C. Sadel, “A Herman-Avila-Bochi formula for higher-dimensional pseudo-unitary and Hermitian-symplectic-cocycles,” Ergodic Theory and Dynamical Systems, vol. 35, no. 5. Cambridge University Press, pp. 1582–1591, 2015.","apa":"Sadel, C. (2015). A Herman-Avila-Bochi formula for higher-dimensional pseudo-unitary and Hermitian-symplectic-cocycles. Ergodic Theory and Dynamical Systems. Cambridge University Press. https://doi.org/10.1017/etds.2013.103","ama":"Sadel C. A Herman-Avila-Bochi formula for higher-dimensional pseudo-unitary and Hermitian-symplectic-cocycles. Ergodic Theory and Dynamical Systems. 2015;35(5):1582-1591. doi:10.1017/etds.2013.103","ista":"Sadel C. 2015. A Herman-Avila-Bochi formula for higher-dimensional pseudo-unitary and Hermitian-symplectic-cocycles. Ergodic Theory and Dynamical Systems. 35(5), 1582–1591.","chicago":"Sadel, Christian. “A Herman-Avila-Bochi Formula for Higher-Dimensional Pseudo-Unitary and Hermitian-Symplectic-Cocycles.” Ergodic Theory and Dynamical Systems. Cambridge University Press, 2015. https://doi.org/10.1017/etds.2013.103."},"date_updated":"2021-01-12T06:51:13Z","quality_controlled":"1","extern":"1","volume":35,"title":"A Herman-Avila-Bochi formula for higher-dimensional pseudo-unitary and Hermitian-symplectic-cocycles","language":[{"iso":"eng"}],"date_published":"2015-03-14T00:00:00Z","publisher":"Cambridge University Press","issue":"5","abstract":[{"text":"A Herman-Avila-Bochi type formula is obtained for the average sum of the top d Lyapunov exponents over a one-parameter family of double-struck G-cocycles, where double-struck G is the group that leaves a certain, non-degenerate Hermitian form of signature (c, d) invariant. The generic example of such a group is the pseudo-unitary group U(c, d) or, in the case c = d, the Hermitian-symplectic group HSp(2d) which naturally appears for cocycles related to Schrödinger operators. In the case d = 1, the formula for HSp(2d) cocycles reduces to the Herman-Avila-Bochi formula for SL(2, ℝ) cocycles.","lang":"eng"}],"month":"03","publication_status":"published"}]