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

Given a model of a system and an objective, the model-checking question askswhether the model satisfies the objective. We study polynomial-time problems intwo classical models, graphs and Markov Decision Processes (MDPs), with respectto several fundamental $\omega$-regular objectives, e.g., Rabin and Streettobjectives. For many of these problems the best-known upper bounds arequadratic or cubic, yet no super-linear lower bounds are known. In this workour contributions are two-fold: First, we present several improved algorithms,and second, we present the first conditional super-linear lower bounds based onwidely believed assumptions about the complexity of CNF-SAT and combinatorialBoolean matrix multiplication. A separation result for two models with respectto an objective means a conditional lower bound for one model that is strictlyhigher than the existing upper bound for the other model, and similarly for twoobjectives with respect to a model. Our results establish the followingseparation results: (1) A separation of models (graphs and MDPs) fordisjunctive queries of reachability and B\"uchi objectives. (2) Two kinds ofseparations of objectives, both for graphs and MDPs, namely, (2a) theseparation of dual objectives such as reachability/safety (for disjunctivequestions) and Streett/Rabin objectives, and (2b) the separation of conjunctionand disjunction of multiple objectives of the same type such as safety,B\"uchi, and coB\"uchi. In summary, our results establish the first model andobjective separation results for graphs and MDPs for various classical$\omega$-regular objectives. Quite strikingly, we establish conditional lowerbounds for the disjunction of objectives that are strictly higher than theexisting upper bounds for the conjunction of the same objectives.

Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction