4 results
Erich Graedel ; Igor Walukiewicz.
We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two […]
Published on November 3, 2006
Pawel Parys ; Igor Walukiewicz.
Alternating timed automata on infinite words are considered. The main result is a characterization of acceptance conditions for which the emptiness problem for these automata is decidable. This result implies new decidability results for fragments of timed temporal logics. It is also shown that, […]
Published on September 19, 2012
Mikolaj Bojanczyk ; Igor Walukiewicz ; Howard Straubing.
We use the recently developed theory of forest algebras to find algebraic characterizations of the languages of unranked trees and forests definable in various logics. These include the temporal logics CTL and EF, and first-order logic over the ancestor relation. While the characterizations are in […]
Published on September 19, 2012
Sylvain Salvati ; Igor Walukiewicz.
We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose the use of a model of lambda-Y-calculus to discriminate the terms that satisfy a given […]
Published on June 11, 2015