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 paper presents a novel algorithm for computing best and worst caseexecution times (BCET/WCET) of timed automata models with cyclic behaviour. Thealgorithms can work on any arbitrary diagonal-free TA and can handle more casesthan previously existing algorithms for BCET/WCET computations, as it canhandle cycles in TA and decide whether they lead to an infinite WCET. We showsoundness of the proposed algorithm and study its complexity. To our knowledge,this is the first model checking algorithm that addresses comprehensively theBCET/WCET problem of systems with cyclic behaviour. Behrmann et al. provide analgorithm for computing the minimum cost/time of reaching a goal state inpriced timed automata (PTA). The algorithm has been implemented in thewell-known model checking tool UPPAAL to compute the minimum time fortermination of an automaton. However, we show that in certain circumstances,when infinite cycles exist, the algorithm implemented in UPPAAL may notterminate, and we provide examples which UPPAAL fails to verify.

Finding Minimum and Maximum Termination Time of Timed Automata Models with Cyclic Behaviour