下推自动机﹙PDA﹚是自动机理论中定义的一种抽象的计算模型。下推自动机比有限状态自动机复杂：除了有限状态组成部分外，还包括一个长度不受限制的栈；下推自动机的状态迁移不但要参考有限状态部分，也要参照栈当前的状态；状态迁移不但包括有限状态的变迁，还包括一个栈的出栈或入栈过程。下推自动机可以形象的理解为，把有限状态自动机扩展使之可以存取一个栈。
下推自动机存在确定与非确定两种形式，两者并不等价。﹙对有限状态自动机两者是等价的﹚
每一个下推自动机都接受一个形式语言。被非确定下推自动机接受的语言是上下文无关语言。
如果我们把下推自动机扩展，允许一个有限状态自动机存取两个栈，我们得到一个能力更强的自动机，这个自动机与图灵机等价。
下推自动机 M 是如下的一个七元组 ( Q, Σ, Γ, δ, q0, Z0, F ) ，其中：
* Q 是一个有穷状态集合；
* Σ 是一个字母表，称为输入字母表。
* Γ 是一个字母表，称为栈字母表。
* q0 属于 Q ，是初始状态。
* Z0 属于 Γ ，是一个特殊的栈符号，称为栈起始符号。
* F 包含于 Q ，是终结状态集合。
* δ : Q×(Σ∪{ε})×Γ -> Q×Γ* 是 M 的动作函数。