Search

• < Previous
• 1
• Next >

---

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

---

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

---

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

---