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 Tools annual

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 Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Complementation of nondeterministic B\"uchi automata (BAs) is an importantproblem in automata theory with numerous applications in formal verification,such as termination analysis of programs, model checking, or in decisionprocedures of some logics. We build on ideas from a recent work on BAdeterminization by Li et al. and propose a new modular algorithm for BAcomplementation. Our algorithm allows to combine several BA complementationprocedures together, with one procedure for a subset of the BA's stronglyconnected components (SCCs). In this way, one can exploit the structure ofparticular SCCs (such as when they are inherently weak or deterministic) anduse more efficient specialized algorithms, regardless of the structure of thewhole BA. We give a general framework into which partial complementationprocedures can be plugged in, and its instantiation with several algorithms.The framework can, in general, produce a complement with an Emerson-Leiacceptance condition, which can often be more compact. Using the algorithm, wewere able to establish an exponentially better new upper bound of $O(4n)$ forcomplementation of the recently introduced class of elevator automata. Weimplemented the algorithm in a prototype and performed a comprehensive set ofexperiments on a large set of benchmarks, showing that our frameworkcomplements well the state of the art and that it can serve as a basis forfuture efficient BA complementation and inclusion checking algorithms.

Modular Mix-and-Match Complementation of B\"{u}chi Automata (Technical Report)