%0 Conference Proceedings
%F jeron-marchand-rusu-tcs-deter-06
%A Jéron, T.
%A Marchand, H.
%A Rusu, V.
%T Symbolic Determinisation of Extended Automata
%B 4th IFIP International Conference on Theoretical Computer Science
%P 197-212
%S IFIP book series
%I Springer Science and Business Media
%C Stantiago, Chile
%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/TCS-2006-deter.pdf
%U http://dx.doi.org/10.1007/978-0-387-34735-6_18
%8 August
%D 2006