Visual Execution and Validation of Finite-State Machines and Pushdown Automata

TL;DR

This paper introduces dynamic visualization tools for finite-state machines and pushdown automata to enhance student understanding of their operational semantics and facilitate verification in automata theory education.

Contribution

The paper presents two novel visualization tools that animate all possible computations of nondeterministic finite automata and pushdown automata, aiding learning and verification.

Findings

Tools successfully visualize all computations step-by-step.

Enhanced student comprehension of nondeterministic and pushdown automata.

Facilitated validation of automata properties visually.

Abstract

In Formal Languages and Automata Theory courses, students find understanding nondeterministic finite-state and pushdown automata difficult. In many cases, this means that it is challenging for them to comprehend the operational semantics of such machines and, as a consequence, determine why a word is accepted or rejected. This is not entirely surprising, because students are mostly trained to design and implement deterministic programs. Comprehension of pushdown automata is further complicated, because reasoning about the stack is necessary. A common difficulty students face, for example, is understanding that two different computations on the same word may reach the same state with different stack values. To aid student understanding, we present two novel dynamic visualization tools for FSM -- a domain-specific programming language for the Automata Theory classroom -- to support the design of such machines. These tools visualize all computations that may be performed, respectively, by a nondeterministic finite-state machine or by a pushdown automata in a stepwise manner. In addition, these tools aid the machine verification process by allowing users to visually validate whether the properties a state represents hold when a machine transitions into it.