Skip to Main content Skip to Navigation
Conference papers

Symbolic Determinisation of Extended Automata

Abstract : 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
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Hervé Marchand Connect in order to contact the contributor
Submitted on : Monday, October 19, 2009 - 8:42:46 AM
Last modification on : Friday, February 4, 2022 - 3:15:45 AM
Long-term archiving on: : Wednesday, June 16, 2010 - 12:52:21 AM


Files produced by the author(s)



Thierry Jéron, Hervé Marchand, Vlad Rusu. Symbolic Determinisation of Extended Automata. 4th IFIP International Conference on Theoretical Computer Science, Aug 2006, Stantiago, Chile, Chile. pp.197-212, ⟨10.1007/978-0-387-34735-6_18⟩. ⟨inria-00424858⟩



Record views


Files downloads