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

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. DiscoverabilityRefers to determining possible actions and the visualization's current state. FeedbackRefers to information provided to understand the visualization's state.Conceptual Model Refers to creating a conceptual model of the process illustrated. AffordancesRefers to the relationship between an object and the user's capabilities. SignifiersRefers to any indicator that communicates appropriate behavior to a user. MappingsRefers to the relationship between controls and their actions.

Authors

Institutions

Publication Details

Journal
Electronic Proceedings in Theoretical Computer Science
Published
2025-08-04
DOI
https://doi.org/10.4204/eptcs.424.5
Primary Topic
Formal Methods in Verification
Type
article
Field-Weighted Citation Impact
0.00
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

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

Marco T. Morazán, Tijana Minić, Andrés M. Garced, David Anthony K. Fields
Electronic Proceedings in Theoretical Computer Science
Formal Methods in Verification
article

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

Marco T. Morazán, Tijana Minić, Andrés M. Garced, David Anthony K. Fields
article en

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. DiscoverabilityRefers to determining possible actions and the visualization's current state. FeedbackRefers to information provided to understand the visualization's state.Conceptual Model Refers to creating a conceptual model of the process illustrated. AffordancesRefers to the relationship between an object and the user's capabilities. SignifiersRefers to any indicator that communicates appropriate behavior to a user. MappingsRefers to the relationship between controls and their actions.

Electronic Proceedings in Theoretical Computer ScienceVol. 424
Seton Hall University (US), University of Washington (US)
Openalex Percentile: Top 79%
Formal Methods in Verification
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.