Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning EFSM Models with Registers in Guards

Germán Vega, Roland Groz, Catherine Oriat, Michael Foster, Neil Walkinshaw, Adenilso Simão

TL;DR

The paper tackles learning $EFSM$ models that include internal registers in guards from a single, non-resettable trace. It extends the $hW$-inference backbone to handle parameterized inputs/outputs and guards driven by registers, using a structured sampling regime with sets $I_1 \\subset I_2 \\subset I_s$ and register partitions $R_w \\subseteq R_g$, guided by a homing sequence $h$ and a characterization set $W$. The method identifies the control structure as an NFSM, collects register-valued samples, and generalises to a full $EFSM$ via genetic programming, with counterexamples from a MAT-like framework refining the model. Experiments on a vending-machine scenario and a more complex guard-walking example illustrate feasibility and highlight practical challenges such as transfer optimization and scalability in the presence of guarded transitions and register updates.

Abstract

This paper presents an active inference method for Extended Finite State Machines, where inputs and outputs are parametrized, and transitions can be conditioned by guards involving input parameters and internal variables called registers. The method applies to (software) systems that cannot be reset, so it learns an EFSM model of the system on a single trace.

Learning EFSM Models with Registers in Guards

TL;DR

The paper tackles learning models that include internal registers in guards from a single, non-resettable trace. It extends the -inference backbone to handle parameterized inputs/outputs and guards driven by registers, using a structured sampling regime with sets and register partitions , guided by a homing sequence and a characterization set . The method identifies the control structure as an NFSM, collects register-valued samples, and generalises to a full via genetic programming, with counterexamples from a MAT-like framework refining the model. Experiments on a vending-machine scenario and a more complex guard-walking example illustrate feasibility and highlight practical challenges such as transfer optimization and scalability in the presence of guarded transitions and register updates.

Abstract

This paper presents an active inference method for Extended Finite State Machines, where inputs and outputs are parametrized, and transitions can be conditioned by guards involving input parameters and internal variables called registers. The method applies to (software) systems that cannot be reset, so it learns an EFSM model of the system on a single trace.
Paper Structure (6 sections, 8 figures, 4 algorithms)

This paper contains 6 sections, 8 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Running example and background models
  3. Assumptions for tractability
  4. Execution of method on running example
  5. A more complex example where $W$ traverses guards
  6. Conclusion

Figures (8)

  • Figure 1: Our vending machine EFSM and an example trace.
  • Figure 2: No register allowed in guard (from Foster2023ICFEM
  • Figure 3: Control NFSM of the vending machine.
  • Figure 4: Sampled FSM with trace from \ref{['fig:example-trace']}
  • Figure 5: Homing tails characterisations (internal SUL states shown only for reference)
  • ...and 3 more figures