Reference. SMT-Based Active Learning of Weighted Automata
We present an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/-style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to produce minimal WFAs. We prove partial correctness and provide a sufficient termination condition, which in particular implies termination for all finite semirings. Our extensive experimental evaluation shows that our algorithm is capable of learning numerous minimal WFAs over both finite and infinite semirings, vastly outperforms a naive baseline, and is competitive with a state-of-the-art algorithm while producing significantly smaller automata and requiring less interaction with the teacher.
Cite
Cites 36 works (1 here)
With notes (1)
Weighted NetKAT: A Programming Language for Quantitative Network Verification suarezacevedo-2026-weighted
We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative quantitative network properties. The language is parametric on a semiring , enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata ( WNKA ) capturing the stateful behavior of our language. With WNKA , we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2’s Abilene network as the underlying topology.
External (35)
- SMT-Based Active Learning of Weighted Automata (artifact) (2026)
- Learning Weighted Automata over Number Rings, Concretely and Categorically (2025)
- Feasability of Learning Weighted Automata on a Semiring (2025)
- On Learning Polynomial Recursive Programs (2024)
- Scalable Tree-based Register Automata Learning (2024)
- Automated Passport Control: Mining and Checking Models of Machine Readable Travel Documents (2024)
- An L* Algorithm for Deterministic Weighted Regular Languages (2024)
- Automata Learning with an Incomplete Teacher (2023)
- Weighted programming: a programming paradigm for specifying mathematical models (2022)
- Timed Automata Learning via SMT Solving (2022)
- Prognosis: closed-box analysis of network protocol implementations (2021)
- What's decidable about weighted automata? (2020)
- Learning Weighted Automata over Principal Ideal Domains (2020)
- Benchmarks for Automata Learning and Conformance Testing (2019)
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions (2018)
- Model learning (2017)
- Combining Model Learning and Model Checking to Analyze TCP Implementations (2016)
- Learning the Language of Error (2015)
- Efficient inference of Mealy machines (2014)
- Formal Models of Bank Cards for Free (2013)
- Sound and Complete Axiomatizations of Coalgebraic Language Equivalence (2013)
- δ-Complete Decision Procedures for Satisfiability over the Reals (2012)
- Inference and Abstraction of the Biometric Passport (2010)
- Exact DFA Identification Using SAT Solvers (2010)
- Handbook of Weighted Automata (2009)
- Angluin-style learning of NFA (2009)
- Z3: An Efficient SMT Solver (2008)
- Experimental Evaluation of Classical Automata Constructions (2005)
- Residual Finite State Automata (2001)
- Efficient Algorithms for the Inference of Minimum Size DFAs (2001)
- Black Box Checking (1999)
- Learning Behaviors of Automata from Multiplicity and Equivalence Queries (1996)
- Test selection based on finite state models (1991)
- Learning regular sets from queries and counterexamples (1987)
- On the Synthesis of Finite-State Machines from Samples of Their Behavior (1972)