3 years ago

# LTL Semantic Tableaux and Alternating $\omega$-automata via Linear Factors.

Peter Thiemann, Martin Sulzmann

Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable $\omega$-automata and then applying model checking.

We revisit Vardi's transformation of an LTL formula to an alternating $\omega$-automaton and Wolper's LTL tableau method for satisfiability checking. We observe that both constructions effectively rely on a decomposition of formulae into linear factors.

Linear factors have been introduced previously by Antimirov in the context of regular expressions.

We establish the notion of linear factors for LTL and verify essential properties such as expansion and finiteness.

Our results shed new insights on the connection between the construction of alternating $\omega$-automata and semantic tableaux.

Publisher URL: http://arxiv.org/abs/1710.06678

DOI: arXiv:1710.06678v1

You might also like
Discover & Discuss Important Research

Keeping up-to-date with research can feel impossible, with papers being published faster than you'll ever be able to read them. That's where Researcher comes in: we're simplifying discovery and making important discussions happen. With over 19,000 sources, including peer-reviewed journals, preprints, blogs, universities, podcasts and Live events across 10 research areas, you'll never miss what's important to you. It's like social media, but better. Oh, and we should mention - it's free.

Researcher displays publicly available abstracts and doesn’t host any full article content. If the content is open access, we will direct clicks from the abstracts to the publisher website and display the PDF copy on our platform. Clicks to view the full text will be directed to the publisher website, where only users with subscriptions or access through their institution are able to view the full article.