Automat ze stosem jest to automat skończony, który może wykorzystywać dodatkową strukturę danych, jaką jest stos. Automaty skończone odpowiadają wyrażeniom regularnym. Automat ze stosem pod względem siły wyrazu odpowiada gramatykom bezkontekstowym, rozpoznając języki bezkontekstowe. Innymi słowy automat ze stosem sprawdza, czy dany łańcuch należy do języka. Automat taki posiada taśmę wejściową, sterowanie skończone oraz stos, który jest łańcuchem symboli pewnego alfabetu. Domyślnie urządzenie będzie niedeterministyczne, posiada bowiem możliwość wyboru z pewnej skończonej liczby ruchów w każdej sytuacji. Mamy tutaj do czynienia z dwoma rodzajami ruchów.
W pierwszym z nich używa się symbolu wejściowego. W zależności od niego, a także od wierzchniego symbolu na stosie oraz stanu sterowania skończonego, mamy do wyboru pewną liczbę możliwości. Każda z nich składa się z następnego stanu dla sterowania skończonego i łańcucha symboli (może okazać się on pusty), którym zastępujemy symbol z wierzchołka stosu. Po wyborze jednego z wymienionych wariantów głowica przesuwa się o jedną pozycję do przodu.
Drugi rodzaj ruchu, nazywany -ruchem, jest podobny do pierwszego, z wyjątkiem tego, że nie posługujemy się symbolem wejściowym, a głowica wejściowa nie jest przesuwana po wykonaniu ruchu. Dzięki temu automat ze stosem ma możliwość manipulowania stosem bez czytania symboli wejściowych.
Język akceptowany przez automat ze stosem możemy zdefiniować na dwa sposoby. W pierwszym przypadku jest on zbiorem wszystkich łańcuchów wejściowych, dla których jakiś ciąg ruchów powoduje opróżnienie przez automat stosu. Nazywamy go językiem akceptowanym przy pustym stosie.
W drugim przypadku wyznaczamy pewne stany jako końcowe i definiujemy język akceptowany przez automat ze stosem jako zbiór wszystkich łańcuchów wejściowych, dla których pewien wybór ruchów powoduje, że automat przechodzi w stan końcowy.
Formalnie automat ze stosem możemy zdefiniować jako uporządkowaną siódemkę:
M = ( Q, Σ, Γ, δ, q0, Z0, F )
gdzie:
Q - skończony zbiór stanów
Σ - skończony alfabet wejściowy
Γ - skończony alfabet stosowy
Z0 - należący do Γ szczególny symbol stosowy, zwany symbolem
początkowym
F ⊆ Q - zbiór stanów końcowych
δ - funkcja przejścia odwzorowująca Q × ( Σ ∪ { ε } ) × Γ
na skończone podzbiory Q × Γ*
q0 - stan początkowy należący do Q
O ile nie zostanie zaznaczone inaczej, małe litery z początku alfabetu będą oznaczały symbole wejściowe, a małe litery z końca alfabetu - łańcuchy symboli wejściowych. Duże litery reprezentują symbole stosowe, a litery greckie - łańcuchy symboli stosowych.