ﻻ يوجد ملخص باللغة العربية
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.
In this paper, we study the parameter synthesis problem for a class of parametric timed automata. The problem asks to construct the set of valuations of the parameters in the parametric timed automa- ton, referred to as the feasible region, under whi
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 ti
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
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, i
We consider the parameter synthesis problem of parametric timed automata (PTAs). The problem is, given a PTA and a property, to compute the set of valuations of the parameters under which the resulting timed automaton satisfies the property. Such a s