This paper presents Gradient- \$\$\backslashvarPi \$\$ , a novel heuristics for finding the variable ordering of Decision Diagrams encoding the state space of Petri net systems. Gradient- \$\$\backslashvarPi \$\$ combines the structural informations of the Petri net (either the set of minimal P-semiflows or, when available, the structure of the net in terms of ``Nested Units'') with a gradient-based greedy strategy inspired by methods for matrix bandwidth reduction. The value of the proposed heuristics is assessed on a public benchmark of Petri net models, showing that Gradient- \$\$\backslashvarPi \$\$ can successfully exploit the structural information to produce good variable orderings.

Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural Units

Amparore Elvio Gilberto;Beccuti Marco;Donatelli Susanna
2017

Abstract

This paper presents Gradient- \$\$\backslashvarPi \$\$ , a novel heuristics for finding the variable ordering of Decision Diagrams encoding the state space of Petri net systems. Gradient- \$\$\backslashvarPi \$\$ combines the structural informations of the Petri net (either the set of minimal P-semiflows or, when available, the structure of the net in terms of ``Nested Units'') with a gradient-based greedy strategy inspired by methods for matrix bandwidth reduction. The value of the proposed heuristics is assessed on a public benchmark of Petri net models, showing that Gradient- \$\$\backslashvarPi \$\$ can successfully exploit the structural information to produce good variable orderings.
ATVA: 15th International Symposium on Automated Technology for Verification and Analysis
Pune, India
October 3–6, 2017
Automated Technology for Verification and Analysis
Springer International Publishing
184
200
978-3-319-68167-2
Amparore Elvio Gilberto ; Beccuti Marco ; Donatelli Susanna
File in questo prodotto:
File Dimensione Formato  
GradientP-ATVA2017.pdf

Accesso aperto

Tipo di file: PDF EDITORIALE
Dimensione 3.48 MB
Formato Adobe PDF
3.48 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2318/1663781
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact