Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userComputing Maximal Expected Termination Time of Probabilistic Timed Automata
159
0
0.0
(
0
)
Added by
Omar Al-Bataineh I.
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The paper addresses the problem of computing maximal expected time to termination of probabilistic timed automata (PTA) models, under the condition that the system will, eventually, terminate. This problem can exhibit high computational complexity, in particular when the automaton under analysis contains cycles that may be repeated very often (due to very high probabilities, e.g. p =0.999). Such cycles can degrade the performance of typical model checking algorithms, as the likelihood of repeating the cycle converges to zero arbitrarily slowly. We introduce an acceleration technique that can be applied to improve the execution of such cycles by collapsing their iterations. The acceleration process of a cyclic PTA consists of several formal steps necessary to handle the cumulative timing and probability information that result from successive executions of a cycle. The advantages of acceleration are twofold. First, it helps to reduce the computational complexity of the problem without adversely affecting the outcome of the analysis. Second, it can bring the worst case execution time problem of PTAs within the bounds of feasibility for model checking techniques. To our knowledge, this is the first work that addresses the problem of accelerating execution of cycles that exhibit both timing and probabilistic behavior.
rate research
Read More
The paper presents a novel algorithm for computing best and worst case execution times (BCET/WCET) of timed automata models with cyclic behaviour. The algorithms can work on any arbitrary diagonal-free TA and can handle more cases than previously existing algorithms for BCET/WCET computations, as it can handle cycles in TA and decide whether they lead to an infinite WCET. We show soundness of the proposed algorithm and study its complexity. To our knowledge, this is the first model checking algorithm that addresses comprehensively the BCET/WCET problem of systems with cyclic behaviour. Behrmann et al. provide an algorithm for computing the minimum cost/time of reaching a goal state in priced timed automata (PTA). The algorithm has been implemented in the well-known model checking tool UPPAAL to compute the minimum time for termination of an automaton. However, we show that in certain circumstances, when infinite cycles exist, the algorithm implemented in UPPAAL may not terminate, and we provide examples which UPPAAL fails to verify.
The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynchs probabilistic bisimilarity for probabilistic automata. In this paper, we present a characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condons simple policy iteration on these games. The correctness of Condons approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in $textbf{UP} cap textbf{coUP}$ and textbf{PPAD}. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. The characterization of the probabilistic bisimilarity distance mentioned above crucially uses a dual presentation of the Hausdorff distance due to Memoli. As an additional contribution, in this paper we show that Memolis result can be used also to prove that the bisimilarity distance bounds the difference in the maximal (or minimal) probability of two states to satisfying arbitrary $omega$-regular properties, expressed, eg., as LTL formulas.
Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in particular, a state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models. In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and an associated maximally-permissive strategy) in acyclic timed automata and games.
We consider a notion of non-interference for timed automata (TAs) that allows to quantify the frequency of an attack; that is, we infer values of the minimal time between two consecutive actions of the attacker, so that (s)he disturbs the set of reachable locations. We also synthesize valuations for the timing constants of the TA (seen as parameters) guaranteeing non-interference. We show that this can reduce to reachability synthesis in parametric timed automata. We apply our method to a model of the Fischer mutual exclusion protocol and obtain preliminary results.
Model checking timed automata becomes increasingly complex with the increase in the number of clocks. Hence it is desirable that one constructs an automaton with the minimum number of clocks possible. The problem of checking whether there exists a timed automaton with a smaller number of clocks such that the timed language accepted by the original automaton is preserved is known to be undecidable. In this paper, we give a construction, which for any given timed automaton produces a timed bisimilar automaton with the least number of clocks. Further, we show that such an automaton with the minimum possible number of clocks can be constructed in time that is doubly exponential in the number of clocks of the original automaton.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
