UPPAAL TIGA est une extension de UPPAAL [BDL04] et il met en œuvre le premier algorithme on-the-fly efficace pour résoudre des jeux basés sur chronométré automates de jeu par rapport à joignabilité et de sécurité des propriétés.
Bien que les jeux chronométrés ont longtemps été connu pour être décidable il a jusqu'à présent été un manque d'algorithmes efficaces et bien sur la volée pour leur analyse.
UPPAAL TIGA fournit une interface graphique conviviale avec son serveur correspondant, et un vérificateur de ligne de commande.
L'algorithme que nous proposons [CDFLL05] est une extension symbolique de l'algorithme on-the-fly suggéré par Liu & Smolka [LS98] pour temps linéaire model-checking de systèmes à états finis. Être sur la volée, l'algorithme symbolique peut résilier à long avant d'avoir exploré l'espace de l'Etat entier.
De plus, les différentes étapes de l'algorithme sont effectuées de manière efficace par l'utilisation de ce qu'on appelle des zones en tant que structure de données sous-jacente. Notre outil implémente diverses optimisations de l'algorithme symbolique de base, ainsi que des méthodes pour obtenir des stratégies de temps optimal gagnantes (pour les jeux d'accessibilité).
Quoi de neuf dans cette version:
Commentaires non trouvées