33 Search Results for "Chatterjee, Krishnendu"

Document
DOI: 10.4230/LIPIcs.MFCS.2023.15
Entropic Risk for Turn-Based Stochastic Games

Authors: Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of turn-based stochastic games with the total reward objective. This gives rise to an objective function that demands the control of systems in a risk-averse manner. We show that the resulting games are determined and, in particular, admit optimal memoryless deterministic strategies. This contrasts risk measures that previously have been considered in the special case of Markov decision processes and that require randomization and/or memory. We provide several results on the decidability and the computational complexity of the threshold problem, i.e. whether the optimal value of ERisk exceeds a given threshold. In the most general case, the problem is decidable subject to Shanuel’s conjecture. If all inputs are rational, the resulting threshold problem can be solved using algebraic numbers, leading to decidability via a polynomial-time reduction to the existential theory of the reals. Further restrictions on the encoding of the input allow the solution of the threshold problem in NP∩coNP. Finally, an approximation algorithm for the optimal value of ERisk is provided.
Cite as

Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. Entropic Risk for Turn-Based Stochastic Games. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 15:1-15:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.MFCS.2023.15,
  author =	{Baier, Christel and Chatterjee, Krishnendu and Meggendorfer, Tobias and Piribauer, Jakob},
  title =	{{Entropic Risk for Turn-Based Stochastic Games}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.15},
  URN =		{urn:nbn:de:0030-drops-185491},
  doi =		{10.4230/LIPIcs.MFCS.2023.15},
  annote =	{Keywords: Stochastic games, risk-aware verification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.11
Complexity of Spatial Games

Authors: Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Ismaël Jecker, and Jakub Svoboda

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
Spatial games form a widely-studied class of games from biology and physics modeling the evolution of social behavior. Formally, such a game is defined by a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G represents an individual, that initially follows some strategy i ∈ {1,2,…,d}. In each round of the game, every individual plays the matrix game with each of its neighbors: An individual following strategy i meeting a neighbor following strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual updates its strategy to its neighbors' strategy with the highest sum of payoffs, and the next round starts. The basic computational problems consist of reachability between configurations and the average frequency of a strategy. For general spatial games and graphs, these problems are in PSPACE. In this paper, we examine restricted setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove that basic computational problems for spatial games with prisoner’s dilemma on a subgraph of a grid are PSPACE-hard.
Cite as

Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Ismaël Jecker, and Jakub Svoboda. Complexity of Spatial Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2022.11,
  author =	{Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Jecker, Isma\"{e}l and Svoboda, Jakub},
  title =	{{Complexity of Spatial Games}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.11},
  URN =		{urn:nbn:de:0030-drops-174038},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.11},
  annote =	{Keywords: spatial games, computational complexity, prisoner’s dilemma, dynamical systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.29
Algorithms and Hardness Results for Computing Cores of Markov Chains

Authors: Ali Ahmadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi, and Ðorđe Žikelić

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
Given a Markov chain M = (V, v_0, δ), with state space V and a starting state v_0, and a probability threshold ε, an ε-core is a subset C of states that is left with probability at most ε. More formally, C ⊆ V is an ε-core, iff ℙ[reach (V\C)] ≤ ε. Cores have been applied in a wide variety of verification problems over Markov chains, Markov decision processes, and probabilistic programs, as a means of discarding uninteresting and low-probability parts of a probabilistic system and instead being able to focus on the states that are likely to be encountered in a real-world run. In this work, we focus on the problem of computing a minimal ε-core in a Markov chain. Our contributions include both negative and positive results: (i) We show that the decision problem on the existence of an ε-core of a given size is NP-complete. This solves an open problem posed in [Jan Kretínský and Tobias Meggendorfer, 2020]. We additionally show that the problem remains NP-complete even when limited to acyclic Markov chains with bounded maximal vertex degree; (ii) We provide a polynomial time algorithm for computing a minimal ε-core on Markov chains over control-flow graphs of structured programs. A straightforward combination of our algorithm with standard branch prediction techniques allows one to apply the idea of cores to find a subset of program lines that are left with low probability and then focus any desired static analysis on this core subset.
Cite as

Ali Ahmadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi, and Ðorđe Žikelić. Algorithms and Hardness Results for Computing Cores of Markov Chains. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 29:1-29:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ahmadi_et_al:LIPIcs.FSTTCS.2022.29,
  author =	{Ahmadi, Ali and Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Meggendorfer, Tobias and Safavi, Roodabeh and \v{Z}ikeli\'{c}, Ðor{\d}e},
  title =	{{Algorithms and Hardness Results for Computing Cores of Markov Chains}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.29},
  URN =		{urn:nbn:de:0030-drops-174216},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.29},
  annote =	{Keywords: Markov Chains, Cores, Complexity}
}
Document
DOI: 10.4230/LITES.8.2.5
Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation

Authors: Paul Kröger and Martin Fränzle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Hybrid discrete-continuous system dynamics arises when discrete actions, e.g. by a decision algorithm, meet continuous behaviour, e.g. due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes.Various flavours of hybrid automata have been suggested as a means to formally analyse CPS dynamics. In a previous article, we demonstrated that all these variants of hybrid automata provide inaccurate, in the sense of either overly pessimistic or overly optimistic, verdicts for engineered systems operating under imprecise observation of their environment due to, e.g., measurement error. We suggested a revised formal model, called Bayesian hybrid automata, that is able to represent state tracking and estimation in hybrid systems and thereby enhances precision of verdicts obtained from the model in comparison to traditional model variants.In this article, we present an extended definition of Bayesian hybrid automata which incorporates a new class of guard and invariant functions that allow to evaluate traditional guards and invariants over probability distributions. The resulting framework allows to model observers with knowledge about the control strategy of an observed agent but with imprecise estimates of the data on which the control decisions are based.
Cite as

Paul Kröger and Martin Fränzle. Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 05:1-05:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kroger_et_al:LITES.8.2.5,
  author =	{Kr\"{o}ger, Paul and Fr\"{a}nzle, Martin},
  title =	{{Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{05:1--05:27},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.5},
  doi =		{10.4230/LITES.8.2.5},
  annote =	{Keywords: }
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.42
Quantitative Verification on Product Graphs of Small Treewidth

Authors: Krishnendu Chatterjee, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
Product graphs arise naturally in formal verification and program analysis. For example, the analysis of two concurrent threads requires the product of two component control-flow graphs, and for language inclusion of deterministic automata the product of two automata is constructed. In many cases, the component graphs have constant treewidth, e.g., when the input contains control-flow graphs of programs. We consider the algorithmic analysis of products of two constant-treewidth graphs with respect to three classic specification languages, namely, (a) algebraic properties, (b) mean-payoff properties, and (c) initial credit for energy properties. Our main contributions are as follows. Consider a graph G that is the product of two constant-treewidth graphs of size n each. First, given an idempotent semiring, we present an algorithm that computes the semiring transitive closure of G in time Õ(n⁴). Since the output has size Θ(n⁴), our algorithm is optimal (up to polylog factors). Second, given a mean-payoff objective, we present an O(n³)-time algorithm for deciding whether the value of a starting state is non-negative, improving the previously known O(n⁴) bound. Third, given an initial credit for energy objective, we present an O(n⁵)-time algorithm for computing the minimum initial credit for all nodes of G, improving the previously known O(n⁸) bound. At the heart of our approach lies an algorithm for the efficient construction of strongly-balanced tree decompositions of constant-treewidth graphs. Given a constant-treewidth graph G' of n nodes and a positive integer λ, our algorithm constructs a binary tree decomposition of G' of width O(λ) with the property that the size of each subtree decreases geometrically with rate (1/2 + 2^{-λ}).
Cite as

Krishnendu Chatterjee, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Quantitative Verification on Product Graphs of Small Treewidth. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 42:1-42:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2021.42,
  author =	{Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
  title =	{{Quantitative Verification on Product Graphs of Small Treewidth}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{42:1--42:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.42},
  URN =		{urn:nbn:de:0030-drops-155533},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.42},
  annote =	{Keywords: graph algorithms, algebraic paths, mean-payoff, initial credit for energy}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.25
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

Authors: James C. A. Main, Mickael Randour, and Jeremy Sproston

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs [Krishnendu Chatterjee et al., 2015]. It has since proved useful in a variety of settings, including parity objectives in games [Véronique Bruyère et al., 2016] and both mean-payoff and parity objectives in Markov decision processes [Thomas Brihaye et al., 2020]. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting.
Cite as

James C. A. Main, Mickael Randour, and Jeremy Sproston. Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 25:1-25:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{main_et_al:LIPIcs.CONCUR.2021.25,
  author =	{Main, James C. A. and Randour, Mickael and Sproston, Jeremy},
  title =	{{Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{25:1--25:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.25},
  URN =		{urn:nbn:de:0030-drops-144021},
  doi =		{10.4230/LIPIcs.CONCUR.2021.25},
  annote =	{Keywords: Window objectives, timed automata, timed games, parity games}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.124
Faster Algorithms for Bounded Liveness in Graphs and Game Graphs

Authors: Krishnendu Chatterjee, Monika Henzinger, Sagar Sudhir Kale, and Alexander Svozil

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
Graphs and games on graphs are fundamental models for the analysis of reactive systems, in particular, for model-checking and the synthesis of reactive systems. The class of ω-regular languages provides a robust specification formalism for the desired properties of reactive systems. In the classical infinitary formulation of the liveness part of an ω-regular specification, a "good" event must happen eventually without any bound between the good events. A stronger notion of liveness is bounded liveness, which requires that good events happen within d transitions. Given a graph or a game graph with n vertices, m edges, and a bounded liveness objective, the previous best-known algorithmic bounds are as follows: (i) O(dm) for graphs, which in the worst-case is O(n³); and (ii) O(n² d²) for games on graphs. Our main contributions improve these long-standing algorithmic bounds. For graphs we present: (i) a randomized algorithm with one-sided error with running time O(n^{2.5} log n) for the bounded liveness objectives; and (ii) a deterministic linear-time algorithm for the complement of bounded liveness objectives. For games on graphs, we present an O(n² d) time algorithm for the bounded liveness objectives.
Cite as

Krishnendu Chatterjee, Monika Henzinger, Sagar Sudhir Kale, and Alexander Svozil. Faster Algorithms for Bounded Liveness in Graphs and Game Graphs. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 124:1-124:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.ICALP.2021.124,
  author =	{Chatterjee, Krishnendu and Henzinger, Monika and Kale, Sagar Sudhir and Svozil, Alexander},
  title =	{{Faster Algorithms for Bounded Liveness in Graphs and Game Graphs}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{124:1--124:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.124},
  URN =		{urn:nbn:de:0030-drops-141930},
  doi =		{10.4230/LIPIcs.ICALP.2021.124},
  annote =	{Keywords: Graphs, Game Graphs, B\"{u}chi}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.23
Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.
Cite as

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 23:1-23:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2020.23,
  author =	{Chatterjee, Krishnendu and Henzinger, Thomas A. and Otop, Jan},
  title =	{{Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{23:1--23:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.23},
  URN =		{urn:nbn:de:0030-drops-128359},
  doi =		{10.4230/LIPIcs.CONCUR.2020.23},
  annote =	{Keywords: vector addition systems, mean-payoff, multidimension, probabilistic semantics}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.22
Simplified Game of Life: Algorithms and Complexity

Authors: Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Ismaël Jecker, and Jakub Svoboda

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
Game of Life is a simple and elegant model to study dynamical system over networks. The model consists of a graph where every vertex has one of two types, namely, dead or alive. A configuration is a mapping of the vertices to the types. An update rule describes how the type of a vertex is updated given the types of its neighbors. In every round, all vertices are updated synchronously, which leads to a configuration update. While in general, Game of Life allows a broad range of update rules, we focus on two simple families of update rules, namely, underpopulation and overpopulation, that model several interesting dynamics studied in the literature. In both settings, a dead vertex requires at least a desired number of live neighbors to become alive. For underpopulation (resp., overpopulation), a live vertex requires at least (resp. at most) a desired number of live neighbors to remain alive. We study the basic computation problems, e.g., configuration reachability, for these two families of rules. For underpopulation rules, we show that these problems can be solved in polynomial time, whereas for overpopulation rules they are PSPACE-complete.
Cite as

Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Ismaël Jecker, and Jakub Svoboda. Simplified Game of Life: Algorithms and Complexity. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 22:1-22:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.MFCS.2020.22,
  author =	{Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Jecker, Isma\"{e}l and Svoboda, Jakub},
  title =	{{Simplified Game of Life: Algorithms and Complexity}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{22:1--22:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.22},
  URN =		{urn:nbn:de:0030-drops-126903},
  doi =		{10.4230/LIPIcs.MFCS.2020.22},
  annote =	{Keywords: game of life, cellular automata, computational complexity, dynamical systems}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2019.21
The Evolutionary Price of Anarchy: Locally Bounded Agents in a Dynamic Virus Game

Authors: Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid

Published in: LIPIcs, Volume 153, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019)

Abstract
The Price of Anarchy (PoA) is a well-established game-theoretic concept to shed light on coordination issues arising in open distributed systems. Leaving agents to selfishly optimize comes with the risk of ending up in sub-optimal states (in terms of performance and/or costs), compared to a centralized system design. However, the PoA relies on strong assumptions about agents' rationality (e.g., resources and information) and interactions, whereas in many distributed systems agents interact locally with bounded resources. They do so repeatedly over time (in contrast to "one-shot games"), and their strategies may evolve. Using a more realistic evolutionary game model, this paper introduces a realized evolutionary Price of Anarchy (ePoA). The ePoA allows an exploration of equilibrium selection in dynamic distributed systems with multiple equilibria, based on local interactions of simple memoryless agents. Considering a fundamental game related to virus propagation on networks, we present analytical bounds on the ePoA in basic network topologies and for different strategy update dynamics. In particular, deriving stationary distributions of the stochastic evolutionary process, we find that the Nash equilibria are not always the most abundant states, and that different processes can feature significant off-equilibrium behavior, leading to a significantly higher ePoA compared to the PoA studied traditionally in the literature.
Cite as

Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid. The Evolutionary Price of Anarchy: Locally Bounded Agents in a Dynamic Virus Game. In 23rd International Conference on Principles of Distributed Systems (OPODIS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 153, pp. 21:1-21:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{schmid_et_al:LIPIcs.OPODIS.2019.21,
  author =	{Schmid, Laura and Chatterjee, Krishnendu and Schmid, Stefan},
  title =	{{The Evolutionary Price of Anarchy: Locally Bounded Agents in a Dynamic Virus Game}},
  booktitle =	{23rd International Conference on Principles of Distributed Systems (OPODIS 2019)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-133-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{153},
  editor =	{Felber, Pascal and Friedman, Roy and Gilbert, Seth and Miller, Avery},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2019.21},
  URN =		{urn:nbn:de:0030-drops-118071},
  doi =		{10.4230/LIPIcs.OPODIS.2019.21},
  annote =	{Keywords: Evolutionary Games, Virus Propagation, Price of Anarchy, Analysis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.6
Combinations of Qualitative Winning for Stochastic Parity Games

Authors: Krishnendu Chatterjee and Nir Piterman

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games.
Cite as

Krishnendu Chatterjee and Nir Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 6:1-6:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.6,
  author =	{Chatterjee, Krishnendu and Piterman, Nir},
  title =	{{Combinations of Qualitative Winning for Stochastic Parity Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.6},
  URN =		{urn:nbn:de:0030-drops-109089},
  doi =		{10.4230/LIPIcs.CONCUR.2019.6},
  annote =	{Keywords: Two Player Games, Stochastic Games, Parity Winning Conditions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.7
Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs

Authors: Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time O(min(n^2, m sqrt{m log n}) + b log n). In this work we present randomized near-linear time algorithms, with expected running time O~(m + b), where the O~ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors.
Cite as

Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil. Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 7:1-7:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.7,
  author =	{Chatterjee, Krishnendu and Dvo\v{r}\'{a}k, Wolfgang and Henzinger, Monika and Svozil, Alexander},
  title =	{{Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.7},
  URN =		{urn:nbn:de:0030-drops-109093},
  doi =		{10.4230/LIPIcs.CONCUR.2019.7},
  annote =	{Keywords: model checking, graph games, Streett games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.8
Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives

Authors: Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The window mechanism was introduced by Chatterjee et al. [Krishnendu Chatterjee et al., 2015] to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.
Cite as

Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 8:1-8:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.8,
  author =	{Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael},
  title =	{{Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.8},
  URN =		{urn:nbn:de:0030-drops-109103},
  doi =		{10.4230/LIPIcs.CONCUR.2019.8},
  annote =	{Keywords: Markov decision processes, window mean-payoff, window parity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.14
On the Complexity of Reachability in Parametric Markov Decision Processes

Authors: Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.
Cite as

Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 14:1-14:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{winkler_et_al:LIPIcs.CONCUR.2019.14,
  author =	{Winkler, Tobias and Junges, Sebastian and P\'{e}rez, Guillermo A. and Katoen, Joost-Pieter},
  title =	{{On the Complexity of Reachability in Parametric Markov Decision Processes}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.14},
  URN =		{urn:nbn:de:0030-drops-109162},
  doi =		{10.4230/LIPIcs.CONCUR.2019.14},
  annote =	{Keywords: Parametric Markov decision processes, Formal verification, ETR, Complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.27
Long-Run Average Behavior of Vector Addition Systems with States

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open.
Cite as

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Long-Run Average Behavior of Vector Addition Systems with States. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 27:1-27:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.27,
  author =	{Chatterjee, Krishnendu and Henzinger, Thomas A. and Otop, Jan},
  title =	{{Long-Run Average Behavior of Vector Addition Systems with States}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{27:1--27:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.27},
  URN =		{urn:nbn:de:0030-drops-109293},
  doi =		{10.4230/LIPIcs.CONCUR.2019.27},
  annote =	{Keywords: vector addition systems, mean-payoff, Diophantine inequalities}
}
  • Refine by Author
  • 29 Chatterjee, Krishnendu
  • 6 Ibsen-Jensen, Rasmus
  • 5 Henzinger, Monika
  • 5 Henzinger, Thomas A.
  • 4 Otop, Jan
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Logic and verification
  • 3 Software and its engineering → Formal software verification
  • 2 Theory of computation
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Graph algorithms analysis
  • Show More...

  • Refine by Keyword
  • 4 graph games
  • 4 mean-payoff
  • 3 complexity
  • 2 Complexity
  • 2 Graph algorithms
  • Show More...

  • Refine by Type
  • 33 document

  • Refine by Publication Year
  • 5 2017
  • 5 2019
  • 4 2016
  • 3 2013
  • 3 2020
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact