Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Active Learning Techniques for Pomset Recognizers

Adrien Pommellet, Amazigh Amrane, Edgar Delaporte, Geoffroy Du Prey, Oscar Peyron

TL;DR

This work extends active learning to the domain of recognizable series-parallel pomset languages by developing PL^\lambda, an algorithm that adapts the state-of-the-art L^\lambda approach to pomset recognizers built on bimonoids. It introduces a new counterexample analysis, FindEBP, which reduces queries to discover refining information from counterexamples, and replaces many equivalence checks with a refined discriminative structure that leverages depth-aware breaking points. A finite test-suite framework extending the W-method is proposed to ensure general equivalence between pomset recognizers using membership queries, under a known bound on model size. Empirical results show significant reductions in membership and symbol complexity when using PL^\lambda with FindEBP compared to PL^* and HCE, indicating practical improvements for automated reasoning about concurrent systems. The work also outlines future directions, including extensions to broader pomset classes (e.g., HDA) and improvements to test-suite strategies.

Abstract

Pomsets are a promising formalism for concurrent programs based on partially ordered sets. Among this class, series-parallel pomsets admit a convenient linear representation and can be recognized by simple algebraic structures known as pomset recognizers. Active learning consists in inferring a formal model of a recognizable language by asking membership and equivalence queries to a minimally adequate teacher (MAT). We improve existing learning algorithms for pomset recognizers by 1. introducing a new counter-example analysis procedure that is in the best case scenario exponentially more efficient than existing methods 2. adapting the state-of-the-art $L^λ$ algorithm to minimize the impact of exceedingly verbose counter-examples and remove redundant queries 3. designing a suitable finite test suite that ensures general equivalence between two pomset recognizers by extending the well-known W-method.

Active Learning Techniques for Pomset Recognizers

TL;DR

This work extends active learning to the domain of recognizable series-parallel pomset languages by developing PL^\lambda, an algorithm that adapts the state-of-the-art L^\lambda approach to pomset recognizers built on bimonoids. It introduces a new counterexample analysis, FindEBP, which reduces queries to discover refining information from counterexamples, and replaces many equivalence checks with a refined discriminative structure that leverages depth-aware breaking points. A finite test-suite framework extending the W-method is proposed to ensure general equivalence between pomset recognizers using membership queries, under a known bound on model size. Empirical results show significant reductions in membership and symbol complexity when using PL^\lambda with FindEBP compared to PL^* and HCE, indicating practical improvements for automated reasoning about concurrent systems. The work also outlines future directions, including extensions to broader pomset classes (e.g., HDA) and improvements to test-suite strategies.

Abstract

Pomsets are a promising formalism for concurrent programs based on partially ordered sets. Among this class, series-parallel pomsets admit a convenient linear representation and can be recognized by simple algebraic structures known as pomset recognizers. Active learning consists in inferring a formal model of a recognizable language by asking membership and equivalence queries to a minimally adequate teacher (MAT). We improve existing learning algorithms for pomset recognizers by 1. introducing a new counter-example analysis procedure that is in the best case scenario exponentially more efficient than existing methods 2. adapting the state-of-the-art algorithm to minimize the impact of exceedingly verbose counter-examples and remove redundant queries 3. designing a suitable finite test suite that ensures general equivalence between two pomset recognizers by extending the well-known W-method.
Paper Structure (45 sections, 12 theorems, 2 equations, 15 figures, 7 algorithms)

This paper contains 45 sections, 12 theorems, 2 equations, 15 figures, 7 algorithms.

Table of Contents

  1. Introduction
  2. Related works
  3. Pomset languages.
  4. Active learning algorithms for finite state machines.
  5. Active learning algorithms for parallel models.
  6. Preliminary Definitions
  7. Series-parallel pomsets
  8. Pomset recognizers
  9. Contexts
  10. A Myhill-Nerode theorem
  11. An Active Learning Algorithm for Pomset Recognizers
  12. Data structures
  13. Covering the congruence classes.
  14. Distinguishing the congruence classes.
  15. Properties of the partition.
  16. ...and 30 more sections

Key Result

theorem 1

A language $L \subseteq \mathrm{SP}(\Sigma)$ is recognizable if and only if $\sim_L$ has finite index, i.e. $\mathrm{SP}(\Sigma) \mathop{\mathrm{/}}\nolimits {\sim_{L}}$ is finite.

Figures (15)

  • Figure 1: The series-parallel pomset $a (b \parallel b) c (ba \parallel bb)$.
  • Figure 2: The term $bc \parallel a$.
  • Figure 3: First pack of components, a discrimination tree, and the resulting hypothesis.
  • Figure 4: The various components of the $\mathit{PL}^\lambda$ algorithm.
  • Figure 5: Second and third packs of components, second discrimination tree.
  • ...and 10 more figures

Theorems & Definitions (37)

  • definition 1: Series-parallel terms
  • definition 2: Series-parallel pomsets
  • definition 3: Bimonoids bloom1996free
  • definition 4: Pomset recognizers
  • definition 5: Multi-contexts
  • theorem 1: LW00:sp
  • definition 6: Reachable, distinguished, minimal pomset recognizers
  • definition 7: Agreement
  • definition 8: Breaking point
  • lemma 1
  • ...and 27 more