Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
2 results

Effective Characterizations of Simple Fragments of Temporal Logic Using Carton--Michel Automata

Preugschat Sebastian ; Thomas Wilke.
We present a framework for obtaining effective characterizations of simple fragments of future temporal logic (LTL) with the natural numbers as time domain. The framework is based on a form of strongly unambiguous automata, also known as prophetic automata or complete unambiguous B\"uchi automata&nbsp;[&hellip;]
Published on June 21, 2013
Volume 9, Issue 2

Unifying B\"uchi Complementation Constructions

Seth J. Fogarty ; Orna Kupferman ; Thomas Wilke ; Moshe Y. Vardi.
Complementation of B\"uchi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that&nbsp;[&hellip;]
Published on March 27, 2013
Volume 9, Issue 1
  • < Previous
  • 1
  • Next >