4 results
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 […]
Published on April 1, 2015
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 […]
Published on December 14, 2011
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 […]
Published on February 3, 2021
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 […]
Published on August 13, 2019