Search

• < Previous
• 1
• Next >

---

Aspect-oriented linearizability proofs

Soham Chakraborty ; Thomas A. Henzinger ; Ali Sezgin ; Viktor Vafeiadis.

Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency&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;]

---

Exact and Approximate Determinization of Discounted-Sum Automata

Udi Boker ; Thomas A. Henzinger.

A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, valuing a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by $\lambda^i$, where the discount factor $\lambda$ is a fixed rational number&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;]

---

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;]

---

Determinacy in Discrete-Bidding Infinite-Duration Games

Milad Aghajohari ; Guy Avni ; Thomas A. Henzinger.

In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players&nbsp;[&hellip;]

---

History-deterministic Timed Automata

Sougata Bose ; Thomas A. Henzinger ; Karoliina Lehtinen ; Sven Schewe ; Patrick Totzke.

We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits&nbsp;[&hellip;]

---