This work is motivated by and arose from the parametric verification of communication protocols over unbounded channels, where the channel capacity is the parameter. Verification required the use of finite state automata (FSA) reduction, including ε-removal, for a specific infinite family of FSA. This paper generalises this work by introducing Recursive Parametric FSA (RP-FSA), an infinite family of FSA that can be represented recursively in a single parameter. Further, the paper states and proves a necessary and sufficient condition regarding the transformation of a RP-FSA to its language equivalent ε-removed family of FSA that is also a RP-FSA in the same parameter. This condition also guarantees a further structural property regarding the RP-FSA and its ε-removed family. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Liu, L., & Billington, J. (2009). Recursive parametric automata and ε-removal. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5522 LNCS, pp. 90–105). https://doi.org/10.1007/978-3-642-02138-1_6
Mendeley helps you to discover research relevant for your work.