[{"title":"Quantitative interprocedural analysis","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"first_name":"Yaron","full_name":"Velner, Yaron","last_name":"Velner"}],"publist_id":"5563","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . ACM, 2015. https://doi.org/10.1145/2676726.2676968.","apa":"Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2015). Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . Mumbai, India: ACM. https://doi.org/10.1145/2676726.2676968","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 2015;50(1):539-551. doi:10.1145/2676726.2676968","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT 50 (2015) 539–551.","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural analysis,” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1. ACM, pp. 539–551, 2015.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1, ACM, 2015, pp. 539–51, doi:10.1145/2676726.2676968."},"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.1145/2676726.2676968","date_published":"2015-01-01T00:00:00Z","date_created":"2018-12-11T11:52:59Z","page":"539 - 551","day":"01","publication":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT ","year":"2015","publisher":"ACM","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T12:01:59Z","status":"public","pubrep_id":"523","type":"journal_article","conference":{"name":"SIGPLAN: Symposium on Principles of Programming Languages","location":"Mumbai, India","end_date":"2015-01-17","start_date":"2015-01-15"},"_id":"1604","volume":50,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5445"},{"status":"public","id":"821","relation":"dissertation_contains"}]},"issue":"1","ec_funded":1,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publication_status":"published","month":"01","intvolume":" 50","scopus_import":1,"oa_version":"None","abstract":[{"lang":"eng","text":"We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs."}]},{"oa":1,"quality_controlled":"1","publisher":"Springer","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","date_created":"2018-12-11T11:52:59Z","doi":"10.1007/978-3-319-21690-4_9","date_published":"2015-07-16T00:00:00Z","page":"140 - 157","day":"16","year":"2015","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"title":"Faster algorithms for quantitative verification in constant treewidth graphs","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"publist_id":"5560","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. Vol. 9206, Springer, 2015, pp. 140–57, doi:10.1007/978-3-319-21690-4_9.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in constant treewidth graphs,” presented at the CAV: Computer Aided Verification, San Francisco, CA, USA, 2015, vol. 9206, pp. 140–157.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157. doi:10.1007/978-3-319-21690-4_9","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157). Presented at the CAV: Computer Aided Verification, San Francisco, CA, USA: Springer. https://doi.org/10.1007/978-3-319-21690-4_9","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,” 9206:140–57. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_9.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification, LNCS, vol. 9206, 140–157."},"intvolume":" 9206","month":"07","main_file_link":[{"url":"http://arxiv.org/abs/1504.07384","open_access":"1"}],"alternative_title":["LNCS"],"scopus_import":1,"oa_version":"Preprint","abstract":[{"text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.","lang":"eng"}],"ec_funded":1,"related_material":{"record":[{"id":"5430","status":"public","relation":"earlier_version"},{"relation":"earlier_version","status":"public","id":"5437"},{"id":"821","status":"public","relation":"dissertation_contains"}]},"volume":9206,"language":[{"iso":"eng"}],"publication_status":"published","status":"public","conference":{"end_date":"2015-07-24","location":"San Francisco, CA, USA","start_date":"2015-07-18","name":"CAV: Computer Aided Verification"},"type":"conference","_id":"1607","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T12:01:59Z"},{"article_processing_charge":"No","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kößler","full_name":"Kößler, Alexander","first_name":"Alexander"},{"first_name":"Ulrich","full_name":"Schmid, Ulrich","last_name":"Schmid"}],"publist_id":"5417","title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","citation":{"ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks,” in Real-Time Systems Symposium, Rome, Italy, 2015, vol. 2015, no. January, pp. 118–127.","short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, in:, Real-Time Systems Symposium, IEEE, 2015, pp. 118–127.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., & Schmid, U. (2015). A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In Real-Time Systems Symposium (Vol. 2015, pp. 118–127). Rome, Italy: IEEE. https://doi.org/10.1109/RTSS.2014.9","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In: Real-Time Systems Symposium. Vol 2015. IEEE; 2015:118-127. doi:10.1109/RTSS.2014.9","mla":"Chatterjee, Krishnendu, et al. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” Real-Time Systems Symposium, vol. 2015, no. January, IEEE, 2015, pp. 118–27, doi:10.1109/RTSS.2014.9.","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2015. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium vol. 2015, 118–127.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” In Real-Time Systems Symposium, 2015:118–27. IEEE, 2015. https://doi.org/10.1109/RTSS.2014.9."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"118 - 127","date_created":"2018-12-11T11:53:37Z","doi":"10.1109/RTSS.2014.9","date_published":"2015-01-15T00:00:00Z","year":"2015","publication":"Real-Time Systems Symposium","day":"15","publisher":"IEEE","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T12:01:59Z","conference":{"start_date":"2014-12-02","end_date":"2014-12-05","location":"Rome, Italy","name":"RTSS: Real-Time Systems Symposium"},"type":"conference","status":"public","_id":"1714","related_material":{"record":[{"relation":"earlier_version","id":"5423","status":"public"},{"relation":"dissertation_contains","id":"821","status":"public"}]},"volume":2015,"issue":"January","publication_status":"published","language":[{"iso":"eng"}],"scopus_import":1,"intvolume":" 2015","month":"01","abstract":[{"text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application.","lang":"eng"}],"oa_version":"None"},{"oa_version":"Published Version","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"}],"month":"07","oa":1,"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"language":[{"iso":"eng"}],"day":"11","file":[{"creator":"system","file_size":861396,"date_updated":"2020-07-14T12:46:56Z","file_name":"IST-2015-340-v1+1_main.pdf","date_created":"2018-12-12T11:54:09Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"5531","checksum":"df383dc62c94d7b2ea639aba088a76c6"}],"publication_status":"published","year":"2015","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"date_created":"2018-12-12T11:39:21Z","doi":"10.15479/AT:IST-2015-340-v1-1","related_material":{"record":[{"relation":"later_version","id":"1437","status":"public"},{"id":"5442","status":"public","relation":"earlier_version"},{"relation":"later_version","status":"public","id":"6009"}]},"date_published":"2015-07-11T00:00:00Z","page":"24","_id":"5441","pubrep_id":"340","status":"public","type":"technical_report","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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.","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.","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.","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","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.","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."},"date_updated":"2023-09-19T14:36:19Z","file_date_updated":"2020-07-14T12:46:56Z","department":[{"_id":"KrCh"}],"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}]},{"oa_version":"Preprint","abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study."}],"month":"04","publisher":"ACM","scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"oa":1,"day":"14","language":[{"iso":"eng"}],"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","publication_status":"published","year":"2015","related_material":{"record":[{"relation":"later_version","id":"1407","status":"public"}]},"date_published":"2015-04-14T00:00:00Z","doi":"10.1145/2728606.2728608","ec_funded":1,"date_created":"2018-12-11T11:53:29Z","page":"259 - 268","_id":"1689","status":"public","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"type":"conference","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","start_date":"2015-04-14","end_date":"2015-04-16","location":"Seattle, WA, United States"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–68, doi:10.1145/2728606.2728608.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–268.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 259–268.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., & Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728608"},"date_updated":"2023-09-20T09:43:09Z","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publist_id":"5456","author":[{"full_name":"Svoreňová, Mária","last_name":"Svoreňová","first_name":"Mária"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Cěrná","full_name":"Cěrná, Ivana","first_name":"Ivana"},{"first_name":"Cǎlin","last_name":"Belta","full_name":"Belta, Cǎlin"}]},{"title":"Evolution of decisions in population games with sequentially searching individuals","author":[{"full_name":"Priklopil, Tadeas","last_name":"Priklopil","first_name":"Tadeas","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"publist_id":"5467","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” Games, vol. 6, no. 4, MDPI, 2015, pp. 413–37, doi:10.3390/g6040413.","short":"T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.","ieee":"T. Priklopil and K. Chatterjee, “Evolution of decisions in population games with sequentially searching individuals,” Games, vol. 6, no. 4. MDPI, pp. 413–437, 2015.","ama":"Priklopil T, Chatterjee K. Evolution of decisions in population games with sequentially searching individuals. Games. 2015;6(4):413-437. doi:10.3390/g6040413","apa":"Priklopil, T., & Chatterjee, K. (2015). Evolution of decisions in population games with sequentially searching individuals. Games. MDPI. https://doi.org/10.3390/g6040413","chicago":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” Games. MDPI, 2015. https://doi.org/10.3390/g6040413.","ista":"Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games with sequentially searching individuals. Games. 6(4), 413–437."},"project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"doi":"10.3390/g6040413","date_published":"2015-09-29T00:00:00Z","date_created":"2018-12-11T11:53:26Z","page":"413 - 437","day":"29","publication":"Games","has_accepted_license":"1","year":"2015","quality_controlled":"1","publisher":"MDPI","oa":1,"department":[{"_id":"NiBa"},{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:12Z","ddc":["000"],"date_updated":"2023-10-17T11:42:52Z","status":"public","pubrep_id":"448","article_type":"original","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"_id":"1681","volume":6,"issue":"4","license":"https://creativecommons.org/licenses/by/4.0/","ec_funded":1,"file":[{"date_created":"2018-12-12T10:12:41Z","file_name":"IST-2016-448-v1+1_games-06-00413.pdf","date_updated":"2020-07-14T12:45:12Z","file_size":518832,"creator":"system","file_id":"4959","checksum":"912e1acbaf201100f447a43e4d5958bd","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["2073-4336"]},"publication_status":"published","month":"09","intvolume":" 6","scopus_import":"1","oa_version":"Published Version","abstract":[{"text":"In many social situations, individuals endeavor to find the single best possible partner, but are constrained to evaluate the candidates in sequence. Examples include the search for mates, economic partnerships, or any other long-term ties where the choice to interact involves two parties. Surprisingly, however, previous theoretical work on mutual choice problems focuses on finding equilibrium solutions, while ignoring the evolutionary dynamics of decisions. Empirically, this may be of high importance, as some equilibrium solutions can never be reached unless the population undergoes radical changes and a sufficient number of individuals change their decisions simultaneously. To address this question, we apply a mutual choice sequential search problem in an evolutionary game-theoretical model that allows one to find solutions that are favored by evolution. As an example, we study the influence of sequential search on the evolutionary dynamics of cooperation. For this, we focus on the classic snowdrift game and the prisoner’s dilemma game.","lang":"eng"}]},{"intvolume":" 9206","month":"07","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.02834"}],"scopus_import":1,"alternative_title":["LNCS"],"oa_version":"Preprint","abstract":[{"text":"For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour.","lang":"eng"}],"ec_funded":1,"related_material":{"record":[{"relation":"research_paper","status":"public","id":"5549"}]},"volume":9206,"language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"eisbn":["978-3-319-21690-4"]},"status":"public","conference":{"start_date":"2015-07-18","end_date":"2015-07-24","location":"San Francisco, CA, United States","name":"CAV: Computer Aided Verification"},"type":"conference","_id":"1603","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2024-02-21T13:52:07Z","oa":1,"publisher":"Springer","quality_controlled":"1","acknowledgement":"This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734.","date_created":"2018-12-11T11:52:58Z","date_published":"2015-07-16T00:00:00Z","doi":"10.1007/978-3-319-21690-4_10","page":"158 - 177","day":"16","year":"2015","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"title":"Counterexample explanation by learning small strategies in Markov decision processes","publist_id":"5564","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"full_name":"Fellner, Andreas","last_name":"Fellner","first_name":"Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. https://doi.org/10.1007/978-3-319-21690-4_10.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.","ama":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:10.1007/978-3-319-21690-4_10","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., & Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. https://doi.org/10.1007/978-3-319-21690-4_10","mla":"Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10."}},{"datarep_id":"28","file":[{"content_type":"application/zip","relation":"main_file","access_level":"open_access","checksum":"b8bcb43c0893023cda66c1b69c16ac62","file_id":"5597","file_size":49557109,"date_updated":"2020-07-14T12:47:00Z","creator":"system","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","date_created":"2018-12-12T13:02:31Z"}],"ec_funded":1,"license":"https://creativecommons.org/publicdomain/zero/1.0/","contributor":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Kretinsky"}],"related_material":{"record":[{"id":"1603","status":"public","relation":"popular_science"}]},"abstract":[{"text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication.","lang":"eng"}],"oa_version":"Published Version","month":"08","date_updated":"2024-02-21T13:52:07Z","ddc":["004"],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:47:00Z","_id":"5549","tmp":{"image":"/images/cc_0.png","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)","short":"CC0 (1.0)"},"type":"research_data","keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"status":"public","year":"2015","has_accepted_license":"1","day":"13","date_created":"2018-12-12T12:31:29Z","date_published":"2015-08-13T00:00:00Z","doi":"10.15479/AT:ISTA:28","oa":1,"publisher":"Institute of Science and Technology Austria","citation":{"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.","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.","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.","short":"A. Fellner, (2015).","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.","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","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"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","publist_id":"5564","author":[{"first_name":"Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","last_name":"Fellner","full_name":"Fellner, Andreas"}],"title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}]},{"conference":{"location":"San Diego, CA, United States","end_date":"2014-01-21","start_date":"2014-01-19","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation"},"type":"conference","status":"public","_id":"10884","department":[{"_id":"KrCh"}],"date_updated":"2022-05-17T08:36:01Z","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.1311.4425","open_access":"1"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 8318","month":"01","abstract":[{"lang":"eng","text":"We revisit the parameterized model checking problem for token-passing systems and specifications in indexed CTL ∗ \\X. Emerson and Namjoshi (1995, 2003) have shown that parameterized model checking of indexed CTL ∗ \\X in uni-directional token rings can be reduced to checking rings up to some cutoff size. Clarke et al. (2004) have shown a similar result for general topologies and indexed LTL \\X, provided processes cannot choose the directions for sending or receiving the token.\r\nWe unify and substantially extend these results by systematically exploring fragments of indexed CTL ∗ \\X with respect to general topologies. For each fragment we establish whether a cutoff exists, and for some concrete topologies, such as rings, cliques and stars, we infer small cutoffs. Finally, we show that the problem becomes undecidable, and thus no cutoffs exist, if processes are allowed to choose the directions in which they send or from which they receive the token."}],"oa_version":"Preprint","ec_funded":1,"volume":8318,"publication_status":"published","publication_identifier":{"eisbn":["9783642540134"],"eissn":["1611-3349"],"isbn":["9783642540127"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"article_processing_charge":"No","external_id":{"arxiv":["1311.4425"]},"author":[{"last_name":"Aminof","full_name":"Aminof, Benjamin","first_name":"Benjamin","id":"4A55BD00-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jacobs, Swen","last_name":"Jacobs","first_name":"Swen"},{"first_name":"Ayrat","full_name":"Khalimov, Ayrat","last_name":"Khalimov"},{"last_name":"Rubin","full_name":"Rubin, Sasha","first_name":"Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87"}],"title":"Parameterized model checking of token-passing systems","citation":{"apa":"Aminof, B., Jacobs, S., Khalimov, A., & Rubin, S. (2014). Parameterized model checking of token-passing systems. In Verification, Model Checking, and Abstract Interpretation (Vol. 8318, pp. 262–281). San Diego, CA, United States: Springer Nature. https://doi.org/10.1007/978-3-642-54013-4_15","ama":"Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized model checking of token-passing systems. In: Verification, Model Checking, and Abstract Interpretation. Vol 8318. Springer Nature; 2014:262-281. doi:10.1007/978-3-642-54013-4_15","ieee":"B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, “Parameterized model checking of token-passing systems,” in Verification, Model Checking, and Abstract Interpretation, San Diego, CA, United States, 2014, vol. 8318, pp. 262–281.","short":"B. Aminof, S. Jacobs, A. Khalimov, S. Rubin, in:, Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 262–281.","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Token-Passing Systems.” Verification, Model Checking, and Abstract Interpretation, vol. 8318, Springer Nature, 2014, pp. 262–81, doi:10.1007/978-3-642-54013-4_15.","ista":"Aminof B, Jacobs S, Khalimov A, Rubin S. 2014. Parameterized model checking of token-passing systems. Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 262–281.","chicago":"Aminof, Benjamin, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. “Parameterized Model Checking of Token-Passing Systems.” In Verification, Model Checking, and Abstract Interpretation, 8318:262–81. Springer Nature, 2014. https://doi.org/10.1007/978-3-642-54013-4_15."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"quality_controlled":"1","publisher":"Springer Nature","acknowledgement":"This work was supported by the Austrian Science Fund through grant P23499-N23\r\nand through the RiSE network (S11403, S11405, S11406, S11407-N23); ERC Starting Grant (279307: Graph Games); Vienna Science and Technology Fund (WWTF)\r\ngrants PROSEED, ICT12-059, and VRG11-005.","page":"262-281","date_created":"2022-03-18T13:01:22Z","date_published":"2014-01-30T00:00:00Z","doi":"10.1007/978-3-642-54013-4_15","year":"2014","publication":"Verification, Model Checking, and Abstract Interpretation","day":"30"},{"_id":"1375","status":"public","type":"journal_article","article_type":"original","date_updated":"2022-09-09T11:50:58Z","department":[{"_id":"KrCh"}],"oa_version":"Preprint","abstract":[{"text":"We consider directed graphs where each edge is labeled with an integer weight and study the fundamental algorithmic question of computing the value of a cycle with minimum mean weight. Our contributions are twofold: (1) First we show that the algorithmic question is reducible to the problem of a logarithmic number of min-plus matrix multiplications of n×n-matrices, where n is the number of vertices of the graph. (2) Second, when the weights are nonnegative, we present the first (1+ε)-approximation algorithm for the problem and the running time of our algorithm is Õ(nωlog3(nW/ε)/ε),1 where O(nω) is the time required for the classic n×n-matrix multiplication and W is the maximum value of the weights. With an additional O(log(nW/ε)) factor in space a cycle with approximately optimal weight can be computed within the same time bound.","lang":"eng"}],"month":"08","intvolume":" 547","scopus_import":"1","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1307.4473"}],"language":[{"iso":"eng"}],"publication_status":"published","issue":"C","volume":547,"ec_funded":1,"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. Approximating the minimum cycle mean. Theoretical Computer Science. 2014;547(C):104-116. doi:10.1016/j.tcs.2014.06.031","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., Loitzenbauer, V., & Raskin, M. (2014). Approximating the minimum cycle mean. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2014.06.031","short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, V. Loitzenbauer, M. Raskin, Theoretical Computer Science 547 (2014) 104–116.","ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, V. Loitzenbauer, and M. Raskin, “Approximating the minimum cycle mean,” Theoretical Computer Science, vol. 547, no. C. Elsevier, pp. 104–116, 2014.","mla":"Chatterjee, Krishnendu, et al. “Approximating the Minimum Cycle Mean.” Theoretical Computer Science, vol. 547, no. C, Elsevier, 2014, pp. 104–16, doi:10.1016/j.tcs.2014.06.031.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. 2014. Approximating the minimum cycle mean. Theoretical Computer Science. 547(C), 104–116.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, Veronika Loitzenbauer, and Michael Raskin. “Approximating the Minimum Cycle Mean.” Theoretical Computer Science. Elsevier, 2014. https://doi.org/10.1016/j.tcs.2014.06.031."},"title":"Approximating the minimum cycle mean","publist_id":"5836","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"},{"full_name":"Krinninger, Sebastian","last_name":"Krinninger","first_name":"Sebastian"},{"first_name":"Veronika","last_name":"Loitzenbauer","full_name":"Loitzenbauer, Veronika"},{"full_name":"Raskin, Michael","last_name":"Raskin","first_name":"Michael"}],"external_id":{"arxiv":["1307.4473"]},"article_processing_charge":"No","publisher":"Elsevier","quality_controlled":"1","oa":1,"day":"28","publication":"Theoretical Computer Science","year":"2014","doi":"10.1016/j.tcs.2014.06.031","date_published":"2014-08-28T00:00:00Z","date_created":"2018-12-11T11:51:40Z","page":"104 - 116"},{"title":"Game theoretic secure localization in wireless sensor networks","department":[{"_id":"KrCh"}],"author":[{"first_name":"Susmit","full_name":"Jha, Susmit","last_name":"Jha"},{"first_name":"Stavros","last_name":"Tripakis","full_name":"Tripakis, Stavros"},{"first_name":"Sanjit","full_name":"Seshia, Sanjit","last_name":"Seshia"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5247","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Jha S, Tripakis S, Seshia S, Chatterjee K. 2014. Game theoretic secure localization in wireless sensor networks. IOT: Internet of Things, 85–90.","chicago":"Jha, Susmit, Stavros Tripakis, Sanjit Seshia, and Krishnendu Chatterjee. “Game Theoretic Secure Localization in Wireless Sensor Networks,” 85–90. IEEE, 2014. https://doi.org/10.1109/IOT.2014.7030120.","ieee":"S. Jha, S. Tripakis, S. Seshia, and K. Chatterjee, “Game theoretic secure localization in wireless sensor networks,” presented at the IOT: Internet of Things, Cambridge, USA, 2014, pp. 85–90.","short":"S. Jha, S. Tripakis, S. Seshia, K. Chatterjee, in:, IEEE, 2014, pp. 85–90.","apa":"Jha, S., Tripakis, S., Seshia, S., & Chatterjee, K. (2014). Game theoretic secure localization in wireless sensor networks (pp. 85–90). Presented at the IOT: Internet of Things, Cambridge, USA: IEEE. https://doi.org/10.1109/IOT.2014.7030120","ama":"Jha S, Tripakis S, Seshia S, Chatterjee K. Game theoretic secure localization in wireless sensor networks. In: IEEE; 2014:85-90. doi:10.1109/IOT.2014.7030120","mla":"Jha, Susmit, et al. Game Theoretic Secure Localization in Wireless Sensor Networks. IEEE, 2014, pp. 85–90, doi:10.1109/IOT.2014.7030120."},"date_updated":"2021-01-12T06:53:38Z","status":"public","type":"conference","conference":{"name":"IOT: Internet of Things","location":"Cambridge, USA","end_date":"2014-10-08","start_date":"2014-10-06"},"_id":"1853","doi":"10.1109/IOT.2014.7030120","date_published":"2014-02-03T00:00:00Z","date_created":"2018-12-11T11:54:22Z","page":"85 - 90","day":"03","language":[{"iso":"eng"}],"publication_status":"published","year":"2014","month":"02","publisher":"IEEE","quality_controlled":"1","oa_version":"None","abstract":[{"lang":"eng","text":"Wireless sensor networks (WSNs) composed of low-power, low-cost sensor nodes are expected to form the backbone of future intelligent networks for a broad range of civil, industrial and military applications. These sensor nodes are often deployed through random spreading, and function in dynamic environments. Many applications of WSNs such as pollution tracking, forest fire detection, and military surveillance require knowledge of the location of constituent nodes. But the use of technologies such as GPS on all nodes is prohibitive due to power and cost constraints. So, the sensor nodes need to autonomously determine their locations. Most localization techniques use anchor nodes with known locations to determine the position of remaining nodes. Localization techniques have two conflicting requirements. On one hand, an ideal localization technique should be computationally simple and on the other hand, it must be resistant to attacks that compromise anchor nodes. In this paper, we propose a computationally light-weight game theoretic secure localization technique and demonstrate its effectiveness in comparison to existing techniques."}]},{"_id":"1884","type":"journal_article","status":"public","citation":{"chicago":"Landau, Dan, Chip Stewart, Johannes Reiter, Michael Lawrence, Carrie Sougnez, Jennifer Brown, Armando Lopez Guillermo, et al. “Novel Putative Driver Gene Mutations in Chronic Lymphocytic Leukemia (CLL): Results from a Combined Analysis of Whole Exome Sequencing of 262 Primary CLL Aamples.” Blood. American Society of Hematology, 2014.","ista":"Landau D, Stewart C, Reiter J, Lawrence M, Sougnez C, Brown J, Lopez Guillermo A, Gabriel S, Lander E, Neuberg D, López Otín C, Campo E, Getz G, Wu C. 2014. Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. Blood. 124(21), 1952–1952.","mla":"Landau, Dan, et al. “Novel Putative Driver Gene Mutations in Chronic Lymphocytic Leukemia (CLL): Results from a Combined Analysis of Whole Exome Sequencing of 262 Primary CLL Aamples.” Blood, vol. 124, no. 21, American Society of Hematology, 2014, pp. 1952–1952.","ieee":"D. Landau et al., “Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples,” Blood, vol. 124, no. 21. American Society of Hematology, pp. 1952–1952, 2014.","short":"D. Landau, C. Stewart, J. Reiter, M. Lawrence, C. Sougnez, J. Brown, A. Lopez Guillermo, S. Gabriel, E. Lander, D. Neuberg, C. López Otín, E. Campo, G. Getz, C. Wu, Blood 124 (2014) 1952–1952.","ama":"Landau D, Stewart C, Reiter J, et al. Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. Blood. 2014;124(21):1952-1952.","apa":"Landau, D., Stewart, C., Reiter, J., Lawrence, M., Sougnez, C., Brown, J., … Wu, C. (2014). Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. Blood. American Society of Hematology."},"date_updated":"2021-01-12T06:53:50Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publist_id":"5211","author":[{"first_name":"Dan","full_name":"Landau, Dan","last_name":"Landau"},{"first_name":"Chip","last_name":"Stewart","full_name":"Stewart, Chip"},{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","first_name":"Johannes","last_name":"Reiter","orcid":"0000-0002-0170-7353","full_name":"Reiter, Johannes"},{"full_name":"Lawrence, Michael","last_name":"Lawrence","first_name":"Michael"},{"full_name":"Sougnez, Carrie","last_name":"Sougnez","first_name":"Carrie"},{"first_name":"Jennifer","full_name":"Brown, Jennifer","last_name":"Brown"},{"full_name":"Lopez Guillermo, Armando","last_name":"Lopez Guillermo","first_name":"Armando"},{"last_name":"Gabriel","full_name":"Gabriel, Stacey","first_name":"Stacey"},{"last_name":"Lander","full_name":"Lander, Eric","first_name":"Eric"},{"last_name":"Neuberg","full_name":"Neuberg, Donna","first_name":"Donna"},{"last_name":"López Otín","full_name":"López Otín, Carlos","first_name":"Carlos"},{"first_name":"Elias","full_name":"Campo, Elias","last_name":"Campo"},{"last_name":"Getz","full_name":"Getz, Gad","first_name":"Gad"},{"first_name":"Catherine","full_name":"Wu, Catherine","last_name":"Wu"}],"department":[{"_id":"KrCh"}],"title":"Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples","abstract":[{"text":"Unbiased high-throughput massively parallel sequencing methods have transformed the process of discovery of novel putative driver gene mutations in cancer. In chronic lymphocytic leukemia (CLL), these methods have yielded several unexpected findings, including the driver genes SF3B1, NOTCH1 and POT1. Recent analysis, utilizing down-sampling of existing datasets, has shown that the discovery process of putative drivers is far from complete across cancer. In CLL, while driver gene mutations affecting >10% of patients were efficiently discovered with previously published CLL cohorts of up to 160 samples subjected to whole exome sequencing (WES), this sample size has only 0.78 power to detect drivers affecting 5% of patients, and only 0.12 power for drivers affecting 2% of patients. These calculations emphasize the need to apply unbiased WES to larger patient cohorts.","lang":"eng"}],"oa_version":"None","publisher":"American Society of Hematology","main_file_link":[{"url":"http://www.bloodjournal.org/content/124/21/1952?sso-checked=true"}],"month":"12","intvolume":" 124","year":"2014","publication_status":"published","day":"04","publication":"Blood","language":[{"iso":"eng"}],"page":"1952 - 1952","volume":124,"issue":"21","date_published":"2014-12-04T00:00:00Z","date_created":"2018-12-11T11:54:32Z"},{"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:98–114. Society of Industrial and Applied Mathematics, 2014. https://doi.org/10.1007/978-3-319-11936-6_8.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014, pp. 98–114.","ieee":"T. Brázdil et al., “Verification of markov decision processes using learning algorithms,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 98–114.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of markov decision processes using learning algorithms. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 98–114). Sydney, Australia: Society of Industrial and Applied Mathematics. https://doi.org/10.1007/978-3-319-11936-6_8","ama":"Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision processes using learning algorithms. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Society of Industrial and Applied Mathematics; 2014:98-114. doi:10.1007/978-3-319-11936-6_8","mla":"Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Society of Industrial and Applied Mathematics, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8."},"title":"Verification of markov decision processes using learning algorithms","editor":[{"first_name":"Franck","full_name":"Cassez, Franck","last_name":"Cassez"},{"full_name":"Raskin, Jean-François","last_name":"Raskin","first_name":"Jean-François"}],"publist_id":"5046","author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"first_name":"Marta","full_name":"Kwiatkowska, Marta","last_name":"Kwiatkowska"},{"first_name":"David","last_name":"Parker","full_name":"Parker, David"},{"first_name":"Mateusz","last_name":"Ujma","full_name":"Ujma, Mateusz"}],"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"26241A12-B435-11E9-9278-68D0E5697425","name":"LIGHT-REGULATED LIGAND TRAPS FOR SPATIO-TEMPORAL INHIBITION OF CELL SIGNALING","grant_number":"24696"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publication":" Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","day":"01","year":"2014","date_created":"2018-12-11T11:55:17Z","doi":"10.1007/978-3-319-11936-6_8","date_published":"2014-11-01T00:00:00Z","page":"98 - 114","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1.","oa":1,"quality_controlled":"1","publisher":"Society of Industrial and Applied Mathematics","date_updated":"2021-01-12T06:54:49Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"_id":"2027","status":"public","conference":{"name":"ALENEX: Algorithm Engineering and Experiments","start_date":"2014-11-03","end_date":"2014-11-07","location":"Sydney, Australia"},"type":"conference","language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"volume":8837,"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples."}],"intvolume":" 8837","month":"11","main_file_link":[{"url":"http://arxiv.org/abs/1402.2967","open_access":"1"}],"alternative_title":["LNCS"]},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_updated":"2021-01-12T06:55:00Z","conference":{"start_date":"2014-09-02","location":"Rome, Italy","end_date":"2014-09-05","name":"CONCUR: Concurrency Theory"},"type":"conference","status":"public","_id":"2053","ec_funded":1,"volume":8704,"publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"url":"http://arxiv.org/abs/1404.5084","open_access":"1"}],"alternative_title":["LNCS"],"intvolume":" 8704","month":"09","abstract":[{"lang":"eng","text":"In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems."}],"oa_version":"Submitted Version","publist_id":"4993","author":[{"first_name":"Holger","full_name":"Hermanns, Holger","last_name":"Hermanns"},{"first_name":"Jan","last_name":"Krčál","full_name":"Krčál, Jan"},{"first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan"}],"editor":[{"first_name":"Paolo","full_name":"Baldan, Paolo","last_name":"Baldan"},{"last_name":"Gorla","full_name":"Gorla, Daniele","first_name":"Daniele"}],"title":"Probabilistic bisimulation: Naturally on distributions","citation":{"mla":"Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:10.1007/978-3-662-44584-6_18.","short":"H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–265.","ieee":"H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 249–265.","ama":"Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on distributions. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:249-265. doi:10.1007/978-3-662-44584-6_18","apa":"Hermanns, H., Krčál, J., & Kretinsky, J. (2014). Probabilistic bisimulation: Naturally on distributions. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 249–265). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_18","chicago":"Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation: Naturally on Distributions.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_18.","ista":"Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265."},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"page":"249 - 265","date_created":"2018-12-11T11:55:27Z","doi":"10.1007/978-3-662-44584-6_18","date_published":"2014-09-01T00:00:00Z","year":"2014","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","day":"01","oa":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","acknowledgement":"This work is supported by the EU 7th Framework Programme under grant agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative Research Teams."},{"date_published":"2014-09-01T00:00:00Z","doi":"10.1007/978-3-662-44584-6_9","volume":8704,"date_created":"2018-12-11T11:55:26Z","page":"109 - 124","day":"01","language":[{"iso":"eng"}],"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","year":"2014","publication_status":"published","month":"09","intvolume":" 8704","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LNCS"],"oa_version":"None","acknowledgement":"The second, third, fourth and fifth authors were supported by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grants PROSEED, ICT12-059, and VRG11-005.","abstract":[{"lang":"eng","text":"A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finite-state systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Büchi word automaton), and establish tight bounds on the sizes of such automata."}],"editor":[{"last_name":"Baldan","full_name":"Baldan, Paolo","first_name":"Paolo"},{"first_name":"Daniele","last_name":"Gorla","full_name":"Gorla, Daniele"}],"title":"Parameterized model checking of rendezvous systems","department":[{"_id":"KrCh"}],"publist_id":"4994","author":[{"last_name":"Aminof","full_name":"Aminof, Benjamin","first_name":"Benjamin","id":"4A55BD00-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kotek, Tomer","last_name":"Kotek","first_name":"Tomer"},{"last_name":"Rubin","full_name":"Rubin, Sacha","first_name":"Sacha"},{"first_name":"Francesco","full_name":"Spegni, Francesco","last_name":"Spegni"},{"last_name":"Veith","full_name":"Veith, Helmut","first_name":"Helmut"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:54:59Z","citation":{"ista":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H. 2014. Parameterized model checking of rendezvous systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 109–124.","chicago":"Aminof, Benjamin, Tomer Kotek, Sacha Rubin, Francesco Spegni, and Helmut Veith. “Parameterized Model Checking of Rendezvous Systems.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:109–24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_9.","ieee":"B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith, “Parameterized model checking of rendezvous systems,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 109–124.","short":"B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 109–124.","apa":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2014). Parameterized model checking of rendezvous systems. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 109–124). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_9","ama":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H. Parameterized model checking of rendezvous systems. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:109-124. doi:10.1007/978-3-662-44584-6_9","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Rendezvous Systems.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 109–24, doi:10.1007/978-3-662-44584-6_9."},"status":"public","type":"conference","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2014-09-02","end_date":"2014-09-05","location":"Rome, Italy"},"_id":"2052"},{"file_date_updated":"2020-07-14T12:45:31Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ddc":["621"],"date_updated":"2021-01-12T06:55:51Z","pubrep_id":"71","status":"public","article_type":"original","type":"journal_article","_id":"2187","ec_funded":1,"volume":51,"issue":"3-4","language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T10:16:44Z","file_name":"IST-2012-71-v1+1_Synthesizing_robust_systems.pdf","creator":"system","date_updated":"2020-07-14T12:45:31Z","file_size":169523,"checksum":"d7f560f3d923f0f00aa10a0652f83273","file_id":"5234","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"publication_status":"published","intvolume":" 51","month":"06","scopus_import":1,"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if assumptions in the specification are violated. To overcome this, we define two robustness notions, combine them, and show how to enforce them in synthesis. The first notion applies to safety properties: If safety assumptions are violated temporarily, we require that the system recovers to normal operation with as few errors as possible. The second notion requires that, if liveness assumptions are violated, as many guarantees as possible should be fulfilled nevertheless. We present a synthesis procedure achieving this for the important class of GR(1) specifications, and establish complexity bounds. We also present an implementation of a special case of robustness, and show experimental results."}],"title":"Synthesizing robust systems","article_processing_charge":"No","author":[{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Greimel","full_name":"Greimel, Karin","first_name":"Karin"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Hofferek","full_name":"Hofferek, Georg","first_name":"Georg"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"},{"first_name":"Bettina","full_name":"Könighofer, Bettina","last_name":"Könighofer"},{"first_name":"Robert","last_name":"Könighofer","full_name":"Könighofer, Robert"}],"publist_id":"4787","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, Könighofer B, Könighofer R. 2014. Synthesizing robust systems. Acta Informatica. 51(3–4), 193–220.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer. “Synthesizing Robust Systems.” Acta Informatica. Springer, 2014. https://doi.org/10.1007/s00236-013-0191-5.","ama":"Bloem R, Chatterjee K, Greimel K, et al. Synthesizing robust systems. Acta Informatica. 2014;51(3-4):193-220. doi:10.1007/s00236-013-0191-5","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., Hofferek, G., Jobstmann, B., … Könighofer, R. (2014). Synthesizing robust systems. Acta Informatica. Springer. https://doi.org/10.1007/s00236-013-0191-5","ieee":"R. Bloem et al., “Synthesizing robust systems,” Acta Informatica, vol. 51, no. 3–4. Springer, pp. 193–220, 2014.","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, G. Hofferek, B. Jobstmann, B. Könighofer, R. Könighofer, Acta Informatica 51 (2014) 193–220.","mla":"Bloem, Roderick, et al. “Synthesizing Robust Systems.” Acta Informatica, vol. 51, no. 3–4, Springer, 2014, pp. 193–220, doi:10.1007/s00236-013-0191-5."},"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"date_created":"2018-12-11T11:56:13Z","date_published":"2014-06-01T00:00:00Z","doi":"10.1007/s00236-013-0191-5","page":"193 - 220","publication":"Acta Informatica","day":"01","year":"2014","has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Springer"},{"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Esparza, Javier, and Jan Kretinsky. “From LTL to Deterministic Automata: A Safraless Compositional Approach,” 8559:192–208. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_13.","ista":"Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.","mla":"Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata: A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208, doi:10.1007/978-3-319-08867-9_13.","ieee":"J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208.","short":"J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208.","apa":"Esparza, J., & Kretinsky, J. (2014). From LTL to deterministic automata: A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-319-08867-9_13","ama":"Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional approach. In: Vol 8559. Springer; 2014:192-208. doi:10.1007/978-3-319-08867-9_13"},"title":"From LTL to deterministic automata: A safraless compositional approach","author":[{"last_name":"Esparza","full_name":"Esparza, Javier","first_name":"Javier"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"4784","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"day":"01","year":"2014","date_published":"2014-01-01T00:00:00Z","doi":"10.1007/978-3-319-08867-9_13","date_created":"2018-12-11T11:56:14Z","page":"192 - 208","acknowledgement":"The author is on leave from Faculty of Informatics, Masaryk University, Czech Republic, and partially supported by the Czech Science Foundation, grant No. P202/12/G061.","quality_controlled":"1","publisher":"Springer","oa":1,"date_updated":"2021-01-12T06:55:53Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"_id":"2190","status":"public","type":"conference","conference":{"name":"CAV: Computer Aided Verification"},"language":[{"iso":"eng"}],"publication_status":"published","volume":8559,"ec_funded":1,"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods."}],"month":"01","intvolume":" 8559","alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1402.3388"}]},{"ddc":["000"],"date_updated":"2021-01-12T06:56:11Z","file_date_updated":"2020-07-14T12:45:34Z","department":[{"_id":"KrCh"}],"_id":"2234","pubrep_id":"428","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","language":[{"iso":"eng"}],"file":[{"date_updated":"2020-07-14T12:45:34Z","file_size":375388,"creator":"system","date_created":"2018-12-12T10:07:57Z","file_name":"IST-2016-428-v1+1_1104.3489.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"803edcc2d8c1acfba44a9ec43a5eb9f0","file_id":"4656"}],"publication_status":"published","publication_identifier":{"issn":["18605974"]},"ec_funded":1,"issue":"1","volume":10,"oa_version":"Published Version","abstract":[{"text":"We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with κ limit-average functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the case of one limit-average function, both randomization and memory are necessary for strategies even for ε-approximation, and that finite-memory randomized strategies are sufficient for achieving Pareto optimal values. Under the satisfaction objective, in contrast to the case of one limit-average function, infinite memory is necessary for strategies achieving a specific value (i.e. randomized finite-memory strategies are not sufficient), whereas memoryless randomized strategies are sufficient for ε-approximation, for all ε > 0. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be ε-approximated in time polynomial in the size of the MDP and 1/ε, and exponential in the number of limit-average functions, for all ε > 0. Our analysis also reveals flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, corrects the flaws, and allows us to obtain improved results.","lang":"eng"}],"intvolume":" 10","month":"02","main_file_link":[{"url":"http://repository.ist.ac.at/id/eprint/428","open_access":"1"}],"scopus_import":1,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Brázdil, Tomáš, et al. “Markov Decision Processes with Multiple Long-Run Average Objectives.” Logical Methods in Computer Science, vol. 10, no. 1, International Federation of Computational Logic, 2014, doi:10.2168/LMCS-10(1:13)2014.","ama":"Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science. 2014;10(1). doi:10.2168/LMCS-10(1:13)2014","apa":"Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., & Kučera, A. (2014). Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-10(1:13)2014","short":"T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, Logical Methods in Computer Science 10 (2014).","ieee":"T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera, “Markov decision processes with multiple long-run average objectives,” Logical Methods in Computer Science, vol. 10, no. 1. International Federation of Computational Logic, 2014.","chicago":"Brázdil, Tomáš, Václav Brožek, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Markov Decision Processes with Multiple Long-Run Average Objectives.” Logical Methods in Computer Science. International Federation of Computational Logic, 2014. https://doi.org/10.2168/LMCS-10(1:13)2014.","ista":"Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. 2014. Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science. 10(1)."},"title":"Markov decision processes with multiple long-run average objectives","author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"last_name":"Brožek","full_name":"Brožek, Václav","first_name":"Václav"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Vojtěch","full_name":"Forejt, Vojtěch","last_name":"Forejt"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"}],"publist_id":"4727","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publication":"Logical Methods in Computer Science","day":"14","year":"2014","has_accepted_license":"1","date_created":"2018-12-11T11:56:29Z","date_published":"2014-02-14T00:00:00Z","doi":"10.2168/LMCS-10(1:13)2014","oa":1,"quality_controlled":"1","publisher":"International Federation of Computational Logic"},{"scopus_import":1,"quality_controlled":"1","publisher":"Elsevier","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1303.3777"}],"oa":1,"month":"02","intvolume":" 521","abstract":[{"text":"Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different classes and representations of Muller games lead to problems of varying computational complexity. One such class are parity games; these are of particular significance in computational complexity, as they remain one of the few combinatorial problems known to be in NP ∩ co-NP but not known to be in P. We show that winning regions for a Muller game can be determined from the alternating structure of its traps. To every Muller game we then associate a natural number that we call its trap depth; this parameter measures how complicated the trap structure is. We present algorithms for parity games that run in polynomial time for graphs of bounded trap depth, and in general run in time exponential in the trap depth. ","lang":"eng"}],"oa_version":"Submitted Version","page":"73 - 91","doi":"10.1016/j.tcs.2013.11.032","volume":521,"date_published":"2014-02-13T00:00:00Z","date_created":"2018-12-11T11:56:33Z","publication_identifier":{"issn":["03043975"]},"year":"2014","publication_status":"published","day":"13","language":[{"iso":"eng"}],"publication":"Theoretical Computer Science","type":"journal_article","status":"public","_id":"2246","author":[{"last_name":"Grinshpun","full_name":"Grinshpun, Andrey","first_name":"Andrey"},{"first_name":"Pakawat","full_name":"Phalitnonkiat, Pakawat","last_name":"Phalitnonkiat"},{"full_name":"Rubin, Sasha","last_name":"Rubin","first_name":"Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andrei","full_name":"Tarfulea, Andrei","last_name":"Tarfulea"}],"publist_id":"4703","department":[{"_id":"KrCh"}],"title":"Alternating traps in Muller and parity games","citation":{"short":"A. Grinshpun, P. Phalitnonkiat, S. Rubin, A. Tarfulea, Theoretical Computer Science 521 (2014) 73–91.","ieee":"A. Grinshpun, P. Phalitnonkiat, S. Rubin, and A. Tarfulea, “Alternating traps in Muller and parity games,” Theoretical Computer Science, vol. 521. Elsevier, pp. 73–91, 2014.","apa":"Grinshpun, A., Phalitnonkiat, P., Rubin, S., & Tarfulea, A. (2014). Alternating traps in Muller and parity games. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2013.11.032","ama":"Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. Alternating traps in Muller and parity games. Theoretical Computer Science. 2014;521:73-91. doi:10.1016/j.tcs.2013.11.032","mla":"Grinshpun, Andrey, et al. “Alternating Traps in Muller and Parity Games.” Theoretical Computer Science, vol. 521, Elsevier, 2014, pp. 73–91, doi:10.1016/j.tcs.2013.11.032.","ista":"Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. 2014. Alternating traps in Muller and parity games. Theoretical Computer Science. 521, 73–91.","chicago":"Grinshpun, Andrey, Pakawat Phalitnonkiat, Sasha Rubin, and Andrei Tarfulea. “Alternating Traps in Muller and Parity Games.” Theoretical Computer Science. Elsevier, 2014. https://doi.org/10.1016/j.tcs.2013.11.032."},"date_updated":"2021-01-12T06:56:16Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87"},{"department":[{"_id":"KrCh"}],"date_updated":"2023-02-21T16:06:56Z","article_type":"original","type":"journal_article","status":"public","_id":"2716","issue":"3-4","related_material":{"record":[{"status":"public","id":"10904","relation":"earlier_version"}]},"volume":51,"publication_status":"published","language":[{"iso":"eng"}],"scopus_import":"1","main_file_link":[{"url":"http://arxiv.org/abs/1201.5073","open_access":"1"}],"month":"06","intvolume":" 51","abstract":[{"text":"Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω ω -regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on vector addition systems with states. Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.","lang":"eng"}],"oa_version":"Preprint","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mickael","full_name":"Randour, Mickael","last_name":"Randour"},{"first_name":"Jean","last_name":"Raskin","full_name":"Raskin, Jean"}],"publist_id":"4176","article_processing_charge":"No","external_id":{"arxiv":["1201.5073"]},"title":"Strategy synthesis for multi-dimensional quantitative objectives","citation":{"ista":"Chatterjee K, Randour M, Raskin J. 2014. Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. 51(3–4), 129–163.","chicago":"Chatterjee, Krishnendu, Mickael Randour, and Jean Raskin. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” Acta Informatica. Springer, 2014. https://doi.org/10.1007/s00236-013-0182-6.","apa":"Chatterjee, K., Randour, M., & Raskin, J. (2014). Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. Springer. https://doi.org/10.1007/s00236-013-0182-6","ama":"Chatterjee K, Randour M, Raskin J. Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. 2014;51(3-4):129-163. doi:10.1007/s00236-013-0182-6","ieee":"K. Chatterjee, M. Randour, and J. Raskin, “Strategy synthesis for multi-dimensional quantitative objectives,” Acta Informatica, vol. 51, no. 3–4. Springer, pp. 129–163, 2014.","short":"K. Chatterjee, M. Randour, J. Raskin, Acta Informatica 51 (2014) 129–163.","mla":"Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” Acta Informatica, vol. 51, no. 3–4, Springer, 2014, pp. 129–63, doi:10.1007/s00236-013-0182-6."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"}],"page":"129 - 163","date_published":"2014-06-01T00:00:00Z","doi":"10.1007/s00236-013-0182-6","date_created":"2018-12-11T11:59:14Z","year":"2014","day":"01","publication":"Acta Informatica","publisher":"Springer","quality_controlled":"1","oa":1,"acknowledgement":"Krishnendu Chatterjee is supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407 (RiSE), ERC Starting Grant (279307: Graph Games) and Microsoft faculty fellowship. Mickael Randour is supported by F.R.S.-FNRS. fellowship. \r\nJean-François Raskin is supported by ERC Starting Grant (279499: inVEST).Thanks to D. Sbabo for useful pointers, V. Bruyère for comments on a preliminary draft, and A. Bohy for fruitful discussions about the Acacia+ tool. We are grateful to the anonymous reviewers for their insightful comments. "},{"_id":"1733","status":"public","type":"journal_article","date_updated":"2023-02-23T11:04:00Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies."}],"intvolume":" 560","month":"12","main_file_link":[{"url":"http://arxiv.org/abs/1210.2450","open_access":"1"}],"scopus_import":1,"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"2916"}]},"volume":560,"issue":"3","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” Theoretical Computer Science. Elsevier, 2014. https://doi.org/10.1016/j.tcs.2014.08.019.","ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363.","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” Theoretical Computer Science, vol. 560, no. 3, Elsevier, 2014, pp. 348–63, doi:10.1016/j.tcs.2014.08.019.","ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface simulation distances,” Theoretical Computer Science, vol. 560, no. 3. Elsevier, pp. 348–363, 2014.","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface simulation distances. Theoretical Computer Science. 2014;560(3):348-363. doi:10.1016/j.tcs.2014.08.019","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., & Radhakrishna, A. (2014). Interface simulation distances. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2014.08.019"},"title":"Interface simulation distances","author":[{"full_name":"Cerny, Pavol","last_name":"Cerny","first_name":"Pavol"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna"}],"publist_id":"5392","oa":1,"publisher":"Elsevier","quality_controlled":"1","publication":"Theoretical Computer Science","day":"04","year":"2014","date_created":"2018-12-11T11:53:43Z","doi":"10.1016/j.tcs.2014.08.019","date_published":"2014-12-04T00:00:00Z","page":"348 - 363"},{"abstract":[{"text":"The computation of the winning set for Büchi objectives in alternating games on graphs is a central problem in computer-aided verification with a large number of applications. The long-standing best known upper bound for solving the problem is Õ(n ⋅ m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the Õ(n ⋅ m) boundary by presenting a new technique that reduces the running time to O(n2). This bound also leads to O(n2)-time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of Õ(n ⋅ m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n3)), and (3) in Markov decision processes (improving for m>n4/3 an earlier bound of O(m ⋅ √m)). We then show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. Our algorithms are the first dynamic algorithms for this problem. We then consider another core graph theoretic problem in verification of probabilistic systems, namely computing the maximal end-component decomposition of a graph. We present two improved static algorithms for the maximal end-component decomposition problem. Our first algorithm is an O(m ⋅ √m)-time algorithm, and our second algorithm is an O(n2)-time algorithm which is obtained using the same technique as for alternating Büchi games. Thus, we obtain an O(min &lcu;m ⋅ √m,n2})-time algorithm improving the long-standing O(n ⋅ m) time bound. Finally, we show how to maintain the maximal end-component decomposition of a graph under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per edge deletion, and O(m) worst-case time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem.","lang":"eng"}],"oa_version":"Submitted Version","main_file_link":[{"open_access":"1","url":"https://eprints.cs.univie.ac.at/3933/"}],"scopus_import":"1","intvolume":" 61","month":"05","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"3165","status":"public"}]},"issue":"3","volume":61,"_id":"2141","type":"journal_article","status":"public","date_updated":"2023-02-23T11:15:12Z","department":[{"_id":"KrCh"}],"oa":1,"publisher":"ACM","quality_controlled":"1","year":"2014","publication":"Journal of the ACM","day":"01","date_created":"2018-12-11T11:55:57Z","date_published":"2014-05-01T00:00:00Z","doi":"10.1145/2597631","article_number":"a15","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"citation":{"mla":"Chatterjee, Krishnendu, and Monika H. Henzinger. “Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition.” Journal of the ACM, vol. 61, no. 3, a15, ACM, 2014, doi:10.1145/2597631.","ama":"Chatterjee K, Henzinger MH. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. Journal of the ACM. 2014;61(3). doi:10.1145/2597631","apa":"Chatterjee, K., & Henzinger, M. H. (2014). Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. Journal of the ACM. ACM. https://doi.org/10.1145/2597631","ieee":"K. Chatterjee and M. H. Henzinger, “Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition,” Journal of the ACM, vol. 61, no. 3. ACM, 2014.","short":"K. Chatterjee, M.H. Henzinger, Journal of the ACM 61 (2014).","chicago":"Chatterjee, Krishnendu, and Monika H Henzinger. “Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition.” Journal of the ACM. ACM, 2014. https://doi.org/10.1145/2597631.","ista":"Chatterjee K, Henzinger MH. 2014. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. Journal of the ACM. 61(3), a15."},"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","article_processing_charge":"No","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","last_name":"Henzinger","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"}],"publist_id":"4883","title":"Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition"},{"_id":"2054","type":"conference","conference":{"start_date":"2014-09-02","end_date":"2014-09-05","location":"Rome, Italy","name":"CONCUR: Concurrency Theory"},"status":"public","date_updated":"2023-02-23T11:23:36Z","department":[{"_id":"KrCh"}],"abstract":[{"lang":"eng","text":"We study two-player concurrent games on finite-state graphs played for an infinite number of rounds, where in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. The objectives are ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). While the qualitative analysis problem for concurrent parity games with infinite-memory, infinite-precision randomized strategies was studied before, we study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision, or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory, or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in (n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. Our symbolic algorithms are based on a characterization of the winning sets as μ-calculus formulas, however, our μ-calculus formulas are crucially different from the ones for concurrent parity games (without bounded rationality); and our memoryless witness strategy constructions are significantly different from the infinite-memory witness strategy constructions for concurrent parity games."}],"oa_version":"None","alternative_title":["LNCS"],"month":"09","intvolume":" 8704","publication_status":"published","language":[{"iso":"eng"}],"volume":8704,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"3354"}]},"ec_funded":1,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"citation":{"ista":"Chatterjee K. 2014. Qualitative concurrent parity games: Bounded rationality. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 544–559.","chicago":"Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:544–59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_37.","short":"K. Chatterjee, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 544–559.","ieee":"K. Chatterjee, “Qualitative concurrent parity games: Bounded rationality,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 544–559.","apa":"Chatterjee, K. (2014). Qualitative concurrent parity games: Bounded rationality. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 544–559). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_37","ama":"Chatterjee K. Qualitative concurrent parity games: Bounded rationality. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:544-559. doi:10.1007/978-3-662-44584-6_37","mla":"Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 544–59, doi:10.1007/978-3-662-44584-6_37."},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publist_id":"4992","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"title":"Qualitative concurrent parity games: Bounded rationality","editor":[{"first_name":"Paolo","full_name":"Baldan, Paolo","last_name":"Baldan"},{"first_name":"Daniele","last_name":"Gorla","full_name":"Gorla, Daniele"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","year":"2014","day":"01","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","page":"544 - 559","doi":"10.1007/978-3-662-44584-6_37","date_published":"2014-09-01T00:00:00Z","date_created":"2018-12-11T11:55:27Z"},{"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Aminof B, Rubin S. 2014. First cycle games. Electronic Proceedings in Theoretical Computer Science, EPTCS. SR: Strategic Reasoning, EPTCS, vol. 146, 83–90.","chicago":"Aminof, Benjamin, and Sasha Rubin. “First Cycle Games.” In Electronic Proceedings in Theoretical Computer Science, EPTCS, 146:83–90. Open Publishing Association, 2014. https://doi.org/10.4204/EPTCS.146.11.","ama":"Aminof B, Rubin S. First cycle games. In: Electronic Proceedings in Theoretical Computer Science, EPTCS. Vol 146. Open Publishing Association; 2014:83-90. doi:10.4204/EPTCS.146.11","apa":"Aminof, B., & Rubin, S. (2014). First cycle games. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 146, pp. 83–90). Grenoble, France: Open Publishing Association. https://doi.org/10.4204/EPTCS.146.11","ieee":"B. Aminof and S. Rubin, “First cycle games,” in Electronic Proceedings in Theoretical Computer Science, EPTCS, Grenoble, France, 2014, vol. 146, pp. 83–90.","short":"B. Aminof, S. Rubin, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, 2014, pp. 83–90.","mla":"Aminof, Benjamin, and Sasha Rubin. “First Cycle Games.” Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 146, Open Publishing Association, 2014, pp. 83–90, doi:10.4204/EPTCS.146.11."},"title":"First cycle games","author":[{"full_name":"Aminof, Benjamin","last_name":"Aminof","first_name":"Benjamin","id":"4A55BD00-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Rubin","full_name":"Rubin, Sasha","first_name":"Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"7345","quality_controlled":"1","publisher":"Open Publishing Association","oa":1,"day":"01","publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS","has_accepted_license":"1","year":"2014","date_published":"2014-04-01T00:00:00Z","doi":"10.4204/EPTCS.146.11","date_created":"2018-12-11T11:46:41Z","page":"83 - 90","_id":"475","status":"public","pubrep_id":"952","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2014-04-05","location":"Grenoble, France","end_date":"2014-04-06","name":"SR: Strategic Reasoning"},"ddc":["004"],"date_updated":"2021-01-12T08:00:53Z","file_date_updated":"2020-07-14T12:46:35Z","department":[{"_id":"KrCh"}],"oa_version":"Published Version","abstract":[{"text":"First cycle games (FCG) are played on a finite graph by two players who push a token along the edges until a vertex is repeated, and a simple cycle is formed. The winner is determined by some fixed property Y of the sequence of labels of the edges (or nodes) forming this cycle. These games are traditionally of interest because of their connection with infinite-duration games such as parity and mean-payoff games. We study the memory requirements for winning strategies of FCGs and certain associated infinite duration games. We exhibit a simple FCG that is not memoryless determined (this corrects a mistake in Memoryless determinacy of parity and mean payoff games: a simple proof by Bj⋯orklund, Sandberg, Vorobyov (2004) that claims that FCGs for which Y is closed under cyclic permutations are memoryless determined). We show that θ (n)! memory (where n is the number of nodes in the graph), which is always sufficient, may be necessary to win some FCGs. On the other hand, we identify easy to check conditions on Y (i.e., Y is closed under cyclic permutations, and both Y and its complement are closed under concatenation) that are sufficient to ensure that the corresponding FCGs and their associated infinite duration games are memoryless determined. We demonstrate that many games considered in the literature, such as mean-payoff, parity, energy, etc., satisfy these conditions. On the complexity side, we show (for efficiently computable Y) that while solving FCGs is in PSPACE, solving some families of FCGs is PSPACE-hard. ","lang":"eng"}],"month":"04","intvolume":" 146","alternative_title":["EPTCS"],"scopus_import":1,"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"5260","checksum":"4d7b4ab82980cca2b96ac7703992a8c8","creator":"system","file_size":100115,"date_updated":"2020-07-14T12:46:35Z","file_name":"IST-2018-952-v1+1_2014_Rubin_First_cycle.pdf","date_created":"2018-12-12T10:17:08Z"}],"language":[{"iso":"eng"}],"publication_status":"published","volume":146,"ec_funded":1},{"issue":"PART 1","volume":8634,"related_material":{"record":[{"status":"public","id":"2211","relation":"later_version"},{"id":"5381","status":"public","relation":"earlier_version"}]},"ec_funded":1,"publication_status":"published","language":[{"iso":"eng"}],"scopus_import":1,"alternative_title":["LNCS"],"month":"01","intvolume":" 8634","abstract":[{"lang":"eng","text":"We consider two-player zero-sum partial-observation stochastic games on graphs. Based on the information available to the players these games can be classified as follows: (a) general partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) perfect-observation (both players have complete view of the game). The one-sided partial-observation games subsumes the important special case of one-player partial-observation stochastic games (or partial-observation Markov decision processes (POMDPs)). Based on the randomization available for the strategies, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. We consider all these classes of games with reachability, and parity objectives that can express all ω-regular objectives. The analysis problems are classified into the qualitative analysis that asks for the existence of a strategy that ensures the objective with probability 1; and the quantitative analysis that asks for the existence of a strategy that ensures the objective with probability at least λ (0,1). In this talk we will cover a wide range of results: for perfect-observation games; for POMDPs; for one-sided partial-observation games; and for general partial-observation games."}],"oa_version":"None","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:23:43Z","type":"conference","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","location":"Budapest, Hungary","end_date":"2014-08-29","start_date":"2014-08-25"},"status":"public","pubrep_id":"141","_id":"1903","page":"1 - 4","date_published":"2014-01-01T00:00:00Z","doi":"10.1007/978-3-662-44522-8_1","date_created":"2018-12-11T11:54:38Z","year":"2014","day":"01","quality_controlled":"1","publisher":"Springer","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"}],"publist_id":"5192","title":"Partial-observation stochastic reachability and parity games","citation":{"chicago":"Chatterjee, Krishnendu. “Partial-Observation Stochastic Reachability and Parity Games,” 8634:1–4. Springer, 2014. https://doi.org/10.1007/978-3-662-44522-8_1.","ista":"Chatterjee K. 2014. Partial-observation stochastic reachability and parity games. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 8634, 1–4.","mla":"Chatterjee, Krishnendu. Partial-Observation Stochastic Reachability and Parity Games. Vol. 8634, no. PART 1, Springer, 2014, pp. 1–4, doi:10.1007/978-3-662-44522-8_1.","ama":"Chatterjee K. Partial-observation stochastic reachability and parity games. In: Vol 8634. Springer; 2014:1-4. doi:10.1007/978-3-662-44522-8_1","apa":"Chatterjee, K. (2014). Partial-observation stochastic reachability and parity games (Vol. 8634, pp. 1–4). Presented at the MFCS: Mathematical Foundations of Computer Science, Budapest, Hungary: Springer. https://doi.org/10.1007/978-3-662-44522-8_1","ieee":"K. Chatterjee, “Partial-observation stochastic reachability and parity games,” presented at the MFCS: Mathematical Foundations of Computer Science, Budapest, Hungary, 2014, vol. 8634, no. PART 1, pp. 1–4.","short":"K. Chatterjee, in:, Springer, 2014, pp. 1–4."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}]},{"article_number":"16","citation":{"chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” ACM Transactions on Computational Logic (TOCL). ACM, 2014. https://doi.org/10.1145/2579821.","ista":"Chatterjee K, Doyen L. 2014. Partial-observation stochastic games: How to win when belief fails. ACM Transactions on Computational Logic (TOCL). 15(2), 16.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 2, 16, ACM, 2014, doi:10.1145/2579821.","ama":"Chatterjee K, Doyen L. Partial-observation stochastic games: How to win when belief fails. ACM Transactions on Computational Logic (TOCL). 2014;15(2). doi:10.1145/2579821","apa":"Chatterjee, K., & Doyen, L. (2014). Partial-observation stochastic games: How to win when belief fails. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2579821","short":"K. Chatterjee, L. Doyen, ACM Transactions on Computational Logic (TOCL) 15 (2014).","ieee":"K. Chatterjee and L. Doyen, “Partial-observation stochastic games: How to win when belief fails,” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 2. ACM, 2014."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"4759","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"}],"external_id":{"arxiv":["1107.2141"]},"title":"Partial-observation stochastic games: How to win when belief fails","publisher":"ACM","quality_controlled":"1","oa":1,"year":"2014","day":"01","publication":"ACM Transactions on Computational Logic (TOCL)","doi":"10.1145/2579821","date_published":"2014-04-01T00:00:00Z","date_created":"2018-12-11T11:56:21Z","_id":"2211","type":"journal_article","status":"public","date_updated":"2023-02-23T12:23:43Z","department":[{"_id":"KrCh"}],"abstract":[{"lang":"eng","text":"In two-player finite-state stochastic games of partial observation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distribution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1) or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Our main results for pure strategies are as follows: (1) For one-sided games with player 2 having perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete and present symbolic algorithms that avoid the explicit exponential construction. (2) For one-sided games with player 1 having perfect observation we show that nonelementarymemory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least nonelementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibit serious flaws in previous results of the literature: we show a nonelementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed."}],"oa_version":"Preprint","scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1107.2141"}],"month":"04","intvolume":" 15","publication_status":"published","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"1903","relation":"earlier_version"},{"relation":"earlier_version","status":"public","id":"2955"},{"relation":"earlier_version","status":"public","id":"5381"}]},"volume":15,"issue":"2"},{"quality_controlled":"1","publisher":"ACM","oa":1,"acknowledgement":"The research was supported in part by ERC Starting grant 278410 (QUALITY).","date_published":"2014-09-16T00:00:00Z","doi":"10.1145/2629686","date_created":"2018-12-11T11:55:21Z","has_accepted_license":"1","year":"2014","day":"16","publication":"ACM Transactions on Computational Logic (TOCL)","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"article_number":"27","author":[{"full_name":"Boker, Udi","last_name":"Boker","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"publist_id":"5013","article_processing_charge":"No","title":"Temporal specifications with accumulative values","citation":{"ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 4. ACM, 2014.","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 15 (2014).","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 2014;15(4). doi:10.1145/2629686","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2014). Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2629686","mla":"Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic (TOCL), vol. 15, no. 4, 27, ACM, 2014, doi:10.1145/2629686.","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 15(4), 27.","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic (TOCL). ACM, 2014. https://doi.org/10.1145/2629686."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"month":"09","intvolume":" 15","abstract":[{"lang":"eng","text":"Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with "controlled accumulation," allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable."}],"oa_version":"Submitted Version","related_material":{"record":[{"id":"3356","status":"public","relation":"earlier_version"},{"status":"public","id":"5385","relation":"earlier_version"}]},"volume":15,"issue":"4","ec_funded":1,"publication_status":"published","file":[{"checksum":"354c41d37500b56320afce94cf9a99c2","file_id":"4851","access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:10:59Z","file_name":"IST-2014-192-v1+1_AccumulativeValues.pdf","creator":"system","date_updated":"2020-07-14T12:45:26Z","file_size":346184}],"language":[{"iso":"eng"}],"article_type":"original","type":"journal_article","status":"public","pubrep_id":"192","_id":"2038","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:26Z","date_updated":"2023-02-23T12:23:54Z","ddc":["000","004"]},{"department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:24:48Z","type":"conference","conference":{"name":"ICST: International Conference on Software Testing, Verification and Validation","start_date":"2014-07-08","location":"Copenhagen, Denmark","end_date":"2014-07-11"},"status":"public","_id":"2162","volume":8573,"issue":"Part 2","related_material":{"record":[{"status":"public","id":"5404","relation":"earlier_version"}]},"ec_funded":1,"publication_status":"published","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1404.5734"}],"month":"01","intvolume":" 8573","abstract":[{"lang":"eng","text":"We study two-player (zero-sum) concurrent mean-payoff games played on a finite-state graph. We focus on the important sub-class of ergodic games where all states are visited infinitely often with probability 1. The algorithmic study of ergodic games was initiated in a seminal work of Hoffman and Karp in 1966, but all basic complexity questions have remained unresolved. Our main results for ergodic games are as follows: We establish (1) an optimal exponential bound on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy); (2) the approximation problem lies in FNP; (3) the approximation problem is at least as hard as the decision problem for simple stochastic games (for which NP ∩ coNP is the long-standing best known bound). We present a variant of the strategy-iteration algorithm by Hoffman and Karp; show that both our algorithm and the classical value-iteration algorithm can approximate the value in exponential time; and identify a subclass where the value-iteration algorithm is a FPTAS. We also show that the exact value can be expressed in the existential theory of the reals, and establish square-root sum hardness for a related class of games."}],"oa_version":"Preprint","publist_id":"4822","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"external_id":{"arxiv":["1404.5734"]},"title":"The complexity of ergodic mean payoff games","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, in:, Springer, 2014, pp. 122–133.","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The complexity of ergodic mean payoff games,” presented at the ICST: International Conference on Software Testing, Verification and Validation, Copenhagen, Denmark, 2014, vol. 8573, no. Part 2, pp. 122–133.","apa":"Chatterjee, K., & Ibsen-Jensen, R. (2014). The complexity of ergodic mean payoff games (Vol. 8573, pp. 122–133). Presented at the ICST: International Conference on Software Testing, Verification and Validation, Copenhagen, Denmark: Springer. https://doi.org/10.1007/978-3-662-43951-7_11","ama":"Chatterjee K, Ibsen-Jensen R. The complexity of ergodic mean payoff games. In: Vol 8573. Springer; 2014:122-133. doi:10.1007/978-3-662-43951-7_11","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Ergodic Mean Payoff Games. Vol. 8573, no. Part 2, Springer, 2014, pp. 122–33, doi:10.1007/978-3-662-43951-7_11.","ista":"Chatterjee K, Ibsen-Jensen R. 2014. The complexity of ergodic mean payoff games. ICST: International Conference on Software Testing, Verification and Validation, LNCS, vol. 8573, 122–133.","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Ergodic Mean Payoff Games,” 8573:122–33. Springer, 2014. https://doi.org/10.1007/978-3-662-43951-7_11."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"page":"122 - 133","date_published":"2014-01-01T00:00:00Z","doi":"10.1007/978-3-662-43951-7_11","date_created":"2018-12-11T11:56:04Z","year":"2014","day":"01","quality_controlled":"1","publisher":"Springer","oa":1},{"date_updated":"2023-02-23T12:24:58Z","department":[{"_id":"KrCh"}],"_id":"2213","conference":{"name":"FoSSaCS: Foundations of Software Science and Computation Structures","end_date":"2014-04-13","location":"Grenoble, France","start_date":"2014-04-05"},"type":"conference","status":"public","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"volume":8412,"related_material":{"record":[{"status":"public","id":"5408","relation":"earlier_version"}]},"abstract":[{"lang":"eng","text":"We consider two-player partial-observation stochastic games on finitestate graphs where player 1 has partial observation and player 2 has perfect observation. The winning condition we study are ε-regular conditions specified as parity objectives. The qualitative-analysis problem given a partial-observation stochastic game and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). These qualitative-analysis problems are known to be undecidable. However in many applications the relevant question is the existence of finite-memory strategies, and the qualitative-analysis problems under finite-memory strategies was recently shown to be decidable in 2EXPTIME.We improve the complexity and show that the qualitative-analysis problems for partial-observation stochastic parity games under finite-memory strategies are EXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis."}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1401.3289"}],"scopus_import":1,"alternative_title":["LNCS"],"intvolume":" 8412","month":"04","citation":{"ista":"Chatterjee K, Doyen L, Nain S, Vardi M. 2014. The complexity of partial-observation stochastic parity games with finite-memory strategies. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 8412, 242–257.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Sumit Nain, and Moshe Vardi. “The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies,” 8412:242–57. Springer, 2014. https://doi.org/10.1007/978-3-642-54830-7_16.","ieee":"K. Chatterjee, L. Doyen, S. Nain, and M. Vardi, “The complexity of partial-observation stochastic parity games with finite-memory strategies,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Grenoble, France, 2014, vol. 8412, pp. 242–257.","short":"K. Chatterjee, L. Doyen, S. Nain, M. Vardi, in:, Springer, 2014, pp. 242–257.","apa":"Chatterjee, K., Doyen, L., Nain, S., & Vardi, M. (2014). The complexity of partial-observation stochastic parity games with finite-memory strategies (Vol. 8412, pp. 242–257). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Grenoble, France: Springer. https://doi.org/10.1007/978-3-642-54830-7_16","ama":"Chatterjee K, Doyen L, Nain S, Vardi M. The complexity of partial-observation stochastic parity games with finite-memory strategies. In: Vol 8412. Springer; 2014:242-257. doi:10.1007/978-3-642-54830-7_16","mla":"Chatterjee, Krishnendu, et al. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. Vol. 8412, Springer, 2014, pp. 242–57, doi:10.1007/978-3-642-54830-7_16."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["1401.3289"]},"publist_id":"4757","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"first_name":"Sumit","full_name":"Nain, Sumit","last_name":"Nain"},{"first_name":"Moshe","full_name":"Vardi, Moshe","last_name":"Vardi"}],"title":"The complexity of partial-observation stochastic parity games with finite-memory strategies","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"year":"2014","day":"01","page":"242 - 257","date_created":"2018-12-11T11:56:21Z","doi":"10.1007/978-3-642-54830-7_16","date_published":"2014-04-01T00:00:00Z","acknowledgement":"This research was supported by European project Cassting (FP7-601148), NSF grants CNS 1049862 and CCF-1139011, by NSF Expe ditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program Engineering”, by BSF grant 9800096, and by gift from Intel.","oa":1,"publisher":"Springer","quality_controlled":"1"},{"date_updated":"2023-02-23T12:24:50Z","department":[{"_id":"KrCh"}],"_id":"2212","type":"conference","conference":{"name":"FoSSaCS: Foundations of Software Science and Computation Structures","start_date":"2014-04-05","end_date":"2014-04-13","location":"Grenoble, France"},"status":"public","publication_status":"published","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"5405","relation":"earlier_version"}]},"volume":8412,"ec_funded":1,"abstract":[{"text":"The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use 2 1/2-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider 2 1/2-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in NP ∩ coNP, matching the best known bound in the special case of 2-player games (where all transitions are deterministic). We present an algorithm running in time O(d·n2d·MeanGame) to compute the set of almost-sure winning states from which the objective can be ensured with probability 1, where n is the number of states of the game, d the number of priorities of the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states in 2 1/2-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective). ","lang":"eng"}],"oa_version":"None","scopus_import":1,"alternative_title":["LNCS"],"month":"04","intvolume":" 8412","citation":{"short":"K. Chatterjee, L. Doyen, H. Gimbert, Y. Oualhadj, in:, Springer, 2014, pp. 210–225.","ieee":"K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj, “Perfect-information stochastic mean-payoff parity games,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Grenoble, France, 2014, vol. 8412, pp. 210–225.","apa":"Chatterjee, K., Doyen, L., Gimbert, H., & Oualhadj, Y. (2014). Perfect-information stochastic mean-payoff parity games (Vol. 8412, pp. 210–225). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Grenoble, France: Springer. https://doi.org/10.1007/978-3-642-54830-7_14","ama":"Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. Perfect-information stochastic mean-payoff parity games. In: Vol 8412. Springer; 2014:210-225. doi:10.1007/978-3-642-54830-7_14","mla":"Chatterjee, Krishnendu, et al. Perfect-Information Stochastic Mean-Payoff Parity Games. Vol. 8412, Springer, 2014, pp. 210–25, doi:10.1007/978-3-642-54830-7_14.","ista":"Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. 2014. Perfect-information stochastic mean-payoff parity games. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 8412, 210–225.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Youssouf Oualhadj. “Perfect-Information Stochastic Mean-Payoff Parity Games,” 8412:210–25. Springer, 2014. https://doi.org/10.1007/978-3-642-54830-7_14."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"4758","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"first_name":"Hugo","last_name":"Gimbert","full_name":"Gimbert, Hugo"},{"first_name":"Youssouf","last_name":"Oualhadj","full_name":"Oualhadj, Youssouf"}],"title":"Perfect-information stochastic mean-payoff parity games","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"year":"2014","day":"01","page":"210 - 225","date_published":"2014-04-01T00:00:00Z","doi":"10.1007/978-3-642-54830-7_14","date_created":"2018-12-11T11:56:21Z","acknowledgement":"This research was supported by European project Cassting (FP7-601148).\r\nA Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/128.","quality_controlled":"1","publisher":"Springer"},{"date_updated":"2023-02-23T12:25:01Z","citation":{"mla":"Chatterjee, Krishnendu, et al. Edit Distance for Timed Automata. Springer, 2014, pp. 303–12, doi:10.1145/2562059.2562141.","ama":"Chatterjee K, Ibsen-Jensen R, Majumdar R. Edit distance for timed automata. In: Springer; 2014:303-312. doi:10.1145/2562059.2562141","apa":"Chatterjee, K., Ibsen-Jensen, R., & Majumdar, R. (2014). Edit distance for timed automata (pp. 303–312). Presented at the HSCC: Hybrid Systems - Computation and Control, Berlin, Germany: Springer. https://doi.org/10.1145/2562059.2562141","short":"K. Chatterjee, R. Ibsen-Jensen, R. Majumdar, in:, Springer, 2014, pp. 303–312.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and R. Majumdar, “Edit distance for timed automata,” presented at the HSCC: Hybrid Systems - Computation and Control, Berlin, Germany, 2014, pp. 303–312.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Ritankar Majumdar. “Edit Distance for Timed Automata,” 303–12. Springer, 2014. https://doi.org/10.1145/2562059.2562141.","ista":"Chatterjee K, Ibsen-Jensen R, Majumdar R. 2014. Edit distance for timed automata. HSCC: Hybrid Systems - Computation and Control, 303–312."},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"publist_id":"4752","title":"Edit distance for timed automata","department":[{"_id":"KrCh"}],"_id":"2216","conference":{"start_date":"2017-04-15","end_date":"2017-04-17","location":"Berlin, Germany","name":"HSCC: Hybrid Systems - Computation and Control"},"type":"conference","status":"public","year":"2014","publication_status":"published","language":[{"iso":"eng"}],"day":"01","page":"303 - 312","date_created":"2018-12-11T11:56:22Z","date_published":"2014-01-01T00:00:00Z","related_material":{"record":[{"status":"public","id":"5409","relation":"earlier_version"}]},"doi":"10.1145/2562059.2562141","abstract":[{"lang":"eng","text":"The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition. In this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in time stamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than δ away from the parameter, for δ > 0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and analogous decidability results hold for rectangular automata."}],"oa_version":"Submitted Version","main_file_link":[{"open_access":"1","url":"https://dl.acm.org/citation.cfm?doid=2562059.2562141"}],"oa":1,"quality_controlled":"1","publisher":"Springer","month":"01"},{"related_material":{"record":[{"status":"public","id":"2063","relation":"later_version"},{"relation":"earlier_version","id":"5412","status":"public"},{"relation":"later_version","id":"5414","status":"public"}]},"date_published":"2014-02-06T00:00:00Z","doi":"10.15479/AT:IST-2014-153-v2-2","date_created":"2018-12-12T11:39:11Z","page":"33","day":"06","file":[{"checksum":"ce4967a184d84863eec76c66cbac1614","file_id":"5539","access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T11:54:17Z","file_name":"IST-2014-153-v2+2_main.pdf","creator":"system","date_updated":"2020-07-14T12:46:47Z","file_size":606049}],"language":[{"iso":"eng"}],"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"year":"2014","publication_status":"published","month":"02","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"oa_version":"Published Version","abstract":[{"lang":"eng","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.\r\nWe introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.\r\nWe present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. "}],"file_date_updated":"2020-07-14T12:46:47Z","department":[{"_id":"KrCh"}],"title":"CEGAR for qualitative analysis of probabilistic systems","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Daca","full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"}],"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:25:18Z","citation":{"ista":"Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic systems, IST Austria, 33p.","chicago":"Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v2-2.","ama":"Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v2-2","apa":"Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v2-2","ieee":"K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis of probabilistic systems. IST Austria, 2014.","short":"K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic Systems, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v2-2."},"status":"public","pubrep_id":"164","type":"technical_report","_id":"5413"},{"status":"public","pubrep_id":"165","type":"technical_report","_id":"5414","title":"CEGAR for qualitative analysis of probabilistic systems","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:48Z","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin"}],"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v3-1.","short":"K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic Systems, IST Austria, 2014.","ieee":"K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis of probabilistic systems. IST Austria, 2014.","ama":"Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v3-1","apa":"Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v3-1","chicago":"Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v3-1.","ista":"Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic systems, IST Austria, 33p."},"date_updated":"2023-02-23T12:25:15Z","month":"02","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"oa_version":"Published Version","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.\r\nWe introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.\r\nWe present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. \r\nWe have implemented our algorithms and show that the compositional analysis leads to significant improvements. ","lang":"eng"}],"date_published":"2014-02-07T00:00:00Z","related_material":{"record":[{"relation":"later_version","status":"public","id":"2063"},{"status":"public","id":"5412","relation":"earlier_version"},{"status":"public","id":"5413","relation":"earlier_version"}]},"doi":"10.15479/AT:IST-2014-153-v3-1","date_created":"2018-12-12T11:39:12Z","page":"33","file":[{"date_updated":"2020-07-14T12:46:48Z","file_size":606227,"creator":"system","date_created":"2018-12-12T11:53:03Z","file_name":"IST-2014-153-v3+1_main.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5464","checksum":"87b93fe9af71fc5c94b0eb6151537e11"}],"day":"07","language":[{"iso":"eng"}],"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"year":"2014","publication_status":"published"},{"oa_version":"Published Version","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.\r\nWe introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.\r\nWe present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. ","lang":"eng"}],"month":"01","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"day":"29","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"4d6cda4bebed970926403ad6ad8c745f","file_id":"5500","file_size":423322,"date_updated":"2020-07-14T12:46:47Z","creator":"system","file_name":"IST-2014-153-v1+1_main.pdf","date_created":"2018-12-12T11:53:39Z"}],"language":[{"iso":"eng"}],"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","year":"2014","doi":"10.15479/AT:IST-2014-153-v1-1","related_material":{"record":[{"id":"2063","status":"public","relation":"later_version"},{"relation":"later_version","id":"5413","status":"public"},{"id":"5414","status":"public","relation":"later_version"}]},"date_published":"2014-01-29T00:00:00Z","date_created":"2018-12-12T11:39:11Z","page":"31","_id":"5412","status":"public","pubrep_id":"153","type":"technical_report","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic systems, IST Austria, 31p.","chicago":"Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v1-1.","ieee":"K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis of probabilistic systems. IST Austria, 2014.","short":"K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic Systems, IST Austria, 2014.","ama":"Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v1-1","apa":"Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v1-1","mla":"Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v1-1."},"date_updated":"2023-02-23T12:25:18Z","file_date_updated":"2020-07-14T12:46:47Z","title":"CEGAR for qualitative analysis of probabilistic systems","department":[{"_id":"KrCh"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","last_name":"Daca","full_name":"Daca, Przemyslaw"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin"}]},{"oa":1,"quality_controlled":"1","publisher":"Springer","acknowledgement":"This research was partly supported by European project Cassting (FP7-601148).\r\nTechnical Report under https://research-explorer.app.ist.ac.at/record/5418\r\n","date_created":"2018-12-11T11:56:04Z","date_published":"2014-01-01T00:00:00Z","doi":"10.1007/978-3-662-43951-7_10","page":"110 - 121","publication":"Lecture Notes in Computer Science","day":"01","year":"2014","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"title":"Games with a weak adversary","external_id":{"arxiv":["1404.5453"]},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"}],"publist_id":"4821","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Doyen L. 2014. Games with a weak adversary. Lecture Notes in Computer Science. ICALP: Automata, Languages and Programming, LNCS, vol. 8573, 110–121.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Games with a Weak Adversary.” In Lecture Notes in Computer Science, 8573:110–21. Springer, 2014. https://doi.org/10.1007/978-3-662-43951-7_10.","ieee":"K. Chatterjee and L. Doyen, “Games with a weak adversary,” in Lecture Notes in Computer Science, Copenhagen, Denmark, 2014, vol. 8573, no. Part 2, pp. 110–121.","short":"K. Chatterjee, L. Doyen, in:, Lecture Notes in Computer Science, Springer, 2014, pp. 110–121.","apa":"Chatterjee, K., & Doyen, L. (2014). Games with a weak adversary. In Lecture Notes in Computer Science (Vol. 8573, pp. 110–121). Copenhagen, Denmark: Springer. https://doi.org/10.1007/978-3-662-43951-7_10","ama":"Chatterjee K, Doyen L. Games with a weak adversary. In: Lecture Notes in Computer Science. Vol 8573. Springer; 2014:110-121. doi:10.1007/978-3-662-43951-7_10","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Games with a Weak Adversary.” Lecture Notes in Computer Science, vol. 8573, no. Part 2, Springer, 2014, pp. 110–21, doi:10.1007/978-3-662-43951-7_10."},"intvolume":" 8573","month":"01","main_file_link":[{"url":"https://arxiv.org/abs/1404.5453","open_access":"1"}],"alternative_title":["LNCS"],"oa_version":"Preprint","abstract":[{"text":"We consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable in general, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player 1 is less informed than player 2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player 1 more informed than player 2 is much more complicated, and we show that already in the case where player 1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. From our results we derive new complexity results for partial-observation stochastic games.","lang":"eng"}],"ec_funded":1,"issue":"Part 2","volume":8573,"related_material":{"record":[{"status":"public","id":"5418","relation":"earlier_version"}]},"language":[{"iso":"eng"}],"publication_status":"published","status":"public","conference":{"start_date":"2014-07-08","location":"Copenhagen, Denmark","end_date":"2014-07-11","name":"ICALP: Automata, Languages and Programming"},"type":"conference","_id":"2163","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:25:29Z"},{"status":"public","pubrep_id":"187","type":"technical_report","_id":"5419","title":"Improved algorithms for reachability and shortest path on low tree-width graphs","file_date_updated":"2020-07-14T12:46:50Z","department":[{"_id":"KrCh"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"citation":{"mla":"Chatterjee, Krishnendu, et al. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-187-v1-1.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2014). Improved algorithms for reachability and shortest path on low tree-width graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-187-v1-1","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-187-v1-1","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Improved algorithms for reachability and shortest path on low tree-width graphs. IST Austria, 2014.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs, IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-187-v1-1.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Improved algorithms for reachability and shortest path on low tree-width graphs, IST Austria, 34p."},"date_updated":"2021-01-12T08:02:03Z","month":"04","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"oa_version":"Published Version","abstract":[{"text":"We consider the reachability and shortest path problems on low tree-width graphs, with n nodes, m edges, and tree-width t, on a standard RAM with wordsize W. We use O to hide polynomial factors of the inverse of the Ackermann function. Our main contributions are three fold:\r\n1. For reachability, we present an algorithm that requires O(n·t2·log(n/t)) preprocessing time, O(n·(t·log(n/t))/W) space, and O(t/W) time for pair queries and O((n·t)/W) time for single-source queries. Note that for constant t our algorithm uses O(n·logn) time for preprocessing; and O(n/W) time for single-source queries, which is faster than depth first search/breath first search (after the preprocessing).\r\n2. We present an algorithm for shortest path that requires O(n·t2) preprocessing time, O(n·t) space, and O(t2) time for pair queries and O(n·t) time single-source queries.\r\n3. We give a space versus query time trade-off algorithm for shortest path that, given any constant >0, requires O(n·t2) preprocessing time, O(n·t2) space, and O(n1−·t2) time for pair queries.\r\nOur algorithms improve all existing results, and use very simple data structures.","lang":"eng"}],"doi":"10.15479/AT:IST-2014-187-v1-1","date_published":"2014-04-14T00:00:00Z","date_created":"2018-12-12T11:39:13Z","page":"34","file":[{"file_size":670031,"date_updated":"2020-07-14T12:46:50Z","creator":"system","file_name":"IST-2014-187-v1+1_main_full_tech.pdf","date_created":"2018-12-12T11:54:25Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"5548","checksum":"c608e66030a4bf51d2d99b451f539b99"}],"day":"14","language":[{"iso":"eng"}],"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"year":"2014","publication_status":"published"},{"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"}],"title":"Games with a weak adversary","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:49Z","date_updated":"2023-02-23T10:30:58Z","citation":{"chicago":"Chatterjee, Krishnendu, and Laurent Doyen. Games with a Weak Adversary. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-176-v1-1.","ista":"Chatterjee K, Doyen L. 2014. Games with a weak adversary, IST Austria, 18p.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. Games with a Weak Adversary. IST Austria, 2014, doi:10.15479/AT:IST-2014-176-v1-1.","short":"K. Chatterjee, L. Doyen, Games with a Weak Adversary, IST Austria, 2014.","ieee":"K. Chatterjee and L. Doyen, Games with a weak adversary. IST Austria, 2014.","apa":"Chatterjee, K., & Doyen, L. (2014). Games with a weak adversary. IST Austria. https://doi.org/10.15479/AT:IST-2014-176-v1-1","ama":"Chatterjee K, Doyen L. Games with a Weak Adversary. IST Austria; 2014. doi:10.15479/AT:IST-2014-176-v1-1"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"type":"technical_report","status":"public","pubrep_id":"176","_id":"5418","page":"18","date_published":"2014-03-22T00:00:00Z","doi":"10.15479/AT:IST-2014-176-v1-1","related_material":{"record":[{"status":"public","id":"2163","relation":"later_version"}]},"date_created":"2018-12-12T11:39:13Z","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","year":"2014","day":"22","file":[{"date_created":"2018-12-12T11:53:07Z","file_name":"IST-2014-176-v1+1_icalp_14.pdf","date_updated":"2020-07-14T12:46:49Z","file_size":328253,"creator":"system","checksum":"1d6958aa60050e1c3e932c6e5f34c39f","file_id":"5468","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"03","abstract":[{"lang":"eng","text":"We consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player 1 is less informed than player 2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player 1 more informed than player 2 is much more complicated, and we show that already in the case where player 1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. Our results have tight connections with partial-observation stochastic games for which we derive new complexity results."}],"oa_version":"Published Version"},{"abstract":[{"text":"We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy).","lang":"eng"}],"oa_version":"Published Version","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa":1,"month":"04","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"year":"2014","publication_status":"published","day":"14","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"49e0fd3e62650346daf7dc04604f7a0a","file_id":"5520","file_size":584368,"date_updated":"2020-07-14T12:46:50Z","creator":"system","file_name":"IST-2014-191-v1+1_main_full.pdf","date_created":"2018-12-12T11:53:58Z"}],"language":[{"iso":"eng"}],"page":"49","doi":"10.15479/AT:IST-2014-191-v1-1","date_published":"2014-04-14T00:00:00Z","date_created":"2018-12-12T11:39:14Z","_id":"5420","type":"technical_report","status":"public","pubrep_id":"191","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, The Value 1 Problem for Concurrent Mean-Payoff Games, IST Austria, 2014.","ieee":"K. Chatterjee and R. Ibsen-Jensen, The value 1 problem for concurrent mean-payoff games. IST Austria, 2014.","ama":"Chatterjee K, Ibsen-Jensen R. The Value 1 Problem for Concurrent Mean-Payoff Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-191-v1-1","apa":"Chatterjee, K., & Ibsen-Jensen, R. (2014). The value 1 problem for concurrent mean-payoff games. IST Austria. https://doi.org/10.15479/AT:IST-2014-191-v1-1","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Value 1 Problem for Concurrent Mean-Payoff Games. IST Austria, 2014, doi:10.15479/AT:IST-2014-191-v1-1.","ista":"Chatterjee K, Ibsen-Jensen R. 2014. The value 1 problem for concurrent mean-payoff games, IST Austria, 49p.","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Value 1 Problem for Concurrent Mean-Payoff Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-191-v1-1."},"date_updated":"2021-01-12T08:02:05Z","ddc":["000","005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"}],"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:50Z","title":"The value 1 problem for concurrent mean-payoff games"},{"_id":"5424","status":"public","pubrep_id":"305","type":"technical_report","ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014, doi:10.15479/AT:IST-2014-305-v1-1.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria, 2014.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria, 2014.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2014). Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria. https://doi.org/10.15479/AT:IST-2014-305-v1-1","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria; 2014. doi:10.15479/AT:IST-2014-305-v1-1","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-305-v1-1.","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2014. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications, IST Austria, 12p."},"date_updated":"2023-02-23T12:25:52Z","file_date_updated":"2020-07-14T12:46:51Z","department":[{"_id":"KrCh"}],"title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"first_name":"Raghav","last_name":"Gupta","full_name":"Gupta, Raghav"},{"last_name":"Kanodia","full_name":"Kanodia, Ayush","first_name":"Ayush"}],"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty."}],"month":"09","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"5512","checksum":"35009d5fad01198341e6c1a3353481b7","creator":"system","file_size":655774,"date_updated":"2020-07-14T12:46:51Z","file_name":"IST-2014-305-v1+1_main.pdf","date_created":"2018-12-12T11:53:51Z"}],"day":"09","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2014","doi":"10.15479/AT:IST-2014-305-v1-1","date_published":"2014-09-09T00:00:00Z","related_material":{"record":[{"relation":"later_version","id":"1732","status":"public"},{"id":"5426","status":"public","relation":"later_version"}]},"date_created":"2018-12-12T11:39:15Z","page":"12"},{"file_date_updated":"2020-07-14T12:46:51Z","title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","department":[{"_id":"KrCh"}],"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"first_name":"Raghav","full_name":"Gupta, Raghav","last_name":"Gupta"},{"first_name":"Ayush","full_name":"Kanodia, Ayush","last_name":"Kanodia"}],"ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014, doi:10.15479/AT:IST-2014-305-v2-1.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria, 2014.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria, 2014.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria; 2014. doi:10.15479/AT:IST-2014-305-v2-1","apa":"Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2014). Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria. https://doi.org/10.15479/AT:IST-2014-305-v2-1","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-305-v2-1.","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2014. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications, IST Austria, 10p."},"date_updated":"2023-02-23T12:25:47Z","pubrep_id":"311","status":"public","type":"technical_report","_id":"5426","date_created":"2018-12-12T11:39:16Z","related_material":{"record":[{"id":"1732","status":"public","relation":"later_version"},{"status":"public","id":"5424","relation":"earlier_version"}]},"doi":"10.15479/AT:IST-2014-305-v2-1","date_published":"2014-09-29T00:00:00Z","page":"10","language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T11:54:15Z","file_name":"IST-2014-305-v2+1_main2.pdf","creator":"system","date_updated":"2020-07-14T12:46:51Z","file_size":656019,"checksum":"730c0a8e97cf2712a884b2cc423f3919","file_id":"5537","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"day":"29","year":"2014","publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","month":"09","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa_version":"Published Version","abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty."}]},{"month":"07","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa_version":"Published Version","abstract":[{"lang":"eng","text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm- deadline real-time tasks based on multi-objective graphs: Given a taskset and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. a clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including D(over), that have been proposed in the past, for various tasksets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are tasksets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application. "}],"date_created":"2018-12-12T11:39:15Z","related_material":{"record":[{"relation":"later_version","id":"1714","status":"public"}]},"date_published":"2014-07-29T00:00:00Z","doi":"10.15479/AT:IST-2014-300-v1-1","page":"14","language":[{"iso":"eng"}],"day":"29","file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"5514","checksum":"4b8fde4d9ef6653837f6803921d83032","creator":"system","file_size":1270021,"date_updated":"2020-07-14T12:46:50Z","file_name":"IST-2014-300-v1+1_main.pdf","date_created":"2018-12-12T11:53:53Z"}],"year":"2014","publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","pubrep_id":"300","status":"public","type":"technical_report","_id":"5423","title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","file_date_updated":"2020-07-14T12:46:50Z","department":[{"_id":"KrCh"}],"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Alexander","last_name":"Kössler","full_name":"Kössler, Alexander"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"last_name":"Schmid","full_name":"Schmid, Ulrich","first_name":"Ulrich"}],"ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:11:15Z","citation":{"short":"K. Chatterjee, A. Kössler, A. Pavlogiannis, U. Schmid, A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks, IST Austria, 2014.","ieee":"K. Chatterjee, A. Kössler, A. Pavlogiannis, and U. Schmid, A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. IST Austria, 2014.","ama":"Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria; 2014. doi:10.15479/AT:IST-2014-300-v1-1","apa":"Chatterjee, K., Kössler, A., Pavlogiannis, A., & Schmid, U. (2014). A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. IST Austria. https://doi.org/10.15479/AT:IST-2014-300-v1-1","mla":"Chatterjee, Krishnendu, et al. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria, 2014, doi:10.15479/AT:IST-2014-300-v1-1.","ista":"Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. 2014. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks, IST Austria, 14p.","chicago":"Chatterjee, Krishnendu, Alexander Kössler, Andreas Pavlogiannis, and Ulrich Schmid. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-300-v1-1."}},{"_id":"5427","type":"technical_report","pubrep_id":"314","status":"public","date_updated":"2021-01-12T08:02:09Z","citation":{"mla":"Chatterjee, Krishnendu, et al. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-314-v1-1.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-314-v1-1","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2014). Optimal tree-decomposition balancing and reachability on low treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-314-v1-1","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Optimal tree-decomposition balancing and reachability on low treewidth graphs. IST Austria, 2014.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs, IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-314-v1-1.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Optimal tree-decomposition balancing and reachability on low treewidth graphs, IST Austria, 24p."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"}],"file_date_updated":"2020-07-14T12:46:52Z","title":"Optimal tree-decomposition balancing and reachability on low treewidth graphs","department":[{"_id":"KrCh"}],"abstract":[{"text":"We consider graphs with n nodes together with their tree-decomposition that has b = O ( n ) bags and width t , on the standard RAM computational model with wordsize W = Θ (log n ) . Our contributions are two-fold: Our first contribution is an algorithm that given a graph and its tree-decomposition as input, computes a binary and balanced tree-decomposition of width at most 4 · t + 3 of the graph in O ( b ) time and space, improving a long-standing (from 1992) bound of O ( n · log n ) time for constant treewidth graphs. Our second contribution is on reachability queries for low treewidth graphs. We build on our tree-balancing algorithm and present a data-structure for graph reachability that requires O ( n · t 2 ) preprocessing time, O ( n · t ) space, and O ( d t/ log n e ) time for pair queries, and O ( n · t · log t/ log n ) time for single-source queries. For constant t our data-structure uses O ( n ) time for preprocessing, O (1) time for pair queries, and O ( n/ log n ) time for single-source queries. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries.","lang":"eng"}],"oa_version":"Published Version","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","month":"11","year":"2014","publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","language":[{"iso":"eng"}],"file":[{"creator":"system","date_updated":"2020-07-14T12:46:52Z","file_size":405561,"date_created":"2018-12-12T11:53:10Z","file_name":"IST-2014-314-v1+1_long.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"9d3b90bf4fff74664f182f2d95ef727a","file_id":"5471"}],"day":"05","page":"24","date_created":"2018-12-12T11:39:16Z","date_published":"2014-11-05T00:00:00Z","doi":"10.15479/AT:IST-2014-314-v1-1"},{"title":"Nested weighted automata","file_date_updated":"2020-07-14T12:46:48Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"ddc":["004"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted Automata. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-170-v1-1.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria; 2014. doi:10.15479/AT:IST-2014-170-v1-1","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2014). Nested weighted automata. IST Austria. https://doi.org/10.15479/AT:IST-2014-170-v1-1","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata. IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2014, doi:10.15479/AT:IST-2014-170-v1-1."},"date_updated":"2023-02-23T12:26:19Z","pubrep_id":"170","status":"public","type":"technical_report","_id":"5415","date_created":"2018-12-12T11:39:12Z","related_material":{"record":[{"id":"1656","status":"public","relation":"later_version"},{"status":"public","id":"467","relation":"later_version"},{"status":"public","id":"5436","relation":"later_version"}]},"doi":"10.15479/AT:IST-2014-170-v1-1","date_published":"2014-02-19T00:00:00Z","page":"27","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"5497","checksum":"31f90dcf2cf899c3f8c6427cfcc2b3c7","file_size":573457,"date_updated":"2020-07-14T12:46:48Z","creator":"system","file_name":"IST-2014-170-v1+1_main.pdf","date_created":"2018-12-12T11:53:36Z"}],"day":"19","publication_status":"published","year":"2014","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"month":"02","oa":1,"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","abstract":[{"text":"Recently there has been a significant effort to add quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains. ","lang":"eng"}]},{"type":"technical_report","status":"public","pubrep_id":"190","_id":"5421","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"department":[{"_id":"KrCh"}],"title":"The complexity of evolution on graphs","file_date_updated":"2020-07-14T12:46:50Z","date_updated":"2023-02-23T12:26:33Z","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2014. The complexity of evolution on graphs, IST Austria, 27p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity of Evolution on Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-190-v2-2.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolution on Graphs, IST Austria, 2014.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolution on graphs. IST Austria, 2014.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. The Complexity of Evolution on Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-190-v2-2","apa":"Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2014). The complexity of evolution on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-190-v2-2","mla":"Chatterjee, Krishnendu, et al. The Complexity of Evolution on Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-190-v2-2."},"ddc":["000","005"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"04","abstract":[{"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 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. 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: (1) We show that the qualitative question is NP-complete and the quantitative approximation question is #P-hard in the special case when the interaction and the replacement graphs coincide and even with the restriction that the resident individuals do not reproduce (which corresponds to an invading population taking over an empty structure). (2) We show that in general the qualitative question is PSPACE-complete and the quantitative approximation question is PSPACE-hard and can be solved in exponential time.","lang":"eng"}],"oa_version":"Published Version","page":"27","date_published":"2014-04-18T00:00:00Z","related_material":{"record":[{"status":"public","id":"5432","relation":"later_version"},{"relation":"later_version","status":"public","id":"5440"}]},"doi":"10.15479/AT:IST-2014-190-v2-2","date_created":"2018-12-12T11:39:14Z","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"year":"2014","publication_status":"published","file":[{"file_id":"5538","checksum":"42f3d8b563286eb0d903832bd9a848d3","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2014-190-v2+2_main_full.pdf","date_created":"2018-12-12T11:54:16Z","creator":"system","file_size":443529,"date_updated":"2020-07-14T12:46:50Z"},{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"0c9a2fd822309719634495a35957e34d","file_id":"6852","creator":"kschuh","file_size":440911,"date_updated":"2020-07-14T12:46:50Z","file_name":"IST-2014-190-v1+1_main_full.pdf","date_created":"2019-09-06T07:30:20Z"}],"day":"18","language":[{"iso":"eng"}]},{"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"title":"Doomsday equilibria for omega-regular games","external_id":{"arxiv":["1311.3238"]},"article_processing_charge":"No","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"last_name":"Filiot","full_name":"Filiot, Emmanuel","first_name":"Emmanuel"},{"first_name":"Jean-François","full_name":"Raskin, Jean-François","last_name":"Raskin"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.” VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, vol. 8318, Springer Nature, 2014, pp. 78–97, doi:10.1007/978-3-642-54013-4_5.","apa":"Chatterjee, K., Doyen, L., Filiot, E., & Raskin, J.-F. (2014). Doomsday equilibria for omega-regular games. In VMCAI 2014: Verification, Model Checking, and Abstract Interpretation (Vol. 8318, pp. 78–97). San Diego, CA, United States: Springer Nature. https://doi.org/10.1007/978-3-642-54013-4_5","ama":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. Doomsday equilibria for omega-regular games. In: VMCAI 2014: Verification, Model Checking, and Abstract Interpretation. Vol 8318. Springer Nature; 2014:78-97. doi:10.1007/978-3-642-54013-4_5","ieee":"K. Chatterjee, L. Doyen, E. Filiot, and J.-F. Raskin, “Doomsday equilibria for omega-regular games,” in VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, San Diego, CA, United States, 2014, vol. 8318, pp. 78–97.","short":"K. Chatterjee, L. Doyen, E. Filiot, J.-F. Raskin, in:, VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 78–97.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean-François Raskin. “Doomsday Equilibria for Omega-Regular Games.” In VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, 8318:78–97. Springer Nature, 2014. https://doi.org/10.1007/978-3-642-54013-4_5.","ista":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. 2014. Doomsday equilibria for omega-regular games. VMCAI 2014: Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 78–97."},"publisher":"Springer Nature","quality_controlled":"1","acknowledgement":" Supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No\r\nS11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","date_created":"2022-03-18T13:03:15Z","doi":"10.1007/978-3-642-54013-4_5","date_published":"2014-01-30T00:00:00Z","page":"78-97","publication":"VMCAI 2014: Verification, Model Checking, and Abstract Interpretation","day":"30","year":"2014","status":"public","conference":{"name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","start_date":"2014-01-19","end_date":"2014-01-21","location":"San Diego, CA, United States"},"type":"conference","_id":"10885","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:52:24Z","intvolume":" 8318","month":"01","alternative_title":["LNCS"],"scopus_import":"1","oa_version":"Preprint","abstract":[{"text":"Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\r\nIn this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\r\nWe present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.","lang":"eng"}],"ec_funded":1,"related_material":{"record":[{"relation":"later_version","id":"681","status":"public"}]},"volume":8318,"language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642540127"],"eisbn":["9783642540134"]}},{"_id":"2039","status":"public","pubrep_id":"440","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["510"],"date_updated":"2023-02-23T14:06:36Z","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:26Z","oa_version":"Published Version","abstract":[{"text":"A fundamental question in biology is the following: what is the time scale that is needed for evolutionary innovations? There are many results that characterize single steps in terms of the fixation time of new mutants arising in populations of certain size and structure. But here we ask a different question, which is concerned with the much longer time scale of evolutionary trajectories: how long does it take for a population exploring a fitness landscape to find target sequences that encode new biological functions? Our key variable is the length, (Formula presented.) of the genetic sequence that undergoes adaptation. In computer science there is a crucial distinction between problems that require algorithms which take polynomial or exponential time. The latter are considered to be intractable. Here we develop a theoretical approach that allows us to estimate the time of evolution as function of (Formula presented.) We show that adaptation on many fitness landscapes takes time that is exponential in (Formula presented.) even if there are broad selection gradients and many targets uniformly distributed in sequence space. These negative results lead us to search for specific mechanisms that allow evolution to work on polynomial time scales. We study a regeneration process and show that it enables evolution to work in polynomial time.","lang":"eng"}],"month":"09","intvolume":" 10","scopus_import":1,"file":[{"creator":"system","file_size":1399093,"date_updated":"2020-07-14T12:45:26Z","file_name":"IST-2016-440-v1+1_journal.pcbi.1003818.pdf","date_created":"2018-12-12T10:11:35Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"712d4c5787ddf97809cfc962507f0738","file_id":"4890"}],"language":[{"iso":"eng"}],"publication_status":"published","issue":"9","volume":10,"related_material":{"record":[{"status":"public","id":"9739","relation":"research_data"}]},"ec_funded":1,"article_number":"7p","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Nowak. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology. Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. 2014. The time scale of evolutionary innovation. PLoS Computational Biology. 10(9), 7p.","mla":"Chatterjee, Krishnendu, et al. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology, vol. 10, no. 9, 7p, Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Nowak, M. (2014). The time scale of evolutionary innovation. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. The time scale of evolutionary innovation. PLoS Computational Biology. 2014;10(9). doi:10.1371/journal.pcbi.1003818","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Nowak, PLoS Computational Biology 10 (2014).","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Nowak, “The time scale of evolutionary innovation,” PLoS Computational Biology, vol. 10, no. 9. Public Library of Science, 2014."},"title":"The time scale of evolutionary innovation","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ben","full_name":"Adlam, Ben","last_name":"Adlam"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"publist_id":"5012","publisher":"Public Library of Science","quality_controlled":"1","oa":1,"day":"11","publication":"PLoS Computational Biology","has_accepted_license":"1","year":"2014","doi":"10.1371/journal.pcbi.1003818","date_published":"2014-09-11T00:00:00Z","date_created":"2018-12-11T11:55:22Z"},{"type":"research_data_reference","status":"public","_id":"9739","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"full_name":"Adlam, Ben","last_name":"Adlam","first_name":"Ben"},{"first_name":"Martin","last_name":"Novak","full_name":"Novak, Martin"}],"article_processing_charge":"No","department":[{"_id":"KrCh"}],"title":"Detailed proofs for “The time scale of evolutionary innovation”","date_updated":"2023-02-23T10:25:37Z","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Novak. “Detailed Proofs for ‘The Time Scale of Evolutionary Innovation.’” Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.s001.","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. 2014. Detailed proofs for “The time scale of evolutionary innovation”, Public Library of Science, 10.1371/journal.pcbi.1003818.s001.","mla":"Chatterjee, Krishnendu, et al. Detailed Proofs for “The Time Scale of Evolutionary Innovation.” Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.s001.","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Novak, M. (2014). Detailed proofs for “The time scale of evolutionary innovation.” Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818.s001","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. Detailed proofs for “The time scale of evolutionary innovation.” 2014. doi:10.1371/journal.pcbi.1003818.s001","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Novak, “Detailed proofs for ‘The time scale of evolutionary innovation.’” Public Library of Science, 2014.","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Novak, (2014)."},"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","publisher":"Public Library of Science","month":"09","oa_version":"Published Version","related_material":{"record":[{"relation":"used_in_publication","id":"2039","status":"public"}]},"doi":"10.1371/journal.pcbi.1003818.s001","date_published":"2014-09-11T00:00:00Z","date_created":"2021-07-28T08:13:57Z","year":"2014","day":"11"},{"abstract":[{"lang":"eng","text":"Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several worst-case instances on which previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting the graph structure does not necessarily help."}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.08234"}],"scopus_import":"1","intvolume":" 70","month":"11","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"related_material":{"record":[{"status":"public","id":"10905","relation":"earlier_version"}]},"volume":70,"issue":"3","_id":"535","type":"journal_article","article_type":"original","status":"public","date_updated":"2023-09-05T14:09:29Z","department":[{"_id":"KrCh"}],"oa":1,"publisher":"Springer","quality_controlled":"1","year":"2014","publication":"Algorithmica","day":"01","page":"457 - 492","date_created":"2018-12-11T11:47:01Z","date_published":"2014-11-01T00:00:00Z","doi":"10.1007/s00453-013-9843-7","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-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"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"citation":{"ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” Algorithmica, vol. 70, no. 3. Springer, pp. 457–492, 2014.","short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70 (2014) 457–492.","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2014). Polynomial-time algorithms for energy games with special weight structures. Algorithmica. Springer. https://doi.org/10.1007/s00453-013-9843-7","ama":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 2014;70(3):457-492. doi:10.1007/s00453-013-9843-7","mla":"Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica, vol. 70, no. 3, Springer, 2014, pp. 457–92, doi:10.1007/s00453-013-9843-7.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2014. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 70(3), 457–492.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica. Springer, 2014. https://doi.org/10.1007/s00453-013-9843-7."},"user_id":"72615eeb-f1f3-11ec-aa25-d4573ddc34fd","article_processing_charge":"No","external_id":{"arxiv":["1604.08234"]},"publist_id":"7282","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"},{"full_name":"Krinninger, Sebastian","last_name":"Krinninger","first_name":"Sebastian"},{"last_name":"Nanongkai","full_name":"Nanongkai, Danupon","first_name":"Danupon"}],"title":"Polynomial-time algorithms for energy games with special weight structures"},{"page":"473 - 490","ec_funded":1,"date_created":"2018-12-11T11:55:30Z","doi":"10.1007/978-3-319-08867-9_31","date_published":"2014-07-01T00:00:00Z","related_material":{"record":[{"relation":"earlier_version","id":"5412","status":"public"},{"id":"5413","status":"public","relation":"earlier_version"},{"status":"public","id":"5414","relation":"earlier_version"},{"status":"public","id":"1155","relation":"dissertation_contains"}]},"volume":8559,"year":"2014","publication_status":"published","language":[{"iso":"eng"}],"day":"01","publisher":"Springer","alternative_title":["LNCS"],"quality_controlled":"1","intvolume":" 8559","month":"07","abstract":[{"text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs 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 ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.","lang":"eng"}],"oa_version":"None","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"4978","title":"CEGAR for qualitative analysis of probabilistic systems","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"citation":{"mla":"Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31.","short":"K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 473–490.","apa":"Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31.","ista":"Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490."},"date_updated":"2023-09-07T11:58:33Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CAV: Computer Aided Verification","location":"Vienna, Austria","end_date":"2014-07-22","start_date":"2014-07-18"},"type":"conference","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"status":"public","_id":"2063"},{"month":"12","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa_version":"Published Version","abstract":[{"text":"Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata.","lang":"eng"}],"date_created":"2018-12-12T11:39:16Z","doi":"10.15479/AT:IST-2014-315-v1-1","related_material":{"record":[{"status":"public","id":"1066","relation":"later_version"}]},"date_published":"2014-12-05T00:00:00Z","page":"26","language":[{"iso":"eng"}],"file":[{"creator":"system","file_size":531046,"date_updated":"2020-07-14T12:46:52Z","file_name":"IST-2014-315-v1+1_report.pdf","date_created":"2018-12-12T11:53:59Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"b1d573bc04365625ff9974880c0aa807","file_id":"5521"}],"day":"05","publication_status":"published","year":"2014","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","pubrep_id":"315","status":"public","type":"technical_report","_id":"5428","title":"Quantitative fair simulation games","file_date_updated":"2020-07-14T12:46:52Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"date_updated":"2023-09-20T12:07:48Z","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. Quantitative Fair Simulation Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-315-v1-1.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p.","mla":"Chatterjee, Krishnendu, et al. Quantitative Fair Simulation Games. IST Austria, 2014, doi:10.15479/AT:IST-2014-315-v1-1.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation Games, IST Austria, 2014.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, Quantitative fair simulation games. IST Austria, 2014.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative Fair Simulation Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-315-v1-1","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2014). Quantitative fair simulation games. IST Austria. https://doi.org/10.15479/AT:IST-2014-315-v1-1"}}]