Recursive parametric automata and ε-removal
Date
2009
Authors
Liu, L.
Billington, J.
Editors
Lee, L.
David, D.
David, D.
Advisors
Journal Title
Journal ISSN
Volume Title
Type:
Book chapter
Citation
Event/exhibition information: 11th International Conference on Formal Methods for Open Object-Based Distributed Systems, Lisbon, Portugal, 09/06/2009-11/06/2009
Source details - Title: Formal techniques for distributed systems : Joint 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009 : proceedings, 2009 / Lee, L., David, D. (ed./s), vol.5522 LNCS, pp.90-105
Statement of Responsibility
Conference Name
Abstract
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.
School/Discipline
Dissertation Note
Provenance
Description
Access Status
Rights
Copyright 2009 IFIP International Federation for Information Processing