English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Linear Temporal Logic (LTL) is a widely used specification framework forlinear time properties of systems. The standard approach for verifying suchproperties is by transforming LTL formulae to suitable $\omega$-automata andthen 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 offormulae into linear factors.  Linear factors have been introduced previously by Antimirov in the context ofregular expressions.  We establish the notion of linear factors for LTL and verify essentialproperties such as expansion and finiteness.  Our results shed new insights on the connection between the construction ofalternating $\omega$-automata and semantic tableaux.

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