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 addresses the problem of computing maximal expected time totermination of probabilistic timed automata (PTA) models, under the conditionthat the system will, eventually, terminate. This problem can exhibit highcomputational complexity, in particular when the automaton under analysiscontains cycles that may be repeated very often (due to very highprobabilities, e.g. p =0.999). Such cycles can degrade the performance oftypical model checking algorithms, as the likelihood of repeating the cycleconverges to zero arbitrarily slowly. We introduce an acceleration techniquethat can be applied to improve the execution of such cycles by collapsing theiriterations. The acceleration process of a cyclic PTA consists of several formalsteps necessary to handle the cumulative timing and probability informationthat result from successive executions of a cycle. The advantages ofacceleration are twofold. First, it helps to reduce the computationalcomplexity of the problem without adversely affecting the outcome of theanalysis. Second, it can bring the "worst case execution time" problem of PTAswithin the bounds of feasibility for model checking techniques. To ourknowledge, this is the first work that addresses the problem of acceleratingexecution of cycles that exhibit both timing and probabilistic behavior.

Computing Maximal Expected Termination Time of Probabilistic Timed Automata