Automata and formal languages