一个下推自动机(PDA) M 可以定义为一个 7-元组:
这里的
- 是状态的有限集合
- 是输入字母表的有限集合
- 是栈字母表的有限集合
- 是开始状态,是 的元素
- 是初始栈符号,是 的元素
- 是最终状态的集合,是 的子集
- 是有限转移(transition)关系 。
M 是确定的,如果它满足下列两个条件:
- 对于任何 ,集合 有最多一个元素。
- 对于任何 ,如果 ,则 对于所有
有两种可能的接受标准: “空栈”接受和“最终状态”接受。对于确定下推自动机这两种接受是不等价的(尽管对于非确定下推自动机是等价的)。被空栈接受的语言是被最终状态接受的语言,同时满足没有在语言中的串是在语言中的其他串的前缀。