Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTimed Comparisons of Semi-Markov Processes
57
0
0.0
(
0
)
Added by
Mathias Ruggaard Pedersen
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Semi-Markov processes are Markovian processes in which the firing time of the transitions is modelled by probabilistic distributions over positive reals interpreted as the probability of firing a transition at a certain moment in time. In this paper we consider the trace-based semantics of semi-Markov processes, and investigate the question of how to compare two semi-Markov processes with respect to their time-dependent behaviour. To this end, we introduce the relation of being faster than between processes and study its algorithmic complexity. Through a connection to probabilistic automata we obtain hardness results showing in particular that this relation is undecidable. However, we present an additive approximation algorithm for a time-bounded variant of the faster-than problem over semi-Markov processes with slow residence-time functions, and a coNP algorithm for the exact faster-than problem over unambiguous semi-Markov processes.
rate research
Read More
When modeling concurrent or cyber-physical systems, non-functional requirements such as time are important to consider. In order to improve the timing aspects of a model, it is necessary to have some notion of what it means for a process to be faster than another, which can guide the stepwise refinement of the model. To this end we study a faster-than relation for semi-Markov decision processes and compare it to standard notions for relating systems. We consider the compositional aspects of this relation, and show that the faster-than relation is not a precongruence with respect to parallel composition, hence giving rise to so-called parallel timing anomalies. We take the first steps toward understanding this problem by identifying decidable conditions sufficient to avoid parallel timing anomalies in the absence of non-determinism.
We consider Markov decision processes (MDP) as generators of sequences of probability distributions over states. A probability distribution is p-synchronizing if the probability mass is at least p in a single state, or in a given set of states. We consider four temporal synchronizing modes: a sequence of probability distributions is always p-synchronizing, eventually p-synchronizing, weakly p-synchronizing, or strongly p-synchronizing if, respectively, all, some, infinitely many, or all but finitely many distributions in the sequence are p-synchronizing. For each synchronizing mode, an MDP can be (i) sure winning if there is a strategy that produces a 1-synchronizing sequence; (ii) almost-sure winning if there is a strategy that produces a sequence that is, for all epsilon > 0, a (1-epsilon)-synchronizing sequence; (iii) limit-sure winning if for all epsilon > 0, there is a strategy that produces a (1-epsilon)-synchronizing sequence. We provide fundamental results on the expressiveness, decidability, and complexity of synchronizing properties for MDPs. For each synchronizing mode, we consider the problem of deciding whether an MDP is sure, almost-sure, or limit-sure winning, and we establish matching upper and lower complexity bounds of the problems: for all winning modes, we show that the problems are PSPACE-complete for eventually and weakly synchronizing, and PTIME-complete for always and strongly synchronizing. We establish the memory requirement for winning strategies, and we show that all winning modes coincide for always synchronizing, and that the almost-sure and limit-sure winning modes coincide for weakly and strongly synchronizing.
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.
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.
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
