## 4 Modeling the Identity Registration Status  
The applications, that use the RIM API, and the FRMCS system need to have synchronized views on the identity registration status. Figure 8 shows the application's view on the registration status of \"Cab radio\" UE, its functional identities, user identity, and user functional identities. Figure 7: Subscription management and notifications about status changes in UE functional number registration. In the DeregisteredUE state, the UE is attached to the FRMCS network, but it is not registered in the FRMCS system. FRMCS application(s) are ready for use. In the UER Registering state, the application waits for the approval/rejection of a UE identity from the FRMCS system. In the RegisteredUE state, the UE is logged in to the FRMCS system and the application may create a subscription for notifications about the UE registration status. In the UERRegistering state, the application waits for the approval/rejection of the UE functional numbers from the FRMCS system. In the RegisteredUEFunctionalNumber state, one or more UE functional number(s) are logged in to the FRMCS system, and the application may create a subscription for notifications about the registration status of UE functional numbers. In the UserRegistering state, the application waits for the approval/rejection of a user identity from the FRMCS system. In the RegisteredUserlentity state, the user is logged in, and the application may create a subscription for notifications about the user registration status. In the UserFIDRegistering state, the user waits for the approval/rejection of his/her functional identity from the FRMCS system. In the RegisteredUserFunctionalIdentity state, one or more user functional identities are registered into the FRMCS system, and the application may subscribe for notifications about the registration status of user functional identities. Both the user and FRMCS system may deregister any of the registered identities. Registrations may have a temporary duration, and, in this case, the FRMCS may request periodic registration status updates from the UE. If a registration update has not been received, the FRMCS system deregisters the respective identity. Figure 8 is simplified, as it does not include the behavior in which a registration update is requested for brevity. Figure 9 shows the FRMCS system's view on the registration status \"Cab radio\" UE, its functional identities, user identity, and user functional identities. Figure 8: How the application views the registration status of \"Cab radio\" UE, its functional identities, user identity, and user functional identities. In the UEnotRegistered state, the UE is not registered in the FRMCS system. In the UERegistered state, the UE identity is registered in the FRMCS system. In the UEFRRegistered state, one or more UE functional numbers are logged in to the FRMCS system. In the UserRegistered state, the user is logged in to the FRMCS system. In the UserFIDRegistered state, one or more user functional identities are registered. In each registered state, the FRMCS system maintains the respective timers determining the valid registration duration. In case a request for a registration update has not been received, the FRMCS system deregisters the identity. Other events may also trigger the deregistration of any registered identity by the FRMCS system, e.g., due to administrative reasons (not shown in Figure 9). In cases where there are changes in the registration status, the FRMCS system notifies the applications with active subscriptions. The models are simplified, as the figures do not show subscription termination in cases of identity deregistration. To prove that the models expose equivalent behavior, i.e., they support synchronized views on the identity registration status, the models are formally described and a bisimulation relationship between their states is identified. The formal model description uses a Labeled Transition System (LTS) to prove the behavioral synchronism of both state machines.