Search

• < Previous
• 1
• Next >

---

Using models to model-check recursive schemes

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&nbsp;[&hellip;]

---

Weak Alternating Timed Automata

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,&nbsp;[&hellip;]

---

Wreath Products of Forest Algebras, with Applications to Tree Logics

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&nbsp;[&hellip;]

---