arXiv:2504.16624cs.LGcs.FL2025-04被引 3

自动分解并发系统,用字母精炼提升学习效率。

A Detailed Account of Compositional Automata Learning through Alphabet Refinement

  • 通过字母精炼将全局行为分解为组件模型。
  • 实验显示比单体学习少5个数量级的查询次数。
  • 适合高并发系统建模,对算法工程师有实用价值。

主动自动机学习从行为观测中推断系统模型,已广泛应用于多个领域。针对并发系统的可扩展性问题,本文提出一种通用的组合式学习方法,无需预先知道系统分解方式。该方法在学习过程中自动将全局字母表细分为组件字母表,并构建字母分布的理论框架,刻画不一致的反例,系统性地更新字母分布以恢复一致性。我们扩展了$ L^{/star} $算法,以处理仅从全局观测中学习组件时产生的部分和可能虚假的信息。证明了整个算法的正确性与终止性。实现名为CoalA,基于先进的主动学习库LearnLib。在630多个系统上的实验表明,CoalA相比单体学习减少了最多五个数量级的成员查询,并在显著并发的系统上展现出更优的等价查询可扩展性。

原文摘要 · Abstract (English)

Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches have recently emerged to address scalability to concurrent systems. We take a significant step beyond available results, including those by the authors, and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. Our approach automatically refines the global alphabet into component alphabets while learning the component models. We develop a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets, characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. We extend $L^{\star}$ to handle partial and potentially spurious information arising when learning components from global observations only. We establish correctness and termination of the full algorithm. We provide an implementation, called CoalA, using the state-of-the-art active learning library LearnLib. Our experiments on more than 630 subject systems show that CoalA delivers up to five orders of magnitude fewer membership queries than monolithic learning, and achieves better scalability in equivalence queries on systems with significant concurrency.

自动机学习组合方法并发系统字母精炼

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。