Search

• < Previous
• 1
• 2
• Next >

---

Algorithms for Game Metrics

Krishnendu Chatterjee ; Luca de Alfaro ; Rupak Majumdar ; Vishwanath Raman.

Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative {\mu}-calculus and related&nbsp;[&hellip;]

---

Qualitative Logics and Equivalences for Probabilistic Systems

Krishnendu Chatterjee ; Luca de Alfaro ; Marco Faella ; Axel Legay.

We investigate logics and equivalence relations that capture the qualitative behavior of Markov Decision Processes (MDPs). We present Qualitative Randomized CTL (QRCTL): formulas of this logic can express the fact that certain temporal properties hold over all paths, or with probability 0 or 1, but&nbsp;[&hellip;]

---

Expressiveness and Closure Properties for Quantitative Languages

Krishnendu Chatterjee ; Laurent Doyen ; Thomas A Henzinger.

Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages~$L$ that assign to each word~$w$ a real number~$L(w)$. In the case of infinite words, the value of a run is naturally computed as the maximum, limsup, liminf, limit-average,&nbsp;[&hellip;]

---

Algorithms for Omega-Regular Games with Imperfect Information

Krishnendu Chatterjee ; Laurent Doyen ; Thomas A. Henzinger ; Jean-Francois Raskin.

We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller&nbsp;[&hellip;]

---

Timed Parity Games: Complexity and Robustness

Krishnendu Chatterjee ; Thomas A. Henzinger ; Vinayak S. Prabhu.

We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are \emph{concurrent} in that at each turn, both players independently propose a time delay and an action, and the action with the shorter&nbsp;[&hellip;]

---

Markov Decision Processes with Multiple Long-run Average Objectives

Tomáš Brázdil ; Václav Brožek ; Krishnendu Chatterjee ; Vojtěch Forejt ; Antonín Kučera.

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 k limit-average functions, in the expectation objective the goal is to maximize the expected&nbsp;[&hellip;]

---

Quantitative Automata under Probabilistic Semantics

Krishnendu Chatterjee ; Thomas A. Henzinger ; Jan Otop.

Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor&nbsp;[&hellip;]

---

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

Krishnendu Chatterjee ; Zuzana Křetínská ; Jan Křetínský.

We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize&nbsp;[&hellip;]

---

Improved Algorithms for Parity and Streett objectives

Krishnendu Chatterjee ; Monika Henzinger ; Veronika Loitzenbauer.

The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems,&nbsp;[&hellip;]

---

Edit Distance for Pushdown Automata

Krishnendu Chatterjee ; Thomas A. Henzinger ; Rasmus Ibsen-Jensen ; Jan Otop.

The edit distance between two words $w_1, w_2$ is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform $w_1$ to $w_2$. The edit distance generalizes to languages $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to&nbsp;[&hellip;]

---