Verification of Parametric Markov Automata under Time-bounded Reachability

Résumé Technique : Vérification d'Automates de Markov Paramétriques sous la Réachabilité à Temps Borné

Énoncé du Problème
Les Automates de Markov (MA) sont un modèle compositionnel pour les systèmes stochastiques déterministes et continus dans le temps, servant de sémantique pour des modèles tels que les réseaux de Petri stochastiques généralisés et les arbres de défaillance dynamiques. Cependant, les algorithmes de model checking existants pour les MA nécessitent des modèles entièrement spécifiés, où tous les taux de transition et les probabilités sont connus avec précision. Cette hypothèse est souvent irréaliste pour des systèmes du monde réel où les paramètres peuvent être soumis à une incertitude environnementale ou être inconnus.

Cet article traite de la vérification des Automates de Markov Paramétriques (pMA), où les taux de transition et les distributions de successeurs probabilistes sont définis par des fonctions paramétriques plutôt que par des constantes fixes. Les auteurs se concentrent sur les propriétés de réachabilité à temps borné (par exemple, « La probabilité d'atteindre un état cible dans un temps $t$ est-elle supérieure à $\theta$ ? »). Deux problèmes spécifiques sont abordés :

1. Vérification de la Satisfaction : Déterminer s'il existe une évaluation de paramètre au sein d'une région donnée qui satisfait ou viole une propriété.
2. Synthèse : Partitionner l'espace des paramètres en régions qui satisfont la propriété et régions qui la violent.

L'analyse doit tenir compte de quatre relations de satisfaction distinctes basées sur l'interaction entre l'ordonnanceur du système (faisant des choix non déterministes) et la « nature » (assignant des valeurs de paramètres) : Faisabilité, Aide Angélique, Robuste et Démoniaque.

Méthodologie
L'approche proposée résout ces problèmes via un processus en deux étapes qui transforme le modèle paramétrique continu en un modèle discret exploitable par les techniques de synthèse existantes, tout en bornant les erreurs introduites.

1. Discrétisation et Transformation :

   • Le pMA est d'abord discrétisé à l'aide d'un pas de discrétisation $\delta$, convertissant le modèle en temps continu en un Processus de Décision de Markov Paramétrique (pMDP). Cette étape généralise les résultats de discrétisation précédents pour les MA non paramétriques.
   • Pour gérer les transitions immédiates des états probabilistiques (qui se produisent sans écoulement du temps), les auteurs emploient une technique d'élimination d'états. Les états probabiliques (PS) sont fusionnés en états markoviens (MS), transformant le modèle en un problème de réachabilité standard à pas borné sur un pMDP.
   • Puisque la discrétisation introduit des termes exponentiels ($e^{-\lambda \delta}$) difficiles à traiter dans la synthèse de paramètres symbolique, les auteurs approximent ces termes en utilisant des développements de Taylor partiels. Cela produit un « pMA discrétisé approximatif » où les probabilités de transition sont représentées par des fonctions rationnelles, bornées par des approximations supérieures et inférieures.

2. Élévation de Paramètres (PL) et Vérification :

   • Le pMDP transformé est analysé en utilisant l'Élévation de Paramètres (PL). Cette technique abstrait les dépendances entre états en traitant les choix de paramètres comme des choix non déterministes faits par un second joueur (« la Nature ») dans un jeu stochastique.
   • La méthode PL calcule des bornes supérieures et inférieures pour la probabilité de réachabilité. Ces bornes sont comparées au seuil spécifié par l'utilisateur $\theta$.
   • L'approche utilise un schéma de raffinement : si les bornes sont non concluantes (c'est-à-dire si l'intervalle traverse le seuil), la région de paramètres est partitionnée, et le processus est répété.
   • L'erreur totale est régie par trois termes : l'erreur de discrétisation ($\epsilon_\delta$), l'erreur de l'approximation de Taylor, et l'erreur introduite par l'abstraction PL. Les auteurs démontrent que l'erreur de discrétisation est le facteur dominant.

Contributions Clés

• Définition de pMA : Le papier introduit formellement les Automates de Markov Paramétriques, étendant les MA avec des fonctions de taux et de probabilité paramétriques.
• Algorithme pour la Réachabilité à Temps Borné : Les auteurs présentent le premier algorithme capable d'effectuer la vérification de satisfaction et la synthèse de paramètres pour les pMA sous des contraintes de réachabilité à temps borné.
• Discrétisation Généralisée : Ils généralisent les résultats de discrétisation de Guck et al. [17] au cadre paramétrique, prouvant que le pMA discrétisé borne la probabilité de réachabilité réelle du pMA.
• Discrétisation Approximative : Une méthode est introduite pour gérer les termes exponentiels dans le modèle discrétisé via le développement de Taylor, permettant l'utilisation d'outils de synthèse basés sur des fonctions rationnelles.
• Implémentation : L'approche est implémentée en utilisant le model checker Storm (via l'interface Stormpy) et supporte à la fois les pMA et les CTMC paramétriques.

Résultats Expérimentaux
Les auteurs ont évalué leur implémentation sur une suite de benchmarks du set de benchmarks QCOMP, incluant des modèles comme flexible-manufacturing, polling, et kanban.

• Vérification : Pour la vérification de satisfaction, l'outil a fourni des réponses concluantes pour tous les benchmarks testés, souvent en quelques secondes.
• Synthèse : Pour la synthèse de paramètres, l'outil a réussi à partitionner les espaces de paramètres pour les modèles plus petits. Cependant, pour des modèles plus larges ou complexes, le processus a fréquemment atteint le délai d'expiration de 15 minutes.
• Goulots d'étranglement de Performance : L'analyse expérimentale identifie la discrétisation comme le principal goulot d'étranglement de performance. Le coût computationnel augmente significativement à mesure que le pas de discrétisation $\delta$ diminue (pour réduire l'erreur) ou que le taux de séjour maximal dans le modèle augmente.
• Comparaison : Comparé à PRISM-PSY sur les CTMC paramétriques (où PRISM-PSY ne nécessite pas de discrétisation), la méthode proposée est plus lente. Cependant, la méthode réussit là où PRISM-PSY échoue : elle peut analyser les pMA et les modèles avec des probabilités de transition paramétriques (pas seulement des taux), tels que le benchmark tandem.

Signification et Revendications
Le papier affirme combler une lacune dans la vérification formelle en permettant l'analyse de l'incertitude dans les Automates de Markov, une classe de modèles largement utilisée en ingénierie de la fiabilité mais auparavant restreinte à des instances entièrement spécifiées. Les auteurs soulignent que leur approche résout les problèmes de vérification et de synthèse jusqu'à une précision arbitraire, à condition que le pas de discrétisation soit suffisamment petit.

Les auteurs restent modestes quant à la scalabilité, reconnaissant que l'implémentation actuelle est limitée par le coût de la discrétisation. Ils déclarent explicitement que les principaux goulots d'étranglement de performance proviennent de la discrétisation du pMA. Par conséquent, ils suggèrent que les travaux futurs devraient étudier des approches évitant totalement la discrétisation, comme l'analyse directe de jeux stochastiques en temps continu ou l'utilisation de techniques d'uniformisation, tout en notant que ces alternatives peuvent introduire leurs propres défis computationnels. Ce travail établit un cadre fondamental pour l'analyse paramétrique de systèmes non déterministes en temps continu, étendant les capacités des outils existants comme Storm pour gérer l'incertitude paramétrique dans une classe de modèles plus large.