Synthétise symbolique via les BDD

Cette séance de cours couvre la synthèse réactive symbolique efficace pour les tâches d'horizon fini à l'aide de diagrammes de décision binaires (BDD) pour représenter compactement les fonctions et ensembles booléens, comme l'ont démontré Keliang He, Andrew Wells, Lydia E. Kavraki et Moshe Y. Vardi de l'Université de Rice. La présentation se penche sur les principales parties du problème, y compris le système de transition et le DFA, données en ce qui concerne les variables booléennes, et les calculs impliquant des fonctions et des ensembles booléens. La séance de cours comprend également un exemple de Wikipédia et fait référence à un article de R. E. Bryant sur les algorithmes basés sur des graphiques pour la manipulation des fonctions booléennes.