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 goal of the thesis is to leverage fast graph algorithms and modernalgorithmic techniques for problems in model checking and synthesis on graphs,MDPs, and game graphs. The results include symbolic algorithms, a well-knownclass of algorithms in model checking that trades limited access to the inputmodel for an efficient representation. In particular, we present the followingresults: Algorithms for game graphs with mean-payoff B\"uchi objectives andmean-payoff coB\"uchi objectives which match one of the best running timebounds for mean-payoff objectives. A near-linear time randomized algorithm forStreett objectives in graphs and MDPs. A sub-cubic time algorithm for boundedB\"uchi objectives in graphs and a cubic time algorithm for game graphs.Conditional lower bounds for queries of reachability objectives in game graphsand MDPs. Linear and near-linear time algorithms for sequential reachabilityobjectives in graphs and MDPs respectively. The first quasi-polynomial timesymbolic algorithm for parity objectives in game graphs. We break along-standing running time bound for MEC decomposition from the '90s byproviding a sub-quadratic time symbolic algorithm.

Leveraging the Power of Graph Algorithms: Efficient Algorithms for Computer-Aided Verification