Wyniki wyszukiwania - BazTech

1

Probabilistic Timed Automata with Clock-Dependent Probabilities

Sproston Jeremy

Fundamenta Informaticae

|

2021

|

Vol. 178, nr 1/2

101--138

EN

Probabilistic timed automata are classical timed automata extended with discrete probability distributions over edges. We introduce clock-dependent probabilistic timed automata, a variant of probabilistic timed automata in which transition probabilities can depend linearly on clock values. Clock-dependent probabilistic timed automata allow the modelling of a continuous relationship between time passage and the likelihood of system events. We show that the problem of deciding whether the maximum probability of reaching a certain location is above a threshold is undecidable for clock-dependent probabilistic timed automata. On the positive side, we show that the maximum and minimum probability of reaching a certain location in clock-dependent probabilistic timed automata can be approximated using a region-graph-based approach.

2

Diagnosis of hybrid systems through bond graph, observers and timed automata

Mhamdi Lotfi, Achbi Mohammed Said, Dhouibi Hedi, Kechida Sihem

Diagnostyka

|

2020

|

Vol. 21, No. 3

113--125

EN

Despite technological advances and progress in industrial systems, the fault diagnosis of a system remains a very important task. In fact an effective diagnosis contributes not only to improved reliability but also to a decrease in maintenance costs. This paper presents an approach to a diagnosis of hybrid systems thanks to the use of Bond Graphs, Observer and Timed Automata. Dynamic models (in normal and failing mode) are generated by an observer based methods as well as through state equations generated by the Bond Graphs model. The procedure of fault localization through a method based on the observer does not allow locating faults with the same signature of failure. Thus the diagnosis technique for the localization of these defects will be based on the time analysis using Timed Automata. The proposed approach is then validated by simulation tests in a two tanks hydraulic system.

3

Robustness of Time Petri Nets under Guard Enlargement

Akshay S., Jard C., Hélouët L., Reynier P.-A.

Fundamenta Informaticae

|

2016

|

Vol. 143, nr 3/4

207--234

EN

Robustness of timed systems aims at studying whether infinitesimal perturbations in clock values can result in new discrete behaviors. A model is robust if the set of discrete behaviors is preserved under arbitrarily small (but positive) perturbations. We tackle this problem for time Petri nets (TPNs, for short) by considering the model of parametric guard enlargement which allows time-intervals constraining the firing of transitions in TPNs to be enlarged by a (positive) parameter. We show that TPNs are not robust in general and checking if they are robust with respect to standard properties (such as boundedness, safety) is undecidable. We then extend the marking class timed automaton construction for TPNs to a parametric setting, and prove that it is compatible with guard enlargements. We apply this result to the (undecidable) class of TPNs which are robustly bounded (i.e., whose finite set of reachable markings remains finite under infinitesimal perturbations): we provide two decidable robustly bounded subclasses, and show that one can effectively build a timed automaton which is timed bisimilar even in presence of perturbations. This allows us to apply existing results for timed automata to these TPNs and show further robustness properties.

4

Relating Reachability Problems in Timed and Counter Automata

Haase C., Ouaknine J., Worrell J.

Fundamenta Informaticae

|

2016

|

Vol. 143, nr 3/4

317--338

EN

We establish a relationship between reachability problems in timed automata and spacebounded counter automata. We show that reachability in timed automata with three or more clocks is logarithmic-space inter-reducible with reachability in space-bounded counter automata with two counters. We moreover show the logarithmic-space equivalence of reachability in two-clock timed automata and space-bounded one-counter automata. This last reduction has recently been employed by Fearnley and Jurdziński to settle the computational complexity of reachability in two-clock timed automata.

5

SAT-based searching for k-quasi-optimal runs in weighted timed automata

Woźna-Szcześniak B., Zbrzezny A.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2010

|

Vol. 15

163--176

EN

In the paper we are concerned with an optimal cost reachability problem for weighted timed automata, and we use a translation to SAT to solve the problem. In particular, we show how to find a run of length k ∈ IN that starts at the initial state and terminates at a state containing a target location, its total cost belongs to the interval [c,c+1), for some natural number c ∈ IN, and the cost of each other run of length k, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of runs is called k-quasi-optimal. We exemplify the use of our solution to the mentioned problem by means of the air traffic control problem, and we provide some preliminary experimental results.