A Fresh Approach to Learning Register Automata

This paper provides an Angluin-style learning algorithm for a class of register automata supporting the notion of fresh data values. More specifically, we introduce session automata which are well suited for modeling protocols in which sessions using fresh values are of major interest, like in security protocols or ad-hoc networks. We show that session automata (i) have an expressiveness partly extending, partly reducing that of register automata, (ii) admit a symbolic regular representation, and (iii) have a decidable equivalence problem. We use these results to establish a learning algorithm that can infer inherently non-deterministic session automata. Moreover, in the case of deterministic automata, it has a better complexity wrt. membership queries than existing learning algorithms for register automata. We strengthen the importance of our automaton model by its characterization in monadic second-order logic.

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00743240
Author Bollig, Benedikt, Habermehl, Peter, Leucker, Martin, Monmege, Benjamin
Maintainer CCSD
Last Updated May 10, 2026, 18:31 (UTC)
Created May 10, 2026, 18:31 (UTC)
Identifier hal-00743240
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Laboratoire Spécification et Vérification [Cachan] (LSV) ; École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)
creator Bollig, Benedikt
date 2012-03-20T00:00:00
harvest_object_id 73a953f1-79cc-4669-aeb3-80c44cb51eb3
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2026-04-23T00:00:00
set_spec type:REPORT