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

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

This paper presents the first model-checking algorithm for an expressivemodal mu-calculus over timed automata, $L^{\mathit{rel},\mathit{af}}_{\nu,\mu}$, and reports performance results for an implementation.This mu-calculus contains extended time-modality operators and can express allof TCTL. Our algorithmic approach uses an "on-the-fly" strategy based on proofsearch as a means of ensuring high performance for both positive and negativeanswers to model-checking questions. In particular, a set of proof rules forsolving model-checking problems are given and proved sound and complete; weencode our algorithm in these proof rules and model-check a property byconstructing a proof (or showing none exists) using these rules. One noteworthyaspect of our technique is that we show that verification performance can beimproved with \emph{derived rules}, whose correctness can be inferred from themore primitive rules on which they are based. In this paper, we give the basicproof rules underlying our method, describe derived proof rules to improveperformance, and compare our implementation of this model checker to the UPPAALtool.

The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix)