אוטומט סופי הוא מכונה מופשטת בתורת החישוביות במדעי המחשב, שהיא בעלת זיכרון מוגבל ומגדירה שפה פורמלית רגולרית.

קיימים שני סוגים של אוטומטים סופיים – אוטומט סופי דטרמיניסטי (DFA –‏ Deterministic Finite Automaton) ואוטומט סופי לא דטרמיניסטי (NFA –‏ Nondeterministic Finite Automaton).

ניתן לתאר אוטומט סופי דטרמיניסטי באמצעות קבוצה סופית של מצבים, המשמשים את האוטומט והוא עובר בהם לפי כללים קבועים מראש במהלך קריאת מילת קלט. חלק ממצבי האוטומט הם מצבים מקבלים. אם בסוף קריאת המילה מגיע האוטומט למצב מקבל, המילה שייכת לשפה המוגדרת על ידיו, אחרת לא. הכללים למעבר ממצב למצב מוגדרים על ידי פונקציית המעברים שמגדירה עבור כל מצב ${\displaystyle q}$ ואות ${\displaystyle \sigma }$ מצב יחיד ${\displaystyle q'}$ (ייתכן ש ${\displaystyle q'=q}$) אליו עובר האוטומט כאשר הוא נמצא במצב ${\displaystyle q}$ והאות שהוא קרא מן הקלט היא ${\displaystyle \sigma }$. כמו כן, אחד המצבים מוגדר כמצב התחלתי שממנו מתחיל האוטומט בקריאת המילים. סדרת מעברי מצבים של אוטומט במהלך קריאה של מילה ${\displaystyle w}$, ואשר מתחילה מן המצב ההתחלתי, נקראת ריצה של האוטומט על ${\displaystyle w}$.

אוטומט סופי אי־דטרמיניסטי דומה לאוטומט הדטרמיניסטי, אלא שפונקציית המעברים מוגדרת באופן שונה. באוטומט האי-דטרמיניסטי, עבור כל מצב ${\displaystyle q}$ ואות ${\displaystyle \sigma }$ עשויים להיות מספר כלשהו (גם 0) של מצבים אליהם יכול האוטומט לעבור כאשר הוא נמצא במצב ${\displaystyle q}$ והאות שהוא קורא מן הקלט היא ${\displaystyle \sigma }$. במודלים מסוימים, פונקציית המעברים מאפשרת מעברים בין מצבים מסוימים ללא קריאת אף אות מן הקלט (מעברי-${\displaystyle \epsilon }$). כתוצאה מכך, עשויות להיות מספר ריצות שונות של האוטומט על מילת קלט מסוימת. מבחינה פורמלית, מילה תתקבל אם ורק אם קיימת ריצה של האוטומט שמסתיימת במצב מקבל כלשהו, גם אם קיימת ריצה אחרת שמסתיימת במצב שאינו מקבל, או כזו ש"נתקעת" משום שהגיעה למצב שממנו אין אף מעבר אפשרי עבור האות שנקראת מן הקלט.

לפי ההגדרה, כל אוטומט סופי דטרמיניסטי הוא בפרט גם אוטומט סופי אי-דטרמיניסטי. בכיוון ההפוך, ניתן להוכיח כי כל אוטומט סופי אי־דטרמיניסטי שקול לאוטומט סופי דטרמיניסטי. כלומר, היעדר הדטרמיניזם אינו מוסיף לכוחו החישובי של האוטומט הסופי (בשונה מאשר במודל של אוטומט מחסנית, לדוגמה).

שפות המתקבלות על ידי אוטומט סופי נקראות שפות רגולריות ונוצרות על ידי דקדוקים רגולריים וביטויים רגולריים.

ישנם מודלים של אוטומטים סופיים מעל עצמים אינסופיים (למשל, מילים אינסופיות, כלומר סדרות אינסופיות של אותיות מהאלפבית). כתוצאה מכך, אין אפשרות להגדיר קבלה של מילה בהתאם למצב שבו נמצא האוטומט בסיומה של הריצה, משום שזו לא מסתיימת.

קיימים מודלים שונים שמגדירים קבלה של מילים אינסופיות. למשל, באוטומט בוקי (Büchi) תנאי הקבלה מגדיר קבוצת מצבים מקבלים, ומילה מתקבלת אם ורק אם היא מבקרת במצב מקבל אינסוף פעמים. באוטומט רבין תנאי הקבלה מורכב מזוגות של קבוצות ${\displaystyle \{\langle G_{1},B_{1}\rangle ,\langle G_{2},B_{2}\rangle ,\cdots ,\langle G_{k},B_{k}\rangle \))$ כאשר ריצה היא מקבלת אם קיים זוג ${\displaystyle \langle G_{i},B_{i}\rangle }$ שעבורו קבוצת המצבים ${\displaystyle S}$ שבהם מבקרת הריצה אינסוף פעמים מקיימת ${\displaystyle S\cap G_{i}\neq \emptyset }$ ו- ${\displaystyle S\cap B_{i}=\emptyset }$, כלומר הריצה מבקרת אינסוף פעמים במצב מ-${\displaystyle G_{i))$ ומבקרת רק מספר סופי של פעמים בכל מצבי ${\displaystyle B_{i))$. מלבד שני מודלים אלו קיימים מודלים רבים נוספים אשר מגדירים את אופן קבלת המילים על ידי האוטומט.

שלא כמו במקרה של אוטומטים סופיים מעל מילים סופיות, שבו קיימת שקילות בין המודלים הדטרמיניסטי והאי-דטרמיניסטי, אין שקילות כזו בהקשר של אוטומט בוקי. קיימות שפות פשוטת שעבורן קיים אוטומט בוקי אי-דטרמיניסטי, אבל לא קיים אוטומט דטרמיניסטי שקול (למשל, שפת כל המילים שמכילות רק מספר סופי של אות נתונה). במקרה של אוטומט רבין כן קיימת שקילות כזו. יותר מכך, לכל אוטומט בוקי קיים אוטומט רבין שקול.

• תורת האוטומטים - מונחים
• ההיררכיה של חומסקי
• אוטומט מחסנית
• מכונת טיורינג

• שמואל זקס ונסים פרנסיז, ‏אוטומטים ושפות פורמליות, האוניברסיטה הפתוחה, 2000

• תורת האוטומטים, באתר MathWorld (באנגלית)
• תורת האוטומטים, באתר אנציקלופדיה בריטניקה (באנגלית)
• אוטומטים (תיאוריה), דף שער בספרייה הלאומית