אוטומט מחסנית
תיאור פורמלי

תיאור מתמטי פורמלי של אוטומט מחסנית  \ A הוא באמצעות השביעייה הסדורה הבאה:
\ A=\left\{Q,\Sigma ,\Gamma ,\delta ,q_{0},\dashv ,F\right\}
כאשר:
Q היא קבוצת מצבי האוטומט. כל מצב בקבוצה זו הוא, בהכרח, אחד מהשניים: "מצב מקבל" או "מצב לא מקבל".
\Sigma  היא (קבוצת) א"ב הקלט. כל איבר בקבוצה זו מכונה "אות".
\Gamma  היא (קבוצת) א"ב של המחסנית. כל איבר בקבוצה זו מכונה "אות".
\delta \colon Q\times \left(\Sigma \cup \left\{\varepsilon \right\}\right)\times \Gamma \to \mathrm {P} \left(Q\times \Gamma ^{*}\right) היא פונקציית המעברים.
q_{0} הוא המצב ההתחלתי (ממנו מתחיל החישוב)  q_{0}\in Q.
\dashv  היא האות ההתחלתית שבמחסנית - תמיד! זוהי אות שמורה מיוחדת, שמשמעותה בפועל היא שהמחסנית ריקה, כי למחסנית ריקה באמת יש משמעות מעשית אחרת באוטומט מחסנית.
F היא קבוצת המצבים המקבלים,  F\subseteq Q. מצב מקבל הוא מצב שמסמן שהאוטומט מחזיר תשובה חיובית. כלומר: אם בסוף הקלט האוטומט נמצא במצב מקבל, זה אומר שהקלט הוא מילה בשפה שהאוטומט מזהה.
משמעותה של פונקציית המעברים היא זו – בהינתן:
המצב הנוכחי של האוטומט (שם המצב),
האות הבאה שהוא קורא מהקלט (או המילה הריקה  \varepsilon , אם רוצים לתאר מעבר, שאינו כולל קריאת מילה מהקלט),
האות שמופיעה בראש המחסנית,
פעולת האוטומט תהיה לעבור למצב אחר (או להישאר במצב שבו הוא נמצא), ולשנות את תוכן המחסנית על ידי הסרת האות שנמצאת בראש המחסנית והכנסת אות או מילה חדשה במקומה למחסנית (ייתכן, אפילו, להכניס את אותה האות שהוצאה, על-מנת לא לשנות את מצב המחסנית).
מכיוון שהאוטומט אי-דטרמיניסטי, לכל שלשה סדורה של: מצב + אות קלט + אות מראש המחסנית, מותאמת קבוצה של זוגות סדורים אפשריים, שכל אחד מהם מורכב מ: המצב שאליו עוברים + המילה שמוכנסת לראש המחסנית (יכולה להיות גם המילה הריקה  \ \varepsilon ; דהיינו, לא להכניס אף אות למחסנית). לכן, טווח פונקציית המעברים הוא  \mathrm {P} \left(Q\times \Gamma ^{*}\right) – קבוצת החזקה של כל הזוגות האפשריים של מצב + המילה המוכנסת לראש המחסנית. עם זאת, מניחים כי רק תת-הקבוצות הסופיות של זוגות שכאלו יכולים להתקבל באמצעות פונקציית המעברים (כלומר, מספר דרכי הפעולה השונות של האוטומט, בהינתן מצב, אות קלט ואות מראש המחסנית הוא סופי).
פונקציית המעברים אינה מוגדרת, כאשר המחסנית ריקה. על כן, ריקון של המחסנית לפני תום קריאת מלוא מילת הקלט גורר בהכרח "היתקעות" של האוטומט ודחיית המילה הנקראת (כלומר, החזרת התשובה, שהמילה אינה בשפה שהאוטומט מזהה). באופן דומה, אין הכרח להגדיר את פונקציית המעברים עבור כל השלשות הסדורות האפשריות, וניתן לחשוב על כל שלשה סדורה, שעבורה הפונקציה אינה מוגדרת, כאילו היא "תוקעת" את האוטומט (כזכור, אנו מדברים על אוטומט (מחסנית) לא דטרמיניסטי).
להלן מספר דוגמאות לפעולת פונקציית המעברים  \delta  (הפועלת על שלשה סדורה ומחזירה זוג סדור), שבכולן האוטומט מתחיל במצב  q ונשאר בו:
(q,Z)\in \delta (q,\sigma ,Z) - האוטומט קורא את האות  \sigma  מהקלט ואינו משנה את ראש המחסנית (ניתן לחשוב על כך כאילו האוטומט הוציא את האות  Z מראש המחסנית ומיד הכניס אותה בחזרה).
(q,\sigma Z)\in \delta (q,\sigma ,Z) - האוטומט קורא את האות  \ \sigma  מהקלט ודוחף אותה למחסנית, מעל ראש המחסנית הקיים (ניתן לחשוב על כך כאילו האוטומט הוציא את האות  Z מראש המחסנית ומיד דחף אותה חזרה, ואחריה דחף גם את האות  \ \sigma ).
(q,\varepsilon )\in \delta (q,\sigma ,Z) - האוטומט קורא את האות  \ \sigma  מהקלט ומוציא את האות  Z מראש המחסנית, מבלי לדחוף למחסנית שום דבר אחר במקומה. בכך, נחשפת האות שמתחתיה (זו שהוכנסה ממש לפני האות  Z למחסנית) ומהווה את ראש המחסנית החדש.