Finite Automata and Their Decision Problems

Reference. Finite Automata and Their Decision Problems

M. O. Rabin, Dana Scott · IBM Journal of Research and Development · 1959 · parsing · DOI

Finite automata are considered in this paper as instruments for classifying finite tapes. Each onetape automaton defines a set of tapes, a two-tape automaton defines a set of pairs of tapes, et cetera. The structure of the defined sets is studied. Various generalizations of the notion of an automaton are introduced and their relation to the classical automata is determined. Some decision problems concerning automata are shown to be solvable by effective algorithms; others turn out to be unsolvable by algorithms.

Cite

Cite as @rabinFiniteAutomataTheir1959 (helia, typst) · \cite{rabinFiniteAutomataTheir1959} (LaTeX)

BibTeX

bibtex · 16 lines

@article{rabinFiniteAutomataTheir1959,
 title = {Finite {Automata} and {Their} {Decision} {Problems}},
 author = {Rabin, M. O. and Scott, D.},
 year = {1959},
 doi = {10.1147/rd.32.0114},
 url = {http://ieeexplore.ieee.org/document/5392601/},
 urldate = {2024-04-29},
 journal = {IBM Journal of Research and Development},
 volume = {3},
 number = {2},
 pages = {114--125},
 month = {April},
 language = {en},
 abstract = {Finite automata are considered in this paper as instruments for classifying finite tapes. Each onetape automaton defines a set of tapes, a two-tape automaton defines a set of pairs of tapes, et cetera. The structure of the defined sets is studied. Various generalizations of the notion of an automaton are introduced and their relation to the classical automata is determined. Some decision problems concerning automata are shown to be solvable by effective algorithms; others turn out to be unsolvable by algorithms.},
 issn = {0018-8646, 0018-8646}
}

hayagriva YAML (typst)

yaml · 20 lines

rabinFiniteAutomataTheir1959:
  type: article
  title: Finite {Automata} and {Their} {Decision} {Problems}
  author:
  - Rabin, M. O.
  - Scott, D.
  date: 1959-04
  page-range: 114-125
  url:
    value: http://ieeexplore.ieee.org/document/5392601/
    date: 2024-04-29
  serial-number:
    doi: 10.1147/rd.32.0114
    issn: 0018-8646, 0018-8646
  abstract: Finite automata are considered in this paper as instruments for classifying finite tapes. Each onetape automaton defines a set of tapes, a two-tape automaton defines a set of pairs of tapes, et cetera. The structure of the defined sets is studied. Various generalizations of the notion of an automaton are introduced and their relation to the classical automata is determined. Some decision problems concerning automata are shown to be solvable by effective algorithms; others turn out to be unsolvable by algorithms.
  parent:
    type: periodical
    title: IBM Journal of Research and Development
    issue: 2
    volume: 3

Download: rabinFiniteAutomataTheir1959.bib · rabinFiniteAutomataTheir1959.yml

Cited by (6)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

We present Dependent Lambek Calculus (Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ ), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ , linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb

The categorical contours of the Chomsky-Schützenberger representation theorem mellies-2025-theLMCS · 2025

We develop fibrational perspectives on context-free grammars and on nondeterministic finite-state automata over categories and operads. A generalized CFG is a functor from a free colored operad (aka multicategory) generated by a pointed finite species into an arbitrary base operad: this encompasses classical CFGs by taking the base to be a certain operad constructed from a free monoid, as an instance of a more general construction of an operad of spliced arrows

𝒲︀ 𝒞︀

for any category

𝒞︀

. A generalized NFA is a functor from an arbitrary bipointed category or pointed operad satisfying the unique lifting of factorizations and finite fiber properties: this encompasses classical word automata and tree automata without

𝜖

-transitions, but also automata over non-free categories and operads. We show that generalized context-free and regular languages satisfy suitable generalizations of many of the usual closure properties, and in particular we give a simple conceptual proof that context-free languages are closed under intersection with regular languages. Finally, we observe that the splicing functor

𝒲︀ : Cat \to Oper

admits a left adjoint

𝒞︀ : Oper \to Cat

, which we call the contour category construction since the arrows of

𝒞︀ 𝒪︀

have a geometric interpretation as oriented contours of operations of

𝒪︀

. A direct consequence of the contour / splicing adjunction is that every pointed finite species induces a universal CFG generating a language of tree contour words. This leads us to a generalization of the Chomsky-Schützenberger Representation Theorem, establishing that a subset of a homset

𝐿 \subseteq 𝒞︀ (𝐴, 𝐵)

is a CFL of arrows if and only if it is a functorial image of the intersection of a

𝒞︀

-chromatic tree contour language with a regular language.

DOI · arXiv

A Bayesian Interpretation of the Internal Model Principle baltieri-2025-aarXiv · 2025

The internal model principle, originally proposed in the theory of control of linear systems, nowadays represents a more general class of results in control theory and cybernetics. The central claim of these results is that, under suitable assumptions, if a system (a controller) can regulate against a class of external inputs (from the environment), it is because the system contains a model of the system causing these inputs, which can be used to generate signals counteracting them. Similar claims on the role of internal models appear also in cognitive science, especially in modern Bayesian treatments of cognitive agents, often suggesting that a system (a human subject, or some other agent) models its environment to adapt against disturbances and perform goal-directed behaviour. It is however unclear whether the Bayesian internal models discussed in cognitive science bear any formal relation to the internal models invoked in standard treatments of control theory. Here, we first review the internal model principle and present a precise formulation of it using concepts inspired by categorical systems theory. This leads to a formal definition of “model” generalising its use in the internal model principle. Although this notion of model is not a priori related to the notion of Bayesian reasoning, we show that it can be seen as a special case of possibilistic Bayesian filtering. This result is based on a recent line of work formalising, using Markov categories, a notion of “interpretation”, describing when a system can be interpreted as performing Bayesian filtering on an outside world in a consistent way.

DOI · arXiv

Self-certifying Railroad Diagrams: Or: How to Teach Nondeterministic Finite Automata hinze-2019-selfMPC · 2019

DOI

Regular-expression derivatives re-examined owensRegularexpressionDerivativesReexamined2009JFP · 2009

Abstract Regular-expression derivatives are an old, but elegant, technique for compiling regular expressions to deterministic finite-state machines. It easily supports extending the regular-expression operators with boolean operations, such as intersection and complement. Unfortunately, this technique has been lost in the sands of time and few computer scientists are aware of it. In this paper, we reexamine regular-expression derivatives and report on our experiences in the context of two different functional-language implementations. The basic implementation is simple and we show how to extend it to handle large character sets (e.g., Unicode). We also show that the derivatives approach leads to smaller state machines than the traditional algorithm given by McNaughton and Yamada.

PDF · DOI · pldb

Derivatives of Regular Expressions brzozowskiDerivativesRegularExpressions1964JACM · 1964

Kleene’s regular expressions, which can be used for describing sequential circuits, were defined using three operators (union, concatenation and iterate) on sets of sequences. Word descriptions of problems can be more easily put in the regular expression language if the language is enriched by the inclusion of other logical operations. However, in the problem of converting the regular expression description to a state diagram, the existing methods either cannot handle expressions with additional operators, or are made quite complicated by the presence of such operators.In this paper the notion of a derivative of a regular expression is introduced and the properties of derivatives are discussed. This leads, in a very natural way, to the construction of a state diagram from a regular expression containing any number of logical operators.

DOI

Cites 7 works (0 here)

External (7)