formal definition of Push down Automata.

In this post we will concentrate on formal definition of Push down Automata. It is also called “Non deterministic Push down Automata” (NPDA). But remember that NPDA is different from “Deterministic Push down Automata” (DPDA)
“Non deterministic Push down Automata” (NPDA)
Formal definition:
A NPDA W can be defined as a 7-tuple:
W = (Q,Σ,Φ,σ,s,Ω,F) where
• Q is a finite set of states
• Σ is a finite set of the input alphabet
• Φ is a finite set of the stack alphabet
• σ (or sometimes δ) is a finite transition relation
(Q x (Σ U {ε} x Ø) ----> P (Q x Ø)
• s is an element of Q the start state
• Ω is the initial stack symbol
• F is subset of Q, consisting of the final states.