标题： 视觉执行与有限状态机和下推自动机的验证 显示英文标题

标题： Visual Execution and Validation of Finite-State Machines and Pushdown Automata

摘要： 在形式语言与自动机理论课程中，学生发现理解非确定性有限状态自动机和下推自动机很困难。 在许多情况下，这意味着他们很难理解这些机器的操作语义，因此难以确定一个单词为何被接受或拒绝。 这并不令人意外，因为学生主要被训练设计和实现确定性程序。 对下推自动机的理解进一步复杂化，因为需要对栈进行推理。 例如，学生面临的一个常见困难是理解同一单词上的两种不同计算可能在不同的栈值下到达相同的状态。 为了帮助学生理解，我们介绍了两种新颖的动态可视化工具用于 FSM——一种用于自动机理论课堂的领域特定编程语言——以支持此类机器的设计。 这些工具分别以逐步的方式可视化非确定性有限状态机或下推自动机可能执行的所有计算。 此外，这些工具通过允许用户视觉验证当机器进入某个状态时，该状态所代表的属性是否成立，从而有助于机器验证过程。 显示英文摘要

摘要： 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.