We introduce session automata, an automata model to process data words, i.e.,words over an infinite alphabet. Session automata support the notion of freshdata values, which are well suited for modeling protocols in which sessionsusing fresh values are of major interest, like in security protocols or ad-hocnetworks. Session automata have an expressiveness partly extending, partlyreducing that of classical register automata. We show that, unlike registerautomata and their various extensions, session automata are robust: They (i)are closed under intersection, union, and (resource-sensitive) complementation,(ii) admit a symbolic regular representation, (iii) have a decidable inclusionproblem (unlike register automata), and (iv) enjoy logical characterizations.Using these results, we establish a learning algorithm to infer sessionautomata through membership and equivalence queries.
展开▼
