Improving the construction of the DBM over approximation of the state spce of real-time preemptive systems

We present in this paper an algorithm allowing an efficient computation of the tightest DBM over-approximation of the state space of preemptive systems modeled by using Time Petri Nets with inhibitor arcs. First of all, we propose an algorithm that reduces the effort of computing the tightest DBM ov...

Teljes leírás

Elmentve itt :
Bibliográfiai részletek
Szerző: Abdelkrim Abdelli
Dokumentumtípus: Cikk
Megjelent: 2012
Sorozat:Acta cybernetica 20 No. 3
Kulcsszavak:Számítástechnika, Kibernetika, Matematika
Tárgyszavak:
doi:10.14232/actacyb.20.3.2012.1

Online Access:http://acta.bibl.u-szeged.hu/30836
LEADER 01989nab a2200241 i 4500
001 acta30836
005 20220617142329.0
008 161017s2012 hu o 0|| eng d
022 |a 0324-721X 
024 7 |a 10.14232/actacyb.20.3.2012.1  |2 doi 
040 |a SZTE Egyetemi Kiadványok Repozitórium  |b hun 
041 |a eng 
100 1 |a Abdelkrim Abdelli 
245 1 0 |a Improving the construction of the DBM over approximation of the state spce of real-time preemptive systems  |h [elektronikus dokumentum] /  |c  Abdelkrim Abdelli 
260 |c 2012 
300 |a 347-384 
490 0 |a Acta cybernetica  |v 20 No. 3 
520 3 |a We present in this paper an algorithm allowing an efficient computation of the tightest DBM over-approximation of the state space of preemptive systems modeled by using Time Petri Nets with inhibitor arcs. First of all, we propose an algorithm that reduces the effort of computing the tightest DBM over-approximated graph. For this effect, each class of this graph is expressed as a pair (M, D), where M is a marking and D is the system of all DBM inequalities even the redundant ones. We thereby make it possible to compute the system D straightforwardly in its normal form, without requiring to compute the intermediary polyhedra. Hence, we succeed to remove the errors reported in the implementation of other DBM approximations. Then we show that by relaxing a bit in the precision of the DBM approximation, we can achieve to construct more compact graphs while reducing still more the cost of their computation. We provide for this abstraction a suitable equivalence relation that contract yet more the graphs. The experimental results comparing the defined constructions with other approaches are reported. 
650 4 |a Természettudományok 
650 4 |a Matematika 
650 4 |a Számítás- és információtudomány 
695 |a Számítástechnika, Kibernetika, Matematika 
856 4 0 |u http://acta.bibl.u-szeged.hu/30836/1/actacyb_20_3_2012_1.pdf  |z Dokumentum-elérés