Learning and Equivalence of Automata with Resources

LEARn | F.R.S.-FNRS Research Project

LEARn LEARn develops algorithms and tools for learning and equivalence checking of automata with resources: computational models equipped with memory such as stacks, counters, weights, or mechanisms for representing nested structure.

The project is motivated by a practical challenge. Modern software systems routinely exchange large volumes of structured data, particularly in formats such as JSON. Reliable schemas are crucial for data validation, API contracts, and the safe use of tools by LLM-based systems, yet designing and maintaining these schemas by hand is often difficult and error-prone. LEARn investigates how automata learning can infer such structure automatically while retaining the formal guarantees needed for verification, analysis, and reliable software development.

Back to homepage

Overview

The central goal of LEARn is to advance both the theory and practical use of learning and equivalence checking for automata with resources. The project begins by studying the learning of visibly pushdown automata (VPA) for JSON schema inference, before extending its focus to equivalence checking for subclasses of weighted pushdown automata.

Visibly pushdown automata provide a natural formalism for data with nested structure, including JSON, XML, HTML, and program execution traces. By learning VPA from example documents, or black-box validators, LEARn aims to automatically construct formal models of structured data formats. These learned models can then support validation, automated analysis, and formal verification.

Motivation

Active automata learning constructs a model of an unknown system by posing structured queries to a black box. This approach is particularly valuable in software verification, where an explicit formal model may be unavailable or difficult to obtain directly. However, extending learning beyond finite automata to models with memory—such as counters and stacks—introduces substantial new challenges.

In practical learning settings, exact equivalence checking against the black-box system is usually unavailable. It is therefore replaced by conformance testing, which searches for discrepancies using carefully selected tests. For systems with stack-like memory, however, equivalence checking often remains the main theoretical and computational bottleneck. Developing stronger exact equivalence algorithms can reveal the structure, limitations, and algorithmic properties of these richer models.

LEARn builds on recent progress showing that the class of one-counter automata can be learned efficiently. It investigates how these ideas can be extended to richer models with stack-based memory, while using advances in exact equivalence checking to develop a deeper understanding of their behaviour and their potential for verification and analysis.

Research Themes

  • Learning VPA for JSON schemas: design scalable active learning algorithms for nested data formats, building on recent progress in learning one-counter automata.
  • Richer query models: study practical query types where the learner can obtain more information regarding the system's internal state during learning.
  • Weighted SDPDA equivalence: develop equivalence algorithms for subclasses of weighted pushdown models, including synchronised and deterministic real-time machines.
  • Automata with additional resources: explore active and passive learning for models with resources such as stacks, counters, weights, and timing constraints.

Objectives

Infer schemas:
derive visibly pushdown models from JSON schemas, examples, or black-box validators.
Scale learning:
reduce query counts and learning time for large alphabets and complex nested data.
Check equivalence:
develop algorithms for weighted pushdown models over fields.
Build tools:
produce open-source prototypes and benchmarks for realistic validation scenarios.

Algorithms and Tools

A central goal of the project is to deliver both theory and usable prototypes. The planned toolchain includes a schema-to-VPA learner, a streaming validator based on learned VPA, and benchmarks for comparing learning time, query complexity, model size, validation speed, and memory use.

The implementation will use and contribute to existing automata-learning ecosystems such as LearnLib and AutomataLib where appropriate. Case studies will include real and synthetic JSON datasets, open-source schemas, and validation scenarios for API messages.

Evaluation

The project will evaluate learned models on real and synthetic JSON datasets, including schemas and documents from open repositories. Experiments will measure membership and equivalence queries, learning time, model size, validation speed, and memory usage, with special attention to large and streaming JSON inputs.

Case studies will test whether automata-based validation can detect errors or improve performance compared with standard validation tools.

Impact

  • Reduce human effort by automating the construction and maintenance of complex schemas.
  • Increase trust in partially understood systems by synthesising formal models with correctness guarantees.
  • Support safer JSON-based interactions in APIs, validation frameworks, and LLM tool-calling workflows.
  • Extend automata learning beyond regular languages toward richer stack-based and weighted models.
  • Advance equivalence-checking techniques for models connected to probabilistic and weighted pushdown systems.