Automata

Introduction

The automata module (aria/automata) provides implementations of finite automata and related algorithms for formal language processing and constraint solving. It includes both classical finite automata (DFA/NFA) and symbolic automata for string constraint solving.

Key Features

  • Finite Automata: DFA and NFA manipulation and conversion

  • Symbolic Automata: Symbolic finite automata with theory-based transitions

  • Automata Learning: Active learning algorithms for automata inference

  • Vendored AALpy: Upstream automata-learning toolkit under ARIA namespace

  • String Constraint Solving: Integration with SMT solvers for string theories

Components

Finite Automata (aria/automata/fa.py)

Basic finite automata operations:

from aria.automata.fa import DFA, NFA

# Create a DFA
dfa = DFA(
    states={'q0', 'q1', 'q2'},
    alphabet={'a', 'b'},
    transitions={('q0', 'a'): 'q1', ('q1', 'b'): 'q2'},
    initial_state='q0',
    accepting_states={'q2'}
)

# Accept strings
result = dfa.accepts("ab")  # True

Symbolic Automata (aria/automata/symautomata)

Symbolic finite automata framework supporting predicate-guarded transitions. This module is adapted from the symautomata project.

The current symbolic API is centered on aria.automata.symautomata.SFA and the guard types Predicate, SetPredicate, and Z3Predicate.

SetPredicate is the finite-alphabet implementation. Z3Predicate is the solver-backed implementation for symbolic domains.

SFA also bridges to the older concrete DFA workflows:

from aria.automata.symautomata import SFA
from aria.automata.symautomata.dfa import DFA

dfa = DFA(["a", "b"])
dfa.add_arc(0, 1, "a")
dfa[1].final = True

sfa = SFA.from_acceptor(dfa)
regex = sfa.to_regex()

Important semantic limits:

  • SFA.concretize(), SFA.save(), and SFA.load() require a finite alphabet.

  • SFA.complete() and SFA.complement() require either a finite alphabet or a predicate_factory that can produce a predicate over the intended symbolic universe.

  • Finite save/load workflows serialize concrete symbols, not symbolic formulas.

Automata Learning (aria/automata/fa_learning.py)

Active learning algorithms for inferring automata from examples:

from aria.automata.fa_learning import learn_automaton

# Learn DFA from membership queries
automaton = learn_automaton(examples, membership_oracle)

Vendored AALpy (aria/automata/aalpy)

ARIA also carries a vendored copy of the upstream AALpy package as aria.automata.aalpy.

Use this namespace when you want the broader active/passive learning toolkit, including reusable oracles, SUL wrappers, stochastic learners, and visibly pushdown automata support.

from aria.automata.aalpy.learning_algs import run_Lstar
from aria.automata.aalpy.oracles import RandomWalkEqOracle
from aria.automata.aalpy.SULs import AutomatonSUL

See AALpy for the vendored package overview and API reference.

Applications

  • String constraint solving in SMT

  • Regular expression analysis

  • Program verification with string operations

  • Vulnerability detection in web applications

References

  • Hopcroft, J. E., & Ullman, J. D. (1979). Introduction to Automata Theory, Languages, and Computation

  • D’Antoni, L., & Veanes, M. (2014). Minimization of Symbolic Automata. POPL 2014

  • Angluin, D. (1987). Learning Regular Sets from Queries and Counterexamples