%O Report 
%F jeron-marchand-rusu-pi-deter-06
%A Jéron, T.
%A Marchand, H.
%A Rusu, V.
%T Symbolic Determinisation of Extended Automata
%N 1176
%I IRISA
%X We define a symbolic determinisation procedure for a class of infinite-state systems, which consists of automata extended with symbolic variables that may be infinite-state. The subclass of extended automata for which the procedure terminates is characterised as bounded lookahead extended automata. It corresponds to automata for which, in any location, the observation of a bounded-length trace is enough to infer the first transition actually taken. We discuss applications of the algorithm to the verification, testing, and diagnosis of infinite-state systems
%U http://www.irisa.fr/vertecs/Publis/Ps/PI-1776.pdf
%8 February
%D 2006