GAL and ITS related papers
While some of the SDD related papers below present early versions of the formalism, more recent and up to date
definitions relating to ITS and GAL should be taken from this document .pdf

(2013) A more abstract definition of the mechanisms that allow to evaluate GAL semantics symbolically (no ITS compositions)
Maximilien Colange, Souheib Baarir, Fabrice Kordon, and Yann ThierryMieg.
Towards Distributed Software ModelChecking
using Decision Diagrams.
In Proceedings of the International Conference on
Computer Aided Verification (CAV'13),
Lecture Notes in Computer Science, St Petersburg, Russia, July
2013. Springer Verlag.
[.pdf ]
DDD and SDD Definitions
 (2002) The paper that defines DDD and inductive homomorphisms:
JeanMichel Couvreur, Emmanuelle Encrenaz, Emmanuel PaviotAdet, Denis
Poitrenaud, and PierreAndre Wacrenier.
Data decision diagrams for Petri net analysis.
In Proceedings of the 23th International Conference on
Application and Theory of Petri Nets (ICATPN'02), volume 2360 of
Lecture Notes in Computer Science, pages 101120, Adelaide, Australia, June
2002. Springer Verlag.
[.pdf ]
[Presentation slides (ppt) ]
 (2005) The paper that defines SDD and how to use hierarchy in the description of a state and encode saturation (manually):
J.M. Couvreur, Y. ThierryMieg. Hierarchical Decision Diagrams to Exploit Model Structure. In 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'05), Lecture Notes in Computer Science (LNCS), Taipei, Taiwan, pp. 443457, (SpringerVerlag)
[.pdf ]
 (2005) Yann ThierryMieg’s PhD thesis where extended discussions on SDD and their inception can be found (in English):
THIERRYMIEG Yann. Techniques for ModelChecking of highlevel specifications. PhD Thesis. 2004
[.ps.gz ]
[Presentation slides (ppt) ]
 (2008) The paper that introduces automatic saturation in DDD/SDD :
Alexandre Hamez, Yann ThierryMieg, Fabrice Kordon: Hierarchical Set Decision Diagrams and Automatic Saturation. In Petri Nets 2008: Applications and Theory of Petri Nets, 29th International
Conference, PETRI NETS 2008, Xi'an, China, June 2327, pp. 211230 (SpringerVerlag)
[.pdf ]
[Presentation slides ]
 (2009) An extended journal version of the ICATPN'08 paper, includes the definition of Instantiable Petri Nets:
Alexandre Hamez, Yann ThierryMieg, Fabrice Kordon: Building efficient ModelCheckers using Hierarchical Set Decision Diagrams and Automatic Saturation.
In Fundamenta Informatica, Special Issue selected Best papers from Petri Nets 2008, (To appear) (IOS Press)
[.pdf ]
 (2009) Introducing the Instantiable Transition System semantic framework, a general formalism that helps express systems in a way that allows efficient SDD solutions.
Yann ThierryMieg, Denis Poitrenaud, Alexandre Hamez and Fabrice Kordon: Hierarchical Set Decision Diagrams and Regular Models.
In Tools and Algorithms for the Construction and Analysis of
Systems, 15th International Conference, TACAS 2009, Held
as Part of ETAPS 2009 , York, UK, March 2229,
2009. LNCS vol. 5505, pp. 115 (Springer)
[.pdf ]
[Presentation slides (ppt) ]
 (2009) Alexandre Hamez's PhD dissertation (IN FRENCH), which contains the most current definitions of the rewriting strategies for automatic saturation.
[.pdf ]
[Presentation slides (pdf) ]
Related publications
 (2008) Using Instantiable Petri Nets to check the consistency of UML behavioral specifications (see also BCC website ):
Yann ThierryMieg, LomMessan Hillah. UML behavioral consistency checking using instantiable Petri nets. In Innovations in Systems and Software Engineering, Volume 4, Issue 3, Oct. 2008,
DOI  10.1007/s1133400800650 pp.293300 SpringerLink,
[.pdf ]
 (2008) Applying SDD to a control problem from the domain of Intelligent Transportation Systems:
Beatrice Berard, Serge Haddad, LomMessan Hillah, Fabrice Kordon and Yann ThierryMieg. Collision Avoidance in Intelligent Transport Systems: towards an Application of Control Theory.
In 9th International Workshop on discrete Event Systems (WODES'08), proceedings Goteborg, Sweden, pp. 346351, (IEEE Press)
[.pdf ]
 (2006) Using DDD to unfold a colored Petri net to a P/T net:
F. Kordon, A. Linard, E. PaviotAdet. Optimized Colored Nets Unfolding. In International Conference on Formal Methods for Networked and Distributed Systems (FORTE '06), Lecture Notes in Computer Science (LNCS), Paris, France, pp. 339355, (SpringerVerlag)
[.pdf ]
 (2006) Vincent Beaudenon’s PhD thesis where SDD are used for modelchecking of Promela specifications (in French):
BEAUDENON Vincent. Diarammes de décision de données pour la vérification de systemes matériels. PhD Thesis. 2006
[.ps ]
 (2004) Using DDD to generate an aggregated state space exploiting symmetries "à la" WellFormed Nets
Y. ThierryMieg, J.M. Ilié, D. Poitrenaud. A Symbolic Symbolic State Space Representation. In 24th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE '04) Lecture Notes in Computer Science (LNCS), Madrid, Spain, pp. 276291, (SpringerVerlag)
[.pdf ]
[Presentation slides (ppt) ]
 (2004) Using DDD to modelcheck LfP, a DSL designed for distributed systems:
F. Bréant, J.M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. PaviotAdet, D. Poitrenaud, D. Regep, G. Sutre.
Modeling and Verifying Behavioral Aspects",
In Formal Methods for Embedded Distributed Systems  How to master the complexity, Kordon Fabrice, Lemoine Michel, pp. 171211, (Kluwer Academic Publishers), (ISBN : 1402079966) [Bréant 2004]
<
