Appliquer l'algorithme DFS à un système de transition pour trouver des états accessibles

Question

Travaillant actuellement sur une question d'examen antérieure qui me dit de calculer le produit de deux systèmes de transition puis Utilisez DFS pour trouver les états accessibles du produit. J'ai appris à calculer le produit des systèmes de transition en examinant les pages 43 et 44 dans le livre "Principes de la vérification du modèle" de Christel Baier et Joost-Pieter Katoen (si quelqu'un en a une copie).

Je comprends que la façon dont ils ont trouvé les états accessibles à la page 44 est de suivre la valeur de la variable Y pour chaque état et de voir si elle se déroule, mais dans ma question particulière, je n'utilise pas de graphique de programme; Il s'agit d'un système de transition qui utilise uniquement Sigma et Gamma (comme actions de poignée de main). Ma première question est de savoir comment déterminer ce qui est un état accessible et ce qui n'est pas dans un produit de systèmes de transition?

Deuxièmement, comment pourrais-je montrer que j'ai utilisé du DFS sur papier? Je n'ai pas trouvé d'articles utiles en ligne à ce sujet et nos notes de conférence ne le couvrent pas pour une raison quelconque.