LIP6 UPMC CNRS Move-team LIP6 UPMC CNRS Move-team Macao FrameKit CPN-AMI
LIP6 > Software > MoVe Sofware > SDD/DDD >

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 Thierry-Mieg. Towards Distributed Software Model-Checking 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:
    Jean-Michel Couvreur, Emmanuelle Encrenaz, Emmanuel Paviot-Adet, Denis Poitrenaud, and Pierre-Andre 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 101-120, 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. Thierry-Mieg. 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. 443-457, (Springer-Verlag) [.pdf ]
  • (2005) Yann Thierry-Mieg’s PhD thesis where extended discussions on SDD and their inception can be found (in English):
    THIERRY-MIEG Yann. Techniques for Model-Checking of high-level specifications. PhD Thesis. 2004 [.ps.gz ] [Presentation slides (ppt) ]
  • (2008) The paper that introduces automatic saturation in DDD/SDD : Alexandre Hamez, Yann Thierry-Mieg, 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 23-27, pp. 211-230 (Springer-Verlag) [.pdf ] [Presentation slides ]
  • (2009) An extended journal version of the ICATPN'08 paper, includes the definition of Instantiable Petri Nets: Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon: Building efficient Model-Checkers 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 Thierry-Mieg, 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 22-29, 2009. LNCS vol. 5505, pp. 1-15 (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 Thierry-Mieg, Lom-Messan 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/s11334-008-0065-0 pp.293-300 SpringerLink, [.pdf ]
  • (2008) Applying SDD to a control problem from the domain of Intelligent Transportation Systems: Beatrice Berard, Serge Haddad, Lom-Messan Hillah, Fabrice Kordon and Yann Thierry-Mieg. 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. 346-351, (IEEE Press) [.pdf ]
  • (2006) Using DDD to unfold a colored Petri net to a P/T net: F. Kordon, A. Linard, E. Paviot-Adet. 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. 339-355, (Springer-Verlag) [.pdf ]
  • (2006) Vincent Beaudenon’s PhD thesis where SDD are used for model-checking 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" Well-Formed Nets Y. Thierry-Mieg, 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. 276-291, (Springer-Verlag) [.pdf ]
    [Presentation slides (ppt) ]
  • (2004) Using DDD to model-check LfP, a DSL designed for distributed systems: F. Bréant, J.-M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot-Adet, 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. 171-211, (Kluwer Academic Publishers), (ISBN : 1-4020-7996-6) [Bréant 2004]