Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Axiomatizing NFAs Generated by Regular Grammars

Roberto Gorrieri

TL;DR

This work axiomatizes language equivalence on GFAs by embedding GFAs into a restricted process algebra $SFM_0$, establishing a representability theorem that every GFA $N$ corresponds to an $SFM_0$ term $p$ with isomorphic semantics. It introduces a precise, compositional denotational semantics mapping $SFM_0$ terms to GFAs, and proves that language equivalence is a congruence for all operators, including recursion. The main contribution is a compact, sound and complete axiom system for language equivalence consisting of $7$ axioms plus $2$ conditional axioms, together with normal-form, saturation, and semi-deterministic techniques to prove completeness. The results enable algebraic reasoning about regular languages via a process-algebraic framework and offer a basis for extending the approach to other equivalences in the linear-time/branching-time spectrum.

Abstract

A subclass of nondeterministic Finite Automata generated by means of regular Grammars (GFAs, for short) is introduced. A process algebra is proposed, whose semantics maps a term to a GFA. We prove a representability theorem: for each GFA $N$, there exists a process algebraic term $p$ such that its semantics is a GFA isomorphic to $N$. Moreover, we provide a concise axiomatization of language equivalence: two GFAs $N_1$ and $N_2$ recognize the same regular language if and only if the associated terms $p_1$ and $p_2$, respectively, can be equated by means of a set of axioms, comprising 7 axioms plus 2 conditional axioms, only.

Axiomatizing NFAs Generated by Regular Grammars

TL;DR

This work axiomatizes language equivalence on GFAs by embedding GFAs into a restricted process algebra , establishing a representability theorem that every GFA corresponds to an term with isomorphic semantics. It introduces a precise, compositional denotational semantics mapping terms to GFAs, and proves that language equivalence is a congruence for all operators, including recursion. The main contribution is a compact, sound and complete axiom system for language equivalence consisting of axioms plus conditional axioms, together with normal-form, saturation, and semi-deterministic techniques to prove completeness. The results enable algebraic reasoning about regular languages via a process-algebraic framework and offer a basis for extending the approach to other equivalences in the linear-time/branching-time spectrum.

Abstract

A subclass of nondeterministic Finite Automata generated by means of regular Grammars (GFAs, for short) is introduced. A process algebra is proposed, whose semantics maps a term to a GFA. We prove a representability theorem: for each GFA , there exists a process algebraic term such that its semantics is a GFA isomorphic to . Moreover, we provide a concise axiomatization of language equivalence: two GFAs and recognize the same regular language if and only if the associated terms and , respectively, can be equated by means of a set of axioms, comprising 7 axioms plus 2 conditional axioms, only.
Paper Structure (14 sections, 19 theorems, 2 equations, 6 figures, 3 tables)

This paper contains 14 sections, 19 theorems, 2 equations, 6 figures, 3 tables.

Table of Contents

  1. Introduction
  2. GFA: Finite Automata generated by regular Grammars
  3. SFM$_0$: Syntax and Semantics
  4. Syntax
  5. Denotational Semantics
  6. Congruence
  7. Algebraic Properties
  8. Axiomatization
  9. The Axioms
  10. Normal Forms and Unique Solutions
  11. Saturated Normal Forms
  12. Semi-deterministic Normal Form
  13. Completeness
  14. Conclusion

Key Result

theorem 1

For each SFM$_0$ process $p$, $\llbracket p \rrbracket_{\emptyset}$ is a reduced GFA. Proof. By induction on the definition of $\llbracket p \rrbracket_{I}$. Then, the thesis follows for $I = \emptyset$. The first base case is for $\hbox{\bf 0}$ and the thesis is obvious, as, for each $I \subseteq \

Figures (6)

  • Figure 1: An NFA recognizing the language $a^+b^+$
  • Figure 2: Graphical description of the representability theorem, up to isomorphism
  • Figure 3: A GFA and a DGFA both recognizing the language $a^*b^*$
  • Figure 4: Saturation and $\epsilon$-free DGFA
  • Figure 5: Two GFAs for Example \ref{['rep-ex']}
  • ...and 1 more figures

Theorems & Definitions (31)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • remark 1
  • definition 5
  • remark 2
  • definition 6
  • theorem 1
  • theorem 2
  • ...and 21 more