Symbolic Language Representations for Parametric Verification of the Revised Capability Exchange Signalling Protocol

Parametric protocol verification is a challenging r-e- search topic. Obtaining symbolic representations of service and protocol languages of a protocol enables parametric verification of the protocol against its service specification. In this paper, we exploit recurrent structural regularities of state spaces to obtain symbolic representations of protocol languages for the revised Capability Exchange Signalling (CES) protocol. This leads to conjectures on a recursive expression for the revised CES protocol language and for the inclusion of the revised CES protocol language in the CES service language, for any values of the parameters. This result also demonstrates the promising future of our approach to finding symbolic representations for service and/or protocol languages.