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.
This work was partially supported by ARC Discovery Grant, DP0559927.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Etessami, K., Yannakakis, M.: Analysis of Recursive State Machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 207–220. Springer, Heidelberg (2001)
Barrett, W.A., Bates, R.M., Gustafson, D.A., Couch, J.D.: Compiler Construction: Theory and Practice, 2nd edn. Science Research Associates (1986)
Benedikt, M., Godefroid, P., Reps, T.: Model Checking of Unrestricted Hierarchical State Machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 652–666. Springer, Heidelberg (2001)
Billington, J., Gallasch, G.E., Han, B.: A Coloured Petri Net Approach to Protocol Verification. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 210–290. Springer, Heidelberg (2004)
Billington, J., Han, B.: Formalising TCP’s Data Transfer Service Language: A Symbolic Automaton and its Properties. Fundamenta Informaticae 80(1-3), 49–74 (2007)
Gallasch, G.E., Billington, J.: A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 201–218. Springer, Heidelberg (2006)
Gallasch, G.E., Billington, J.: Parametric Language Analysis of the Class of Stop-and-Wait Protocols. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 191–210. Springer, Heidelberg (2008)
Gordon, S., Billington, J.: Analysing a Missile Simulator with Coloured Petri Nets. Int. J. on Software Tools for Technology Transfer 2(2), 144–159 (1998)
ITU: Recommendation H.245, Control protocol for multimedia communication (2005)
Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, 2nd edn., vol. 1. Springer, Heidelberg (1997)
Liu, L., Billington, J.: Tackling the Infinite State Space of a Multimedia Control Protocol Service Specification. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 273–293. Springer, Heidelberg (2002)
Liu, L., Billington, J.: A Proof of the Recursive Formula for the Infinite Service Language of the CES Protocol. Technical report, CSEC-13, Computer Systems Engineering Centre, University of South Australia (2004)
Liu, L., Billington, J.: Obtaining the Service Language for H.245’s Multimedia Capability Exchange Signalling Protocol: the Final Step. In: 10th Int. Multi-Media Modelling Conference, pp. 323–328. IEEE, Los Alamitos (2004)
Liu, L., Billington, J.: Reducing Parametric Automata: A Multimedia Protocol Service Case Study. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 483–486. Springer, Heidelberg (2004)
Louden, K.C.: Compiler Construction: Principles and Practice. PWS Publishing Company (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 IFIP International Federation for Information Processing
About this paper
Cite this paper
Liu, L., Billington, J. (2009). Recursive Parametric Automata and ε-Removal. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2009 2009. Lecture Notes in Computer Science, vol 5522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02138-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-02138-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02137-4
Online ISBN: 978-3-642-02138-1
eBook Packages: Computer ScienceComputer Science (R0)