دانلود مقاله ISI انگلیسی شماره 78594
عنوان فارسی مقاله

TCTL-حفظ ترجمه از شبکه های پتری timed-arc به شبکه های اتوماسیون زمان

کد مقاله سال انتشار مقاله انگلیسی ترجمه فارسی تعداد کلمات
78594 2014 26 صفحه PDF سفارش دهید محاسبه نشده
خرید مقاله
پس از پرداخت، فوراً می توانید مقاله را دانلود فرمایید.
عنوان انگلیسی
TCTL-preserving translations from timed-arc Petri nets to networks of timed automata
منبع

Publisher : Elsevier - Science Direct (الزویر - ساینس دایرکت)

Journal : Theoretical Computer Science, Volume 537, 5 June 2014, Pages 3–28

کلمات کلیدی
تأیید رسمی؛ TCTL؛ شبکه های پتری Timed-arc؛ اتوماسیون زمان
پیش نمایش مقاله
پیش نمایش مقاله TCTL-حفظ ترجمه از شبکه های پتری timed-arc به شبکه های اتوماسیون زمان

چکیده انگلیسی

We present a framework for TCTL-preserving translations between time-dependent modeling formalisms. The framework guarantees that once the original and the translated system are in one-by-many correspondence relation (a notion of behavioral equivalence between timed transition systems) then TCTL properties of the original system can be transformed too while preserving the verification answers. We demonstrate the usability of the technique on two reductions from bounded timed-arc Petri nets to networks for timed automata, providing unified proofs of the translations implemented in the verification tool TAPAAL. We evaluate the efficiency of the approach on a number of experiments: alternating bit protocol, Fischer's protocol, Lynch–Shavit protocol, MPEG-2 encoder, engine workshop and medical workflow. The results are encouraging and confirm the practical applicability of the approach.

خرید مقاله
پس از پرداخت، فوراً می توانید مقاله را دانلود فرمایید.