# Modern Graph Algorithmic Techniques in Formal Verification

Project Period: 2011-09-01 – 2015-08-31
Externally Funded
Principal Investigator
Krishnendu Chatterjee
Department(s)
Chatterjee Group
Description
One of the most important challenges in computer science is to develop correct systems or write correct programs. Subtle errors in complex systems and large programs lead to many critical errors such as the famous Pentium bug, or explosions of space rockets (such as ESA's Ariane 5 rocket). The field of computer aided verification develops automated techniques that formally analyze the correctness of systems and help in discovering subtle errors and bugs. In computer aided verification first a mathematical model of the system is created. Usually these mathematical models are extensions of graph models, where vertices represent states of the system, edges represent transitions, and paths represent behaviors of the system. The mathematical model is then analyzed against a specification which describes the desired set of behaviors of the system. Thus in the heart of the automated techniques are algorithms for analysis of graph properties. As systems that are being developed are becoming larger and more complex at a rapid pace, there is a danger that the existing computer aided verification techniques fail to keep up and become very slow. At the same time modern algorithmic techniques have significantly improved graph algorithmic problems in other fields, but are not yet employed in verification. Hence our goal is to use these new algorithmic techniques to speed up graph theoretic problems in computer aided verification in order to allow it to cope with increased complexity and size. Since most computer aided verification techniques use few core graph theoretic algorithms, we will focus on improving them to impact the formal analysis of systems and programs for a wide range of applications. This is also of theoretical interest as for these problems there are large gaps between the current best known algorithms and the lower bounds. We will focus on the following two modern algorithmic techniques to improve the running time of algorithms of these problems. 1. Dynamic graph algorithmic techniques: Many algorithms in computer aided verification use repeated computation on similar graphs, yet none of the algorithms use data structures developed for dynamic graph problems. We will explore the development of new data structures and techniques for dynamic graph problems to obtain better algorithms. 2. Randomized techniques: Many connectivity-related graph problems can be solved more efficiently with randomization, yet few algorithms in computer aided verification use any randomization. We will study how randomization can be used to design faster algorithms. We will also develop symbolic versions of our algorithms and present efficient implementations of them in a research prototype to demonstrate the practical feasibility of our algorithms.
Grant Number
P 23499-N23
Funding Organisation
FWF

### 113 Publications

2016 | Conference Paper | IST-REx-ID: 1327
Stochastic shortest path with energy constraints in POMDPs
T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotny, in:, Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–1466.

2015 | Journal Article | IST-REx-ID: 1694
Quantitative temporal simulation and refinement distances for timed systems
K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015) 2291–2306.
View | DOI

2014 | Conference Paper | IST-REx-ID: 2027
Verification of markov decision processes using learning algorithms
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.

2015 | Journal Article | IST-REx-ID: 2034
Probabilistic opacity for Markov decision processes
B. Bérard, K. Chatterjee, N. Sznajder, Information Processing Letters 115 (2015) 52–59.

2015 | Conference Paper | IST-REx-ID: 1839
Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187.

2014 | Journal Article | IST-REx-ID: 2039
The time scale of evolutionary innovation
K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Nowak, PLoS Computational Biology 10 (2014).
View | Files available | DOI

2015 | Journal Article | IST-REx-ID: 1598
Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
K. Chatterjee, M. Joglekar, N. Shah, Theoretical Computer Science 573 (2015) 71–89.

2014 | Journal Article | IST-REx-ID: 1733
Interface simulation distances
P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.

2017 | Journal Article | IST-REx-ID: 671
Memory-n strategies of direct reciprocity
C. Hilbe, V. Martinez, K. Chatterjee, M. Nowak, PNAS 114 (2017) 4715–4720.

2013 | Conference Paper | IST-REx-ID: 2820
Automated analysis of real-time scheduling using graph games
K. Chatterjee, A. Kößler, U. Schmid, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, ACM, 2013, pp. 163–172.
View | Files available | DOI

2016 | Journal Article | IST-REx-ID: 1529
Optimal cost almost-sure reachability in POMDPs
K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Artificial Intelligence 234 (2016) 26–48.

2012 | Journal Article | IST-REx-ID: 3260
Evolutionary dynamics of biological auctions
K. Chatterjee, J. Reiter, M. Nowak, Theoretical Population Biology 81 (2012) 69–80.
View | Files available | DOI | Download (ext.) | PubMed | Europe PMC

2018 | Journal Article | IST-REx-ID: 157
Evolution of cooperation in stochastic games
C. Hilbe, Š. Šimsa, K. Chatterjee, M. Nowak, Nature 559 (2018) 246–249.
View | Files available | DOI

2012 | Conference Paper | IST-REx-ID: 2957
Decidable problems for probabilistic automata on infinite words
K. Chatterjee, M. Tracol, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012, p. 6280437.

2014 | Conference Paper | IST-REx-ID: 2212
Perfect-information stochastic mean-payoff parity games
K. Chatterjee, L. Doyen, H. Gimbert, Y. Oualhadj, in:, Springer, 2014, pp. 210–225.
View | Files available | DOI

2015 | Conference Paper | IST-REx-ID: 1656
Nested weighted automata
K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015, p. 7174926.
View | Files available | DOI | arXiv

2017 | Journal Article | IST-REx-ID: 467
Nested weighted automata
K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017) 31.

2016 | Conference Paper | IST-REx-ID: 1138
Quantitative automata under probabilistic semantics
K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.

2013 | Conference Paper | IST-REx-ID: 2446
Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis
K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575.

2013 | Conference Paper | IST-REx-ID: 2819
Quantitative timed simulation functions and refinement metrics for real-time systems
K. Chatterjee, V. Prabhu, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Springer, 2013, pp. 273–282.

2012 | Journal Article | IST-REx-ID: 2972
Energy parity games
K. Chatterjee, L. Doyen, Theoretical Computer Science 458 (2012) 49–60.
View | Files available | DOI

2012 | Journal Article | IST-REx-ID: 3254
The complexity of stochastic Müller games
K. Chatterjee, Information and Computation 211 (2012) 29–48.

2014 | Conference Paper | IST-REx-ID: 2054
Qualitative concurrent parity games: Bounded rationality
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.
View | Files available | DOI

2014 | Conference Paper | IST-REx-ID: 475
First cycle games
B. Aminof, S. Rubin, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, 2014, pp. 83–90.
View | Files available | DOI

2017 | Journal Article | IST-REx-ID: 716
The complexity of mean-payoff pushdown games
K. Chatterjee, Y. Velner, Journal of the ACM 64 (2017) 34.
View | DOI

2017 | Journal Article | IST-REx-ID: 653
Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer
A. Makohon Moore, M. Zhang, J. Reiter, I. Božić, B. Allen, D. Kundu, K. Chatterjee, F. Wong, Y. Jiao, Z. Kohutek, J. Hong, M. Attiyeh, B. Javier, L. Wood, R. Hruban, M. Nowak, N. Papadopoulos, K. Kinzler, B. Vogelstein, C. Iacobuzio Donahue, Nature Genetics 49 (2017) 358–366.
View | DOI

2015 | Journal Article | IST-REx-ID: 1501
CEGAR for compositional analysis of qualitative properties in Markov decision processes
K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264.

2015 | Journal Article | IST-REx-ID: 1602
Faster algorithms for algebraic path properties in recursive state machines with constant treewidth
K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.

2015 | Conference Paper | IST-REx-ID: 1657
Unifying two views on multiple mean-payoff objectives in Markov decision processes
K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.
View | Files available | DOI

2015 | Conference Paper | IST-REx-ID: 1607
Faster algorithms for quantitative verification in constant treewidth graphs
K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.

2018 | Journal Article | IST-REx-ID: 2
Indirect reciprocity with private noisy and incomplete information
C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, M. Nowak, PNAS 115 (2018) 12241–12246.
View | Files available | DOI | Download (ext.) | PubMed | Europe PMC

2012 | Conference Paper | IST-REx-ID: 3165
An O(n2) time algorithm for alternating Büchi games
K. Chatterjee, M. Henzinger, in:, Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2012, pp. 1386–1399.
View | Files available | DOI

2015 | Conference Paper | IST-REx-ID: 1481
Automatic generation of alternative starting positions for simple traditional board games
U. Ahmed, K. Chatterjee, S. Gulwani, in:, AAAI Press, 2015, pp. 745–752.

2014 | Conference Paper | IST-REx-ID: 2213
The complexity of partial-observation stochastic parity games with finite-memory strategies
K. Chatterjee, L. Doyen, S. Nain, M. Vardi, in:, Springer, 2014, pp. 242–257.

2014 | Conference Paper | IST-REx-ID: 2162
The complexity of ergodic mean payoff games
K. Chatterjee, R. Ibsen-Jensen, in:, Springer, 2014, pp. 122–133.

2016 | Conference Paper | IST-REx-ID: 1324
Indefinite-horizon reachability in Goal-DEC-POMDPs
K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, AAAI Press, 2016, pp. 88–96.

2013 | Conference Paper | IST-REx-ID: 1374
Infinite-state games with finitary conditions
K. Chatterjee, N. Fijalkow, in:, 22nd EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–196.
View | Files available | DOI

2015 | Conference Paper | IST-REx-ID: 1689
Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
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.

2015 | Conference Paper | IST-REx-ID: 1691
Temporal logic motion planning using POMDPs with parity objectives: Case study paper
M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–238.
View | DOI

2015 | Journal Article | IST-REx-ID: 1665
Mutations driving CLL and their evolution in progression and relapse
D. Landau, E. Tausch, A. Taylor Weiner, C. Stewart, J. Reiter, J. Bahlo, S. Kluth, I. Božić, M. Lawrence, S. Böttcher, S. Carter, K. Cibulskis, D. Mertens, C. Sougnez, M. Rosenberg, J. Hess, J. Edelmann, S. Kless, M. Kneba, M. Ritgen, A. Fink, K. Fischer, S. Gabriel, E. Lander, M. Nowak, H. Döhner, M. Hallek, D. Neuberg, G. Getz, S. Stilgenbauer, C. Wu, Nature 526 (2015) 525–530.
View | DOI

2014 | Journal Article | IST-REx-ID: 2187
Synthesizing robust systems
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.
View | Files available | DOI

2012 | Conference Paper | IST-REx-ID: 2947
Equivalence of games with probabilistic uncertainty and partial observation games
K. Chatterjee, M. Chmelik, R. Majumdar, in:, Springer, 2012, pp. 385–399.

2012 | Conference Paper | IST-REx-ID: 2916
Interface Simulation Distances
P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, 2012, pp. 29–42.

2012 | Journal Article | IST-REx-ID: 3128
A survey of partial-observation stochastic parity games
K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design 43 (2012) 268–284.
View | Files available | DOI

2018 | Conference Paper | IST-REx-ID: 34
Sensor synthesis for POMDPs with reachability objectives
K. Chatterjee, M. Chemlík, U. Topcu, in:, AAAI Press, 2018, pp. 47–55.

2017 | Journal Article | IST-REx-ID: 717
Hyperplane separation technique for multidimensional mean-payoff games
K. Chatterjee, Y. Velner, Journal of Computer and System Sciences 88 (2017) 236–259.

2018 | Journal Article | IST-REx-ID: 419
Partners and rivals in direct reciprocity
C. Hilbe, K. Chatterjee, M. Nowak, Nature Human Behaviour 2 (2018) 469–477.
View | Files available | DOI

2016 | Conference Paper | IST-REx-ID: 1071
Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs
K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.
View | Files available | DOI

2015 | Journal Article | IST-REx-ID: 1709
Biological auctions with multiple rewards
J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of the Royal Society of London Series B Biological Sciences 282 (2015).
View | Files available | DOI | Download (ext.) | PubMed | Europe PMC

2015 | Conference Paper | IST-REx-ID: 1603
Counterexample explanation by learning small strategies in Markov decision processes
T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.

2017 | Journal Article | IST-REx-ID: 464
Improved algorithms for parity and Streett objectives
K. Chatterjee, M. Henzinger, V. Loitzenbauer, Logical Methods in Computer Science 13 (2017).
View | Files available | DOI

2015 | Conference Paper | IST-REx-ID: 1610
Edit distance for pushdown automata
K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, 9135 (2015) 121–133.
View | Files available | DOI

2018 | Journal Article | IST-REx-ID: 5751
Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory
A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M.A. Nowak, Communications Biology 1 (2018) 71.
View | Files available | DOI

2013 | Conference Paper | IST-REx-ID: 2295 View | Files available | DOI

2013 | Conference Paper | IST-REx-ID: 2000
TTP: Tool for tumor progression
J. Reiter, I. Božić, K. Chatterjee, M. Nowak, in:, Proceedings of 25th Int. Conf. on Computer Aided Verification, Springer, 2013, pp. 101–106.

2014 | Conference Paper | IST-REx-ID: 2163
K. Chatterjee, L. Doyen, in:, Lecture Notes in Computer Science, Springer, 2014, pp. 110–121.

2017 | Journal Article | IST-REx-ID: 1065
Pushdown reachability with constant treewidth
K. Chatterjee, G.F. Osang, Information Processing Letters 122 (2017) 25–29.
View | Files available | DOI

2014 | Journal Article | IST-REx-ID: 1375
Approximating the minimum cycle mean
K. Chatterjee, M. Henzinger, S. Krinninger, V. Loitzenbauer, M. Raskin, Theoretical Computer Science 547 (2014) 104–116.

2015 | Conference Paper | IST-REx-ID: 1609
The complexity of synthesis from probabilistic components
K. Chatterjee, L. Doyen, M. Vardi, 9135 (2015) 108–120.

2017 | Journal Article | IST-REx-ID: 1407
Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.

2018 | Journal Article | IST-REx-ID: 198
Language acquisition with communication between learners
R. Ibsen-Jensen, J. Tkadlec, K. Chatterjee, M. Nowak, Journal of the Royal Society Interface 15 (2018).
View | Files available | DOI

2014 | Journal Article | IST-REx-ID: 2234
Markov decision processes with multiple long-run average objectives
T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, Logical Methods in Computer Science 10 (2014).

2012 | Conference Paper | IST-REx-ID: 2715
Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
K. Chatterjee, M. Joglekar, N. Shah, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 461–473.
View | Files available | DOI

2012 | Conference Paper | IST-REx-ID: 2936
Finite automata with time delay blocks
K. Chatterjee, T.A. Henzinger, V. Prabhu, in:, Roceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 43–52.

2015 | Journal Article | IST-REx-ID: 1731
K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, Information and Computation 245 (2015) 3–16.

2015 | Journal Article | IST-REx-ID: 1856
Measuring and synthesizing systems in probabilistic environments
K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM 62 (2015).

2015 | Journal Article | IST-REx-ID: 523
Looking at mean-payoff and total-payoff through windows
K. Chatterjee, L. Doyen, M. Randour, J. Raskin, Information and Computation 242 (2015) 25–52.

2014 | Journal Article | IST-REx-ID: 535
Polynomial time algorithms for energy games with special weight structures
K. Chatterjee, M. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70 (2014) 457–492.

2016 | Conference Paper | IST-REx-ID: 1438
Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
K. Chatterjee, H. Fu, P. Novotny, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.

2017 | Journal Article | IST-REx-ID: 681
Doomsday equilibria for omega-regular games
K. Chatterjee, L. Doyen, E. Filiot, J. Raskin, Information and Computation 254 (2017) 296–315.

2015 | Conference Paper | IST-REx-ID: 1820
Optimal cost almost-sure reachability in POMDPs
K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , AAAI Press, 2015, pp. 3496–3502.

2015 | Journal Article | IST-REx-ID: 1673
Amplifiers of selection
B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 471 (2015) 20150114.
View | Files available | DOI

2015 | Conference Paper | IST-REx-ID: 1661
Improved algorithms for one-pair and k-pair Streett objectives
K. Chatterjee, M. Henzinger, V. Loitzenbauer, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015, p. 7174888.

2017 | Journal Article | IST-REx-ID: 465
Edit distance for pushdown automata
K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).
View | Files available | DOI

2015 | Journal Article | IST-REx-ID: 1604
Quantitative interprocedural analysis
K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT 50 (2015) 539–551.
View | Files available | DOI

2016 | Conference Paper | IST-REx-ID: 1166
A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps
K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.
View | Files available

2017 | Thesis | IST-REx-ID: 821
Algorithmic advances in program analysis and their applications
A. Pavlogiannis, Algorithmic Advances in Program Analysis and Their Applications, IST Austria, 2017.
View | Files available | DOI

2012 | Conference Paper | IST-REx-ID: 2955
Partial-observation stochastic games: How to win when belief fails
K. Chatterjee, L. Doyen, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012, p. 6280436.

2014 | Conference Paper | IST-REx-ID: 2063
CEGAR for qualitative analysis of probabilistic systems
K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.
View | Files available | DOI

2017 | Conference Paper | IST-REx-ID: 1011
Faster algorithms for weighted recursive state machines
K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.

2017 | Journal Article | IST-REx-ID: 1080
Reconstructing metastatic seeding patterns of human cancers
J. Reiter, A. Makohon Moore, J. Gerold, I. Božić, K. Chatterjee, C. Iacobuzio Donahue, B. Vogelstein, M. Nowak, Nature Communications 8 (2017).
View | Files available | DOI

2015 | Journal Article | IST-REx-ID: 1624
Cellular cooperation with shift updating and repulsion
A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).
View | Files available | DOI

2015 | Journal Article | IST-REx-ID: 1698
The complexity of multi-mean-payoff and multi-energy games
Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.

2015 | Conference Paper | IST-REx-ID: 1838
Assume-guarantee synthesis for concurrent reactive programs with partial information
R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp. 517–532.

2013 | Conference Paper | IST-REx-ID: 2444
Faster algorithms for Markov decision processes with low treewidth
K. Chatterjee, J. Ła̧Cki, 8044 (2013) 543–558.

2013 | Conference Paper | IST-REx-ID: 2305
Trading performance for stability in Markov decision processes
T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, in:, 28th Annual ACM/IEEE Symposium, IEEE, 2013, pp. 331–340.

2017 | Journal Article | IST-REx-ID: 1294
Trading performance for stability in Markov decision processes
T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, Journal of Computer and System Sciences 84 (2017) 144–170.
View | Files available | DOI

2013 | Conference Paper | IST-REx-ID: 2886
Controllable-choice message sequence graphs
M. Chmelik, V. Řehák, 7721 (2013) 118–130.

2013 | Journal Article | IST-REx-ID: 2824
Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems
K. Chatterjee, V. Prabhu, Information and Computation 228–229 (2013) 83–119.
View | DOI

2013 | Journal Article | IST-REx-ID: 2831
Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
K. Chatterjee, M. Henzinger, M. Joglekar, N. Shah, Formal Methods in System Design 42 (2013) 301–327.

2013 | Journal Article | IST-REx-ID: 2836
Assume-guarantee synthesis for digital contract signing
K. Chatterjee, V. Raman, Formal Aspects of Computing 26 (2013) 825–859.

2012 | Journal Article | IST-REx-ID: 2848
Evolutionary game dynamics in populations with different learners
K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.

2013 | Journal Article | IST-REx-ID: 2817
Density games
S. Novak, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 334 (2013) 26–34.
View | Files available | DOI

2012 | Conference Paper | IST-REx-ID: 3252
Synthesizing protocols for digital contract signing
K. Chatterjee, V. Raman, in:, Springer, 2012, pp. 152–168.

2014 | Journal Article | IST-REx-ID: 2141 View | Files available | DOI | Download (ext.)

2011 | Conference Paper | IST-REx-ID: 3346
Two views on multiple mean payoff objectives in Markov Decision Processes
T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, in:, IEEE, 2011.

2018 | Journal Article | IST-REx-ID: 454
Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness
J. Reiter, C. Hilbe, D. Rand, K. Chatterjee, M. Nowak, Nature Communications 9 (2018).
View | Files available | DOI

2018 | Journal Article | IST-REx-ID: 5993
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018).
View | Files available | DOI

2018 | Journal Article | IST-REx-ID: 738
Automated competitive analysis of real time scheduling with graph games
K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54 (2018) 166–207.
View | Files available | DOI

2013 | Conference Paper | IST-REx-ID: 2329
Hyperplane separation technique for multidimensional mean-payoff games
K. Chatterjee, Y. Velner, 8052 (2013) 500–515.