Systèmes d'addition vectorielle avec des «obstacles» finis

11

Un système d'addition vectorielle (VAS) est un ensemble fini d' actions AZd . Nd est l'ensemble des marquages . Une course est un mot non vide de marques m0m1mn st i{0,,n1},mi+1miA . Si un tel mot existe, nous disons que mn est accessible à partir de m0 .

Le problème de l'accessibilité des VAS est connu pour être décidable (mais sa complexité est un problème ouvert).

Supposons maintenant qu'un ensemble fini de marquages ​​interdits (les obstacles ) soit donné. Je voudrais savoir si le problème de l'accessibilité est encore décidable.

Intuitivement, l'ensemble fini d'obstacles ne devrait interférer avec les trajets que localement, de sorte que le problème devrait rester décidable. Mais il ne semble pas trivial de le prouver.

MODIFIER . Je garderai la réponse de @ Jérôme comme étant acceptée, mais je voudrais ajouter une question de suivi: que se passe-t-il si l'ensemble des marquages ​​est Zd ?

Nicolas Perrin
la source
avez-vous une bonne référence pour avoir une intuition des idées derrière la preuve de décidabilité? (par exemple des diapositives)
Denis
1
Voici les slides: lsv.ens-cachan.fr/Events/Pavas/slides-Leroux.pdf ; et un article récent: hal.archives-ouvertes.fr/hal-00674970 ; Fondamentalement, l'accessibilité est résolue par un algorithme d'énumération, basé sur le fait que si n'est pas accessible à partir de x , alors il existe deux ensembles de Presburger disjoints qui prouvent en quelque sorte l'inaccessibilité. Quelques autres diapositives: automata.rwth-aachen.de/movep2010/abstracts/slides-leroux.pdf . yx
Nicolas Perrin
M Praveen a donné plusieurs conférences sur les deux principales approches du problème: cmi.ac.in/~praveenm/talks
Sylvain
Pour les sous-cas du problème avec des obstacles finis (par exemple de dimension restreinte), il semble qu'une preuve de décidabilité pourrait être basée sur une propriété "d'élimination du zigzag". Voir cet article: labri.fr/perso/leroux/published-papers/LS-concur04.ps , et ces diapositives: labri.fr/perso/sutre/Talks/Documents/… .
Nicolas Perrin
1
Je comprends pourquoi le problème est résolu lorsqu'il y a des actions non nulles qui se résument à zéro, mais que se passe-t-il lorsque de telles actions n'existent pas? Une partie de votre réponse a été coupée du commentaire :)
Nicolas Perrin

Réponses:

5

L'idée est basée sur une discussion que j'ai eue avec Grégoire Sutre cet après-midi.

Le problème est décidable comme suit.

Un filet de Petri est un ensemble fini de paires dans N d × N d appelées transitions. Étant donné une transition t = ( u , v ) , nous notons t la relation binaire définie sur l'ensemble des configurations N d par x ty s'il existe un vecteur zN d tel que x = u + z etTNd×Ndt=(u,v)tNdxtyzNdx=u+z . On note T la relation d'accessibilité en une étapetT t . La fermeture réflexive et transitive de cette relation est notée T .y=v+zTtTtT

Soit l'ordre partiel classique sur N d et défini par ux s'il existe zN d tel que x = u + z . La fermeture vers le haut d'un ensemble X de N d est l'ensemble X des vecteurs { vN dxXNduxzNdx=u+zXNdX. La fermeture vers le bas d'un ensembleX est l'ensembleX des vecteurs{vNdxx .{vNdxX.xv}XX.{vNdxx.vx}

Notez que si pour un ensemble fini B de N d et si T est un réseau de Petri, nous pouvons calculer un nouveau réseau de Petri T B tel que pour toutes les configurations x , y , nous avons x Ty et x , yU si, et seulement si, x T ByU=BBNdTTBx,yxTyx,yUxTByt=(u,v)bBtb=(u+z,v+z)zNd1idTU ={tbtTz(i)=max{b(i)u(i),b(i)v(i),0}1idTU={tbtTbB} satisfait à l'exigence.

Supposons maintenant que soit un réseau de Petri, l'ensemble d'obstacles. Nous introduisons l'ensemble fini . Observez que nous pouvons calculer efficacement un ensemble fini de tel que . Soit la relation binaire définie sur par if , ou s'il existe telle sorte queO D = O B N d B = N dD R N dO x R y x = y x , yN dO x TxT TOD=OBNdB=NdDRNdOxRyx=yx,yNdOxTxTByTy.

Maintenant, observez simplement que s'il existe une exécution de la configuration initiale à la configuration finale qui évite l'obstacle , alors il en existe une qui évite l'obstacle dans et qui passe par des configurations dans au plus le cardinal de cet ensemble. Par conséquent, le problème se réduit à sélectionner des configurations distinctes non déterministes dans , corriger comme la configuration initiale , comme la dernière , et vérifiez quey O O DO c 1,,c nDO c 0x cn+1y c jRc j+1jxyOODOc1,,cnDOc0xcn+1ycjRcj+1 pour chaque . Ce dernier problème se réduit aux questions classiques d'accessibilité pour les réseaux de Petri.j

Jérôme
la source
Merci beaucoup!! Cette question me revenait périodiquement à l'esprit!
Nicolas Perrin
2
Maintenant, c'est peut-être évident, mais j'aimerais poser une question de suivi, bien sûr. Et si nous permettons à d'être l'ensemble des marquages? Dans ce cas, la même construction exacte ne fonctionne pas. Y a-t-il un argument simple qui étend le résultat? Zd
Nicolas Perrin
4

J'ai réfléchi à votre question sur les systèmes d'addition vectorielle avec des états (VASS) équivalents à VAS et j'ai trouvé cette solution. Maintenant, j'ai lu la belle réponse de Jérôme et je dois dire que ma réponse est très similaire, alors veuillez accepter sa réponse même si vous considérez la mienne comme correcte.


Idée: Il est possible de convertir un VASS en un VASS qui interdit les vecteurs plus petits ou égaux aux obstacles. Ce n'est pas exactement ce que nous voulons, car les vecteurs plus petits mais pas égaux aux obstacles peuvent être atteints. Cependant, il existe de nombreux vecteurs de ce type. Cela permet une décomposition des séries minimales en plusieurs séries finies qui sont soit une transition de soit une série équivalente de . Par conséquent, oui , le problème est décidable.V V V VVVV


Détails: Soit soit un -VASS, à savoir est un graphique marqué au fini de telle sorte que . Soit l'ensemble des obstacles. Soit et , nous écrivons chaque fois que est un courir à partir à avec chaque configuration intermédiaire . Nous dénotonsd V T Q × Z d × Q O N d tc T * X N dV=(Q,T)dVTQ×Zd×QONdπ­TXNdp(u)πXq(v)πp(u)q(v)Q×XX={y:yx for some xX} .

Soit une course minimale telle que , c'est-à-dire une course minimale qui évite les obstacles. Ensuite, par le principe du pigeonhole, peut être factorisé comme une course qui n'entre que plusieurs fois de façon finie. Plus formellement, il existe , et tel queπp(u)πNdOq(v)πOOt1,t1,tn+1,tn+1T{ε}π1,,πn+1T{pi(ui),qi(vi),ri(wi)}i[0,n+1]Q×Nd

  • π=t1π1t1tn+1πn+1tn+1 ,
  • i[0,n] pi(ui)ti+1Ndqi+1(vi+1)πi+1NdOri+1(wi+1)ti+1Ndpi+1(ui+1)
  • p0(u0)=p(u), pn+1(un+1)=q(v) ,
  • i[1,n] uiOO .
  • n|Q||O|.

Par conséquent, il suffit de deviner , et les configurations intermédiaires. Tester si peut être effectué en convertissant en un nouveau -VASS où chaque transition est remplacée par un gadget de transitions. Par exemple, si alors les transitions sont remplacées comme suit:nt1,t1,,tn+1,tn+1p(x)NdOq(y)VdVtT4|O|+1O={(1,5),(2,3)}Gadget VASS

Michael Blondin
la source
1
Merci!! Deux bonnes réponses en moins de 2 jours, je dois dire que cette communauté fonctionne bien :)
Nicolas Perrin