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

Abdelkrim, Abdelli: Improving the construction of the DBM over approximation of the state spce of real-time preemptive systems. In: Acta cybernetica, (20) 3. pp. 347-384. (2012)

[img]
Preview
Cikk, tanulmány, mű
actacyb_20_3_2012_1.pdf

Download (546kB) | Preview

Abstract

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.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2012
Volume: 20
Number: 3
ISSN: 0324-721X
Page Range: pp. 347-384
Language: angol
DOI: https://doi.org/10.14232/actacyb.20.3.2012.1
Uncontrolled Keywords: Természettudomány, Matematika
Additional Information: Bibliogr.: p. 383-384. és a lábjegyzetekben; Abstract
Date Deposited: 2016. Oct. 17. 10:38
Last Modified: 2018. Jun. 05. 14:26
URI: http://acta.bibl.u-szeged.hu/id/eprint/30836

Actions (login required)

View Item View Item