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/

Global: Zendy Plus annual

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

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The standard technique for LTL model checking (M ϕ) consists on translating the negation of the LTL specification, ϕ, into a B¨ uchi automaton Aϕ, and then on checking if the product M Aϕ has an empty language. The efforts to maximize the efficiency of this process have so far concentrated on developing translation algorithms producing B¨ uchi automata which are "as small as possible", under the implicit conjecture that this fact should make the final product smaller. In this paper we build on a different conjecture and present an alternative approach in which we generate instead B¨ uchi automata which are "as deterministic as possible", in the sense that we try to reduce as much as we are able to the presence of non-deterministic decision states in Aϕ. We motivate our choice and present some empirical tests to support this approach.

“More Deterministic” vs. “Smaller” Büchi Automata for Efficient LTL Model Checking