ݺߣ

ݺߣShare a Scribd company logo

شبکه‌های پتری

•
•
Mahdi Dolati
Mahdi Dolati

معرفی مختصری بر شبکه‌های پتری و بیان رسمی ساختار و رفتار آنها، همچنین افزونه‌های شبکه‌های پتری شامل انواع جدید یال و افزودن زمان

1 of 40
Downloaded 132 times
‫ایتĬīهĬīشبکĬīریĬ
‫معرفی‬ •‫شده‬ ‫توزیع‬ ‫های‬‫سیستم‬ ‫سازی‬‫مدل‬ ‫زبان‬ •‫نمایش‬ ‫برای‬ ‫گرافیکی‬ ‫مدل‬ ‫دارای‬ •‫در‬ ‫پتری‬ ‫آدام‬ ‫کارل‬۱۹۳۹ •‫شیمیایی‬ ‫های‬‫فرایند‬ Mahdi Dolati Verification of Reactive Systems 2
‫مدل‬ ‫استاتیک‬ •‫دار‬‫وزن‬ ‫بخشی‬ ‫دو‬ ‫و‬ ‫دار‬‫جهت‬ ‫گراف‬ ‫یک‬ Mahdi Dolati Verification of Reactive Systems 3
‫مدل‬ ‫استاتیک‬ •‫پتری‬ ‫ی‬‫شبکه‬ •‫مکان‬ •‫انتقال‬ Mahdi Dolati Verification of Reactive Systems 4
‫مدل‬ ‫استاتیک‬ •‫شده‬ ‫گذاری‬‫نشان‬ ‫پتری‬ ‫ی‬‫شبکه‬ •‫توکن‬ Mahdi Dolati Verification of Reactive Systems 5
‫مدل‬ ‫استاتیک‬ •‫شده‬ ‫گذاری‬‫نشان‬ ‫پتری‬ ‫ی‬‫شبکه‬ M0 = (0, 1, 1) Mahdi Dolati Verification of Reactive Systems 6
‫مدل‬ ‫استاتیک‬ ‫رسمی‬ ‫بیان‬ •‫ی‬‫شبکه‬N = (P, T, F) •‫های‬‫مکان‬ ‫ی‬‫مجموعه‬P‫های‬‫انتقال‬ ‫و‬T‫که‬𝑃 ∩ 𝑇 = ϕ •‫های‬‫یال‬ ‫مجموعه‬F‫که‬𝐹 ⊆ 𝑃 × 𝑇 ∪ 𝑇 × 𝑃 •‫پتری‬ ‫ی‬‫شبکه‬PN = (N, M, W) •N‫است‬ ‫شبکه‬ ‫یک‬ •𝑀: 𝑃 → ℕ‫مکان‬ ‫هر‬ ‫توکن‬ ‫تعداد‬ •𝑊: 𝐹 → ℕ‫یال‬ ‫هر‬ ‫وزن‬ Mahdi Dolati Verification of Reactive Systems 7
‫مدل‬ ‫رفتار‬ •‫فعال‬ ‫های‬‫انتقال‬ •‫شرط‬ ،‫ها‬‫محل‬–‫ها‬‫رخداد‬ ،‫ها‬‫انتقال‬ Mahdi Dolati Verification of Reactive Systems 8
‫مدل‬ ‫رفتار‬ •‫انتقال‬ ‫یک‬ ‫کردن‬ ‫عمل‬ •‫غیرقطعی‬ Mahdi Dolati Verification of Reactive Systems 9
‫مدل‬ ‫رفتار‬ •‫انتقال‬ ‫یک‬ ‫کردن‬ ‫عمل‬ •‫غیرقطعی‬ Mahdi Dolati Verification of Reactive Systems 10
‫مدل‬ ‫رفتار‬ ‫رسمی‬ ‫بیان‬ •‫انتقال‬ ‫برای‬t • 𝑡− 𝑝 = 𝑊 𝑝, 𝑡 , 𝑖𝑓𝑓 𝑝, 𝑡 ∈ 𝐹 0 , 𝑖𝑓𝑓 𝑝, 𝑡 ∉ 𝐹 • 𝑡+ 𝑝 = 𝑊 𝑡, 𝑝 , 𝑖𝑓𝑓 𝑡, 𝑝 ∈ 𝐹 0 , 𝑖𝑓𝑓 𝑡, 𝑝 ∉ 𝐹 p t pt W(p, t) W(p, t) Mahdi Dolati Verification of Reactive Systems 11
‫رسمی‬ ‫بیان‬‫مدل‬ ‫رفتار‬ •‫انتقال‬t‫است‬ ‫فعال‬ • ∀𝑝: 𝑃 ∙ 𝑡− 𝑝 ≤ 𝑀 𝑝 •‫انتقال‬t‫کند‬‫می‬ ‫عمل‬ • ∀𝑝: 𝑃 ∙ 𝑀′ 𝑝 = 𝑀 𝑝 − 𝑡− 𝑝 + 𝑡+ 𝑝 •‫با‬𝑀 → 𝑡 𝑀′‫دهیم‬‫می‬ ‫نشان‬ Mahdi Dolati Verification of Reactive Systems 12
‫عملیاتی‬ ‫معنای‬ •‫گام‬ ‫یک‬ ‫در‬ ‫پذیری‬‫دسترس‬𝑀 → 𝑡 𝑀′ •‫پذیری‬‫دسترس‬𝑀 →∗ 𝑀′ (‫متعدی‬ ‫بازتابی‬ ‫بستار‬→ 𝑡 ) • 𝑅 𝑁 ≜ {𝑀′ |𝑀0 →∗ 𝑀′ } •‫ی‬‫رابطه‬→ 𝑡 ‫روی‬ ‫بر‬ ‫شده‬ ‫محدود‬𝑅 𝑁 •‫حالت‬ ‫فضای‬ Mahdi Dolati Verification of Reactive Systems 13
‫عملیاتی‬ ‫معنای‬(‫مثال‬) Mahdi Dolati Verification of Reactive Systems 14
‫ریاضیاتی‬ ‫های‬‫ویژگی‬ •‫باال‬ ‫پذیری‬ ‫تحلیل‬ •‫ها‬‫ویژگی‬ ‫از‬ ‫بسیاری‬ ‫اتوماتیک‬ ‫تعیین‬ •‫پذیری‬‫دسترس‬ •‫بودن‬ ‫زنده‬ •‫داری‬‫کران‬ •‫بست‬‫بن‬ Mahdi Dolati Verification of Reactive Systems 15
‫پذیری‬‫دسترس‬ •‫صحت‬ ‫تعیین‬𝑀 ∈ 𝑅(𝑁) •‫نمایی‬ ‫فضایی‬ ‫پیچیدگی‬[L76] •‫خطادار‬ ‫های‬‫حالت‬ ‫کردن‬ ‫پیدا‬ •‫دارد‬ ‫ادامه‬ ‫ی‬‫بهینه‬ ‫ی‬‫محاسبه‬ ‫برای‬ ‫تحقیقات‬ •‫دیگر‬ ‫های‬‫روش‬ Mahdi Dolati Verification of Reactive Systems 16
‫بودن‬ ‫زنده‬ •‫عمل‬ ‫توالی‬ •‫گراف‬ ‫در‬G •‫اولیه‬ ‫گذاری‬‫نشان‬ ‫با‬M0 •𝜎 = 𝑡𝑖1 … 𝑡𝑖𝑛 •𝑀0 → 𝐺,𝑡 𝑖1 𝑀1 … 𝑀 𝑛−1 → 𝐺,𝑡 𝑖𝑛 𝑀 𝑛 •‫عمل‬ ‫های‬‫توالی‬ ‫تمام‬ ‫مجموعه‬ •L(N) Mahdi Dolati Verification of Reactive Systems 17
‫بودن‬ ‫زنده‬ •‫انتقال‬ ‫یک‬ •‫مرده‬:‫نکند‬ ‫عمل‬ ‫توالی‬ ‫هیچ‬ ‫در‬ •L1-‫زنده‬:‫باشد‬ ‫ممکن‬ ‫آن‬ ‫رخداد‬ •‫دارد‬ ‫وجود‬ ‫عمل‬ ‫های‬‫توالی‬ ‫از‬ ‫بعضی‬ ‫در‬ •L2-‫زنده‬:‫دلخواه‬ ‫صورت‬ ‫به‬ ‫ها‬‫بار‬ •‫حداقل‬k‫های‬‫توالی‬ ‫بعضی‬ ‫در‬ ‫بار‬‫وجود‬ ‫عمل‬‫دارد‬ •L3-‫زنده‬:‫نامحدود‬ ‫صورت‬ ‫به‬ ‫بارها‬ •‫حداقل‬k‫بعضی‬ ‫در‬ ‫بار‬‫پیشوندی‬ ‫ی‬‫زیرمجموعه‬ ‫یک‬ ‫اعضای‬-‫توال‬ ‫بسته‬‫ها‬‫ی‬ •L4-‫زنده‬:‫کند‬ ‫عمل‬ ‫همیشه‬ •L1-‫زنده‬‫ممکن‬ ‫های‬‫گذاری‬‫نشان‬ ‫تمام‬ ‫در‬ Mahdi Dolati Verification of Reactive Systems 18
‫داری‬‫کران‬ •‫محدود‬ ‫ها‬‫توکن‬ ‫تعداد‬ ‫ممکن‬ ‫های‬‫گذاری‬‫نشان‬ ‫تمام‬ ‫در‬ ‫اگر‬ ‫باشد‬ •‫استفاده‬:‫بافر‬ ‫سرریز‬ ،‫محدود‬ ‫منابع‬ •‫اگر‬ ‫تنها‬ ‫و‬ ‫اگر‬ ‫دار‬‫کران‬‫گراف‬‫محدود‬ ‫پذیری‬‫دسترس‬ •‫دار‬‫ظرفیت‬ ‫های‬‫محل‬ ‫با‬ ‫پتری‬ ‫ی‬‫شبکه‬ ‫گسترش‬ Mahdi Dolati Verification of Reactive Systems 19
‫پتری‬ ‫ی‬‫شبکه‬ ‫مثال‬ Mahdi Dolati Verification of Reactive Systems 20
‫ها‬‫افزونه‬ •‫یال‬ ‫مختلف‬ ‫انواع‬ •‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ •‫رنگی‬ ‫پتری‬ ‫ی‬‫شبکه‬ Mahdi Dolati Verification of Reactive Systems 21
‫یال‬ ‫مختلف‬ ‫انواع‬ •‫ریست‬ (1, 1, 0, 5) → 𝒕𝟐 … Mahdi Dolati Verification of Reactive Systems 22
‫یال‬ ‫مختلف‬ ‫انواع‬ •‫ریست‬ (1, 1, 0, 5) → 𝒕𝟐 (𝟏, 𝟎, 𝟏, 𝟎) Mahdi Dolati Verification of Reactive Systems 23
‫یال‬ ‫مختلف‬ ‫انواع‬ •‫خواندن‬ (1, 1, 0, 1) → 𝒕𝟐 … Mahdi Dolati Verification of Reactive Systems 24
‫یال‬ ‫مختلف‬ ‫انواع‬ •‫خواندن‬ (1, 1, 0, 1) → 𝒕𝟐 (1, 0, 1, 0) Mahdi Dolati Verification of Reactive Systems 25
‫یال‬ ‫مختلف‬ ‫انواع‬ •‫بازدارنده‬ t1‫اگر‬ ‫تنها‬ ‫و‬ ‫اگر‬ ‫است‬ ‫شده‬ ‫بازداشته‬M(P3) ≥ 1‫یا‬M(P4) ≥ 1 Mahdi Dolati Verification of Reactive Systems 26
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ •‫پتری‬ ‫های‬‫شبکه‬ ‫مختلف‬ ‫های‬‫بخش‬ ‫در‬ ‫زمانی‬ ‫توصیف‬ •‫ها‬‫انتقال‬ •‫ها‬‫مکان‬ •‫ها‬‫یال‬ •‫ها‬‫توکن‬ •‫غیرقطعی‬ ‫صورت‬ ‫به‬ ‫زمان‬ ‫گذر‬ Mahdi Dolati Verification of Reactive Systems 27
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ •‫پتری‬ ‫های‬‫شبکه‬ ‫قدرت‬‫کمتر‬‫تورینگ‬ ‫ماشین‬ ‫قدرت‬ ‫از‬ ‫است‬.[P13] •‫دار‬‫زمان‬ ‫پتری‬ ‫های‬‫شبکه‬ ‫قدرت‬‫معادل‬‫تورینگ‬ ‫ماشین‬ ‫است‬.[P08] Mahdi Dolati Verification of Reactive Systems 28
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ at‫و‬ ‫زمان‬ ‫زودترین‬bt‫زمانی‬ ‫دیرترین‬(‫شدن‬ ‫فعال‬ ‫از‬ ‫بعد‬) ‫کند‬ ‫عمل‬ ‫تواند‬ ‫می‬ ‫انتقال‬ ‫که‬ ‫است‬ Mahdi Dolati Verification of Reactive Systems 29
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ •‫مکانی‬ ‫گذاری‬‫نشان‬ •m0 = (2, 0, 1) •‫زمانی‬ ‫گذاری‬‫نشان‬ •‫شده‬ ‫فعال‬ ‫انتقال‬ ‫که‬ ‫باری‬ ‫آخرین‬ ‫از‬ ‫زمان‬ ‫نمایش‬ •h0 = (#, 0, 0, 0) Mahdi Dolati Verification of Reactive Systems 30
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ •‫شبکه‬ ‫این‬ ‫در‬ ‫حالت‬z = (m, h) •m‫مکانی‬ ‫گذاری‬‫نشان‬ ‫یک‬ •h‫زمانی‬ ‫گذاری‬‫نشان‬ ‫یک‬ •‫به‬ ‫حالت‬ ‫تغییر‬z’ = (m’, h’) •‫انتقال‬ ‫یک‬ ‫شدن‬ ‫فعال‬𝑧 → 𝑡 𝑧′ •‫زمان‬ ‫گذشت‬𝑧 → 𝜏 𝑧′ Mahdi Dolati Verification of Reactive Systems 31
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ Mahdi Dolati Verification of Reactive Systems 32
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ Mahdi Dolati Verification of Reactive Systems 33
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ Mahdi Dolati Verification of Reactive Systems 34
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ Mahdi Dolati Verification of Reactive Systems 35
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ Mahdi Dolati Verification of Reactive Systems 36
‫دار‬‫زمان‬ ‫پتری‬ ‫ی‬‫شبکه‬ Mahdi Dolati Verification of Reactive Systems 37
‫تشکر‬ ‫با‬! ‫پرسش؟‬ Mahdi Dolati Verification of Reactive Systems 38
‫منابع‬ • [P08] Prof. Louchka Popova-Zeugmann, “Time Petri Nets: Theory, Tools and Applications Part I”, Humboldt-Universität zu Berlin, Course Lecture • Prof. Morgan Magnin, “Computational Approaches to Analyze Complex Dynamic Systems : Model-Checking and its Applications”, NII International advanced lectures series on ICT: series of 4 lectures of 2 hours in Spring 2013 at National Institute of Informatics, , Tōkyō, Japan • http://en.wikipedia.org/wiki/Petri_net Mahdi Dolati Verification of Reactive Systems 39
‫ارجاعات‬ • [L76] Lipton, R. “The Reachability Problem Requires Exponential Space”, Technical Report 62, Yale University, 1976 • [P13] Louchka Popova-Zeugmann, “Time and Petri Nets”, Springer, Chapter 2, 2013 Mahdi Dolati Verification of Reactive Systems 40

More Related Content

شبکه‌های پتری