Résumé - Étudier les séquences d'auto-localisation et de synchronisation pour les Machines à États Finis Tempsés avec des délais de sortie

Étudier les séquences d'auto-localisation et de synchronisation pour les Machines à États Finis Tempsés avec des délais de sortie

2025-07-19 08:03:14

{"Evgenii Vinarskii","Jakub Ruszil","Adam Roman","Natalia Kushik"}

{cs.FL,cs.CC}

Ce document s'immerge dans l'étude des séquences de retour et de synchronisation pour les Machines à États Finis Tempsés (TFSM) avec des délais de sortie, enquêtant sur leurs propriétés et dérivant des méthodes. Les auteurs définissent des séquences de retour et de synchronisation pour les TFSM avec des délais de sortie, démontrant que plusieurs propriétés qui s'appliquent aux machines non temporelles ne s'appliquent pas nécessairement aux machines temporelles. Ils explorent diverses approches pour dériver ces séquences, y compris les méthodes basées sur l'arbre des successeurs tronqués et les méthodes basées sur l'abstraction des FSM. Le document identifie des sous-classes de TFSM pour lesquelles ces approches peuvent être directement appliquées et celles pour lesquelles d'autres méthodes sont nécessaires. Il évalue également la complexité de la vérification de l'existence et de la dérivation des séquences de retour et de synchronisation (les plus courtes) pour les TFSM avec des délais de sortie. Les découvertes clés incluent : - Les auteurs introduisent des séquences de retour et de synchronisation pour les TFSM avec des délais de sortie et démontrant leurs propriétés. - Ils explorent diverses approches pour dériver ces séquences, y compris les méthodes basées sur l'arbre des successeurs tronqués et les méthodes basées sur l'abstraction des FSM. - Ils identifient des sous-classes de TFSM pour lesquelles ces approches peuvent être directement appliquées. - Ils évaluent la complexité de la vérification de l'existence et de la dérivation des séquences de retour et de synchronisation (les plus courtes). - Ils proposent une abstraction de FSM modifiée pour faciliter la dérivation de ces séquences pour les TFSM avec des délais de sortie. - Ils étudient les propriétés de la correspondance entre les séquences de retour et de synchronisation pour les TFSM avec des délais de sortie et leurs abstractions non temporelles. Dans l'ensemble, le document contribue à la compréhension des séquences de retour et de synchronisation pour les TFSM avec des délais de sortie, fournissant des informations sur leurs propriétés et leurs méthodes de dérivation.