Extending Temporal Logic with Omega-automata

More about the book

Focusing on automata theoretic techniques, the book explores their application in model checking and satisfiability for advanced extensions of LTL, particularly in hardware design specifications. It highlights Intel's development of ForSpec, a specification language that expands LTL, and discusses the integration of automata in its backend translation tool. The study emphasizes the renewed interest in automata connectives and the effective use of alternating automata in this context, providing insights into their role in enhancing hardware model checking.