בתרשים של רשת פטרי (ראה תרשים למעלה מימין), מקומות מתוארים בדרך כלל כעיגולים, מעברים כמלבנים צרים וארוכים וקשתות כחצים בכיוון אחד המראים קשרים של מקומות למעברים או מעברים למקומות. אם התרשים היה של רשת אלמנטרית, אז אותם מקומות בתצורה היו מסומנים כעיגולים, כאשר כל עיגול מקיף נקודה אחת הנקראת "אסימון". בתרשים הנתון של רשת פטרי (ראה מימין), עיגולי המקומות יכולים להכיל אסימון אחד או יותר כדי להראות את מספר הפעמים שהמקום מופיע בתצורה. התצורה של האסימונים המפוזרים על פני תרשים רשת פטרי כל נקרא "סימון".
באיור העליון, המקום "p1" הוא מקום קלט של מעבר "t"; ואילו המקום "p2" הוא מקום הפלט של אותו מעבר. תהי "PN0" (איור למעלה) רשת פטרי עם סימון המוגדרת "M0" ותהי "PN1" (איור למטה) רשת פטרי עם סימון המוגדרת "M1". התצורה של "PN0" "מאפשרת" את מעבר t בשל התכונה כי כל מקומות הקלט בעלי מספר מספיק של אסימונים (מוצגים באיורים כנקודות) ה"שווה או גדול" לריבוי הקשתות המתאימות שלהם שלהם ל-"t". אם ורק אם המעבר מאופשר, המעבר יופעל. בדוגמה זו, ה"הפעלה" של מעבר "t" יוצר מפה בעלת סימון המוגדרת "M1" בדמות של "M0" הנוצרת ברשת פטרי "PN1" כפי שניתן לראות באיור למטה. ניתן לתאר את חוק ההפעלה של מעבר, כמתואר בתרשים, כחיסור מספר האסימונים ממקומות הקלט שלו השווה לריבוי קשתות הקלט בהתאמה, והוספת מספר חדש של אסימונים במקומות הפלט השווה לריבוי קשתות הפלט המתאימות.
הערה 1. המשמעות המדויקת של "שווה ל- או גדול מ-" תלויה בתכונות האלגבריות המדויקות של הוספה המיושמת על "Z" בחוק ההפעלה, כאשר שינויים קלים בתכונות האלגבריות יכולים להוביל לסוגים אחרים של רשתות פטרי; לדוגמה, רשתות פטרי אלגבריות.
ההגדרה להלן מבוססת באופן רופף על . ישנן הגדרות חלופיות רבות.
תחביר.
גרף רשת פטרי (מכונה לעיתים "רשת פטרי", ראו למטה) הוא שלשה formula_6, כאשר:
"רלציית הזרימות" היא קבוצת הקשתות: formula_8. בספרי לימוד רבים, קשתות יכולות להיות בעלות ריבוי 1. ספרים אלו בדרך כלל מגדירים רשתות פטרי על ידי "F" במקום "W". כשמשתמשים במוסכמה הזו, גרף רשת פטרי הוא מולטיגרף מכוון formula_9 עם מחיצות הצמתים "S" ו-"T".
"קבוצת הקלט" של מעבר "t" הוא קבוצת "מקומות הקלט" שלו: formula_10;
"קבוצת הפלט" שלו הוא קבוצת המקומות formula_11. ההגדרות של קבוצות הקלט והפלט של מקומות הן מקבילות.
"סימון" של רשת פטרי (גרף) הוא רב-קבוצה של המקומות שלה, למשל המיפוי formula_12. אנו אומרים כי הסימון מקצה לכל מקום מספר של "אסימונים".
רשת פטרי (יש המכנים אותה "רשת פטרי מסומנת", ראה למעלה) היא 4-יה formula_13, כאשר
סמנטיקת ביצוע.
מילולית:
אנו בדרך כלל מתעניינים במה שעשוי לקרות כאשר מעברים עלולים לפעול ברציפות באופן שרירותי.
אנו אומרים כי סימון formula_19 הוא "נגיש" מסימון "M" בצעד אחד אם formula_20; אנו אומרים כי הוא "נגיש מ-"M" אם formula_21 כאשר: formula_22 הוא הסגור הטרנזיטיבי של formula_23; כלומר, אם הוא נגיש ב-0 צעדים או יותר.
עבור רשת פטרי (מסומנת) formula_24, אנו מתעניינים בהפעלות שעשויות להתרחש החל מהסימון ההתחלתי formula_15. קבוצת "הסימונים הנגישים" שלו היא הקבוצה formula_26.
"גרף הנגישות" (reachability graph) של "N" הוא רלציית המעברים (מכפלה קרטזית של קבוצת המעברים בעצמה) formula_23 המוגבל על ידי הסימונים הנגישים שלו formula_28. זהו מרחב המצבים של הרשת.
"רצף ההפעלות" (firing sequence) של רשת פטרי עם גרף "G" וסימון התחלתי formula_15 הוא רצף של מעברים formula_30 כך ש-formula_31. קבוצת רצפי ההפעלות מסומנת formula_32.
הגדרות חלופיות.
כפי שצוין לעיל, הגדרה חלופית נפוצה היא איסור ריבוי קשתות (משקל כל קשת תמיד 1) והחלפת רב-הקבוצה של קשתות "W" בקבוצה פשוטה, המכונה "רלציית הזרימה", formula_33.
זה לא מגביל את כוח ההבעה של רשת הפטרי היות ששתי השיטות מסוגלות לייצג זו את זו.
חלופה נפוצה נוספת, למשל, ב-Desel and Juhás (2001), מאפשרת לסמן "קיבולות" של מקומות. נושא זה נדון תחת "הרחבות" בהמשך.
ניסוח במונחים של וקטורים ומטריצות.
הסימונים של רשת פטרי formula_13 יכולים להיחשב כוקטורים של מספרים שלמים אי-שליליים באורך formula_35.
רלציית המעברים שלה יכולה להיות מתוארת כזוג מטריצות formula_35 על formula_37:
ואז ההפרש ביניהן
שים לב שחובה כי " W " יהיה רצף הפעלות; אם ברשת מתאפשרים רצפים אקראיים של מעברים, בדרך כלל תיווצר קבוצה גדולה יותר.
formula_46
formula_47
formula_48
formula_49
תכונות מתמטיות של רשתות פטרי.
אחד הגורמים לכך שרשתות פטרי הן מעניינות הוא שהן מספקות איזון בין כוח המידול ויכולת ניתוח: ניתן לקבוע באופן אוטומטי דברים רבים על מערכות מקביליות ברשתות פטרי, אף על פי שחלק מהדברים הללו "יקר" מאוד לקביעה במקרה הכללי. מספר תת-קבוצות של רשתות פטרי אשר נחקרו מסוגלות למדל קבוצות מעניינות של מערכות מקביליות, ולהקל על בעיות אלה.
ניתן למצוא סקירה על בעיות החלטה כאלו, עם תוצאות כריעות וסיבוכיות של רשתות פטרי ושל מספר תתי-קבוצות, ניתן למצוא בEsparza and Nielsen (1995).
Esparza ונילסן (1995)
נגישות.
בעיית הנגישות (reachability) של רשתות פטרי היא להכריע, בהינתן רשת הפטרי "N" והסימון "M", האם formula_50, האם ניתן להגיע לסימון "M" על ידי רצף כלשהו של מעברים.
ברור כי זהו עניין של הליכה בגרף הנגישות המוגדר לעיל, עד שנגיע לסימון המבוקש או עד שנדע כי כבר לא ניתן להגיע אליו, אולם זה יותר קשה ממה שזה נראה בהתחלה: גרף הנגישות הוא בדרך כלל אינסופי, וזה לא קל לקבוע מתי זה ניתן לעצור.
למעשה, בעיה זו הוצגה כבעלת קושי EXSPACE שנים לפני שהיא הוצגה בכלל ככריעה (Mayr, 1981). עדיין מתפרסמים מחקרים על כיצד ניתן לבצע זאת ביעילות.
אמנם נדמה כי נגישות היא כלי טוב למציאת מצבים שגויים, אך בדרך כלל הגרף מכיל יותר מדי מצבים מכדי לחשב. על מנת להקל על בעיה זו, משתמשים בדרך כלל בלוגיקה עיתית ליניארית (Linear Temporal Logic) בשילוב עם שיטת התמונה האנליטית כדי להוכיח שלא ניתן להגיע למצבים כאלו. LTL משתמש בטכניקת ההחלטה למחיצה כדי למצוא האם אכן ניתן להגיע למצב, על ידי מציאת קבוצת תנאים הכרחיים על מנת להגיע אליו, ואז מוכיח כי תנאים אלו אינם מספקים.
חיות.
ניתן לתאר רשת פטרי כבעלת דרגות חיות שונות של חיות (liveness)formula_51. רשת פטרי formula_52 נקראת בעלת חיות formula_53 אם ורק אם כל המעברים שלה הם בעלי חיות formula_53, כאשר מעבר הוא
שימו לב כי הדרשות מחמירות בסדר עולה: חיות formula_65 מרמזת חיות formula_66 עבור formula_67.
הגדרות אלו הן בהתאם לסקירה של Murata, אשר משתמש ב"חיות" formula_68 כמונח עבור "מת".
חסימות.
מקום ברשת פטרי נקרא "חסום-k" אם הוא לא מכיל יותר מ-"k" אסימונים בכל הסימונים הנגישים, כולל הסימון ההתחלתי; הוא נחשב כ"שמור" (safe) אם הוא "חסום-1"; הוא "קבוצה חסומה k" אם הוא "חסום-k" עבור "k" כלשהו.
ישנן מספר הגדרות חסימות של רשת פטרי
שים לב כי רשת היא חסומה אם ורק אם גרף הנגישות שלה הוא סופי.
חסימות היא כריעה על ידי בחינת בעיות כיסוי, על ידי בניית עץ קארפ-מילר.
כפיית חסימות באופן מפורש על מקומות ברשת נתונה עשויה להיות שימושית. זה יכול לשמש מידול של משאבים מוגבלים.
הגדרות מסוימות של רשתות פטרי מתירות זאת באופן מפורש כתכונה תחבירית.
באופן רשמי, "רשתות פטרי עם קיבולת מקומות" יכולות להיות מוגדרות כ-n-יות formula_69, כאשר formula_70 היא רשת פטרי, formula_71 הקצאה של קיבולות לחלק או כל המקומות, ורלציית המעברים היא זה שבדרך כלל מוגבל לסימונים כאשר כל מקום עם קיבולת יש לכל היות מספר אסימונים כזה.
למשל אם ברשת "N", מוקצה הקיבולת 2 לשני מקומות, נקבל רשת פטרי עם קיבולות מקום, נניח "N2"; גרף הנגישות שלה מוצג בצד ימין.
לחלופין, ניתן לחסום מקומות על ידי הרחבת הרשת. ליתר דיוק, מקום יכול להיות חסום-"k" על ידי הוספת "מקום-נגד" עם זרימה הפוכה אליו, והוספת אסימונים כך שסך האסימונים במקומות-הנגד יהיה "k".
רשתות פטרי בדידות, רציפות והיברידיות.
כמו גם לאירועים בדידים, יש רשתות פטרי לתהליכים רציפים ובדידים-רציפים היברידיים, שהם שימושיים בתורת הבקרה בדידה, רציפה ושליטה, וקשורה לתורת האוטומטים בדידים, רציפים והיברידיים.
הרחבות.
ישנן הרחבות רבות לרשתות פטרי. חלקן בעלות תאימות מלאה לאחור (למשל רשתות פטרי צבעוניות) עם רשת הפטרי המקורית. ישנם המוסיפים תכונות שלא ניתנות למידול בפורמליזם של רשת הפטרי המקורית (למשל רשתות פטרי מתוזמנות). אף על פי שמודלים בעלי תאימות לאחור אינם מיישמים את כוח החישוב של רשתות פטרי, ייתכן שיש להם ייצוגים תמציתיים והם עשויים להיות יותר נוחים למידול. לעיתים הרחבות שלא ניתן לייצג כרשת פטרי מקורית הן מאוד חזקות, אך בדרך כלל חסרות את המגוון הרחב של כלים מתמטיים הזמינים לניתוח ברשתות פטרי רגילות.
המונח רשת פטרי ברמת-על (high-level petri net) משמש פורמליזם של רשתות פטרי המיישמות את הפורמליזם של אשת פטרי מקורית; זה כולל רשתות פטרי צבעוניות, רשתות פטרי היררכיות כגון רשתות בתוך רשתות, וכל שאר ההרחבות הנידונות בפרק זה. המונח גם משמש במיוחד את רשתות הפטרי הצבעוניות הנתמכות על ידי CPN tools.
רשימה קצרה של הרחבות אפשריות: