S. Aggarwal, R. Alonso, and C. Courcoubetis, Distributed reachability analysis for protocol verification environments, Discrete Event Systems: Models and Application, vol.103, pp.40-56, 1987.

K. Ajami, S. Haddad, and J. Ilié, Exploiting symmetry in linear temporal model checking: One step beyond, Proc. 4th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), vol.1384, pp.52-67, 1998.

J. Barnat, L. Brim, and J. Strîbrnà, Distributed LTL model checking in SPIN, Proc. 8th International SPIN workshop on Model Checking Software (SPIN'2001), vol.2057, pp.200-216, 2001.

S. Blom and S. Orzan, Distributed state space minimization, Electronic Notes in Theoretical Computer Science, vol.80, pp.1-15, 2003.

M. C. Boukala and L. Petrucci, Towards distributed verification of Petri nets properties, Proc. 1st International Workshop on Verification and Evaluation of Computer and Communication Systems (VECOS'07), pp.15-26, 2007.

E. M. Clarke, T. Filkorn, and S. Jha, Exploiting symmetry in temporal logic model checking, Proc. 5th Int. Conf. Computer Aided Verification (CAV'93), vol.697, pp.450-462, 1993.

H. Garavel, R. Mateescu, and I. Smarandache, Parallel state space construction for model-checking, Proc. 8th International SPIN workshop on Model Checking Software (SPIN'2001), vol.2057, pp.217-234, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00072247

L. Kristensen and L. Petrucci, An approach to distributed state exploration for coloured Petri nets, Proc. 25th Int. Application and Theory of Petri Nets, vol.3099, pp.474-483, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00003392

C. Lakos and L. Petrucci, Modular analysis of systems composed of semiautonomous subsystems, Proc. 4th Int. Conf. on Application of Concurrency to System Design (ACSD'2004), pp.185-194, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00003393

F. Lerda and R. Sisto, Distributed-memory model checking with SPIN, Proc. 5th and 6th International SPIN workshops on Model Checking Software (SPIN'1999), vol.1680, pp.22-39, 1999.

R. Nalumasu and G. Gopalakrishnan, A new partial order reduction algorithm for concurrent systems, Proc. Int. Conf. Hardware Description Languages and their Applications (CHDL'97), 1997.

K. Schmidt, Automated generation of a progress measure for the sweep-line method, Proc. 10th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), vol.2988, pp.192-204, 2004.

A. Valmari, A stubborn attack on state explosion, Formal Methods in Systems Design, vol.1, issue.4, pp.297-322, 1992.

R. Alur and D. L. Dill, A theory of timed automata, Theor. Comp. Sci, vol.126, pp.183-235, 1994.

H. R. Andersen, Partial model checking, Proc. of LICS'95, pp.398-407, 1995.

A. Arnold, Nivat's processes and their synchronization, Theor. Comp. Sci, vol.281, issue.1-2, pp.31-36, 2002.

B. Berthomieu, P. Ribet, and F. Vernadat, The tool tina -construction of abstract state spaces for petri nets and time petri nets, International Journal of Production Research, vol.42, issue.4, 2004.

B. Berthomieu and F. Vernadat, State class constructions for branching analysis of time petri nets, Tools and Algorithms for the Construction and Analysis of Systems -TACAS, vol.2619, pp.442-457, 2003.

D. Beyer, C. Lewerentz, and A. Noack, Rabbit: A tool for bdd-based verification of real-time systems, Computer-Aided Verification -CAV, vol.2725, pp.122-125

. Springer, , 2003.

M. Bozga, O. Maler, A. Pnueli, and S. Yovine, Some progress in the symbolic verification of timed automata, Computer Aided Verification -CAV, pp.179-190, 1997.
URL : https://hal.archives-ouvertes.fr/hal-00374086

J. Burch, E. Clarke, and K. Mcmillan, Symbolic model checking: 10 20 states and beyond. Information and Computation (Issue for LICS90 best papers, vol.98, pp.153-181, 1992.

J. Couvreur and Y. Thierry-mieg, Hierarchical Decision Diagrams to Exploit Model Structure, Formal Techniques for Networked and Distributed Systems -FORTE, vol.3731, pp.443-457, 2005.
URL : https://hal.archives-ouvertes.fr/hal-01488360

D. L. Dill, Timing assumptions and verification of finite-state concurrent systems, Automatic Verification Methods for Finite State Systems, vol.407, pp.197-212

. Springer, , 1989.

G. Gardey, D. Lime, M. Magnin, and O. H. Roux, Roméo: A tool for analyzing time Petri nets, 17th International Conference on Computer Aided Verification (CAV'05), vol.3576, 2005.

A. Hamez, Y. Thierry-mieg, and F. Kordon, Hierarchical Set Decision Diagrams and Automatic Saturation, LNCS, vol.5062, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01303835

M. Hendriks, G. Behrmann, K. G. Larsen, P. Niebert, and F. W. Vaandrager, Adding Symmetry Reduction to Uppaal, First International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS'03), vol.2791, pp.46-59, 2003.

T. A. Henzinger, Z. Manna, and A. Pnueli, What good are digital clocks, Int. Coll. Automata, Languages, and Programming -ICALP, vol.623, pp.545-558

. Springer, , 1992.

C. N. Ip and D. L. Dill, Better verification through symmetry, Formal Methods in System Design, vol.9, pp.41-75, 1996.

F. Laroussinie and K. G. Larsen, Compositional model checking of real time systems, CONCUR, vol.962, pp.27-41, 1995.

K. G. Larsen, P. Pettersson, and W. Yi, UPPAAL in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152, 1997.

M. Magnin, D. Lime, and O. H. Roux, Symbolic state space of Stopwatch Petri nets with discrete-time semantics, LNCS, vol.5062, pp.307-326, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00523612

P. M. Merlin, A study of the recoverability of computing systems, 1974.

J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard, Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams, ENTCS, 1999.

P. Niebert and D. Peled, Efficient model checking for ltl with partial order snapshots, Theor. Comput. Sci, vol.410, issue.42, pp.4180-4189, 2009.

L. Popova, Time Petri Nets State Space Reduction using Dynamic Programming, Journal of Control and Cynernetics, vol.35, issue.3, pp.721-748, 2006.

S. A. Seshia and R. E. Bryant, Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods, Computer Aided Verification -CAV, vol.2725, pp.154-166, 2003.

Y. Thierry-mieg, D. Poitrenaud, A. Hamez, and F. Kordon, Hierarchical set decision diagrams and regular models, Tools and Algorithms for the Construction and Analysis of Systems -TACAS, vol.5505, pp.1-15, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01294397

F. Wang, Efficient verification of timed automata with BDD-like structures, Int. Journal on Soft. Tools for Technology Transfer, vol.6, issue.1, pp.77-97, 2004.

S. Yovine, Kronos: A verification tool for real-time systems, International Journal of Software Tools for Technology Transfer, vol.1, issue.1-2, pp.123-133, 1997.

V. A. Bashkin, Nets of active resources for distributed systems modeling, Comp. Science. Novosibirsk, pp.43-54, 2008.

V. A. Bashkin, Formalization of semantics of systems with unreliable agents by means of nets of active resources, Programming and Computer Software, vol.36, issue.4, pp.187-196, 2010.

E. Best, R. Devillers, and M. Koutny, Petri Net Algebra. EATCS Monographs on TCS, 2001.

E. Best, W. Fraczak, R. P. Hopkins, H. Klaudel, and E. Pelz, M-nets: an algebra of high level Petri nets, with an application to the semantics of concurrent programming languages, Acta Inf, vol.35, pp.813-857, 1998.

S. Christensen and L. Petrucci, Modular analysis of Petri nets, The Computer Journal, vol.43, issue.3, pp.224-242, 2000.

K. Jensen, Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, 1994.

S. Haddad and D. Poitrenand, Theoretical aspects of recursive Petri nets, Proc. of ATPN'99. LNCS 1639, pp.228-247, 1999.
URL : https://hal.archives-ouvertes.fr/hal-01574369

E. Kindler, A compositional partial order semantics for Petri net components, Proc. of ATPN'1997, vol.1248, pp.235-252, 1997.

K. Klai, S. Haddad, and J. Ilié, Modular Verification of Petri Nets Properties: A Structure-Based Approach, Proc. of FORTE'2005, vol.3731, pp.189-203, 2005.
URL : https://hal.archives-ouvertes.fr/hal-01416459

M. Köhler and H. Rölke, Super-Dual Nets, Proc. of CS&P'2005, pp.271-280

K. Lautenbach, Duality of Marked Place/Transition Nets, Research Report, vol.18, 2003.

I. A. Lomazova, Nested Petri nets -a Formalism for Specification and Verification of Multi-Agent Distributed Systems. Fundamenta Informaticae, pp.195-214, 2000.

C. Petri, Forgotten Topics" of Net Theory, Proc. of ATPN'1987, pp.500-514

R. Valk, Petri Nets as Token Objects: An Introduction to Elementary Object Nets, vol.1420, pp.1-25, 1998.

S. Behnel, R. Bradshaw, C. Citro, L. Dalcin, D. S. Seljebotn et al., Cython: The best of both worlds, Computing in Science & Engineering, vol.13, issue.2, 2011.

R. Bouroulet, H. Klaudel, and E. Pelz, Modelling and verification of authentication using enhanced net semantics of SPL (Security Protocol Language), ACSD'06, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00340477

E. Clarke, A. Emerson, and J. Sifakis, Model checking: Algorithmic verification and debugging, 2007.

R. Esser, Dining philosophers Petri net, 1998.

S. Evangelista, Méthodes et outils de vérification pour les réseaux de Petri de haut niveau, 2006.

S. Evangelista, S. Haddad, and J. Pradat-peyre, Syntactical colored Petri nets reductions, ATVA'05, vol.3707, 2005.

S. Evangelista and L. M. Kristensen, Search-order independent state caching. ToP-NOC III, 2010.

S. Evangelista and J. Pradat-peyre, An efficient algorithm for the enabling test of colored Petri nets, CPN'04, number 570 in DAIMI report PB. University of Arhus, 2004.
URL : https://hal.archives-ouvertes.fr/hal-01124934

S. Evangelista and J. Pradat-peyre, Memory efficient state space storage in explicit software model checking, SPIN'05, vol.3639, 2005.
URL : https://hal.archives-ouvertes.fr/hal-01125050

S. Evangelista, M. Westergaard, and L. M. Kristensen, The ComBack method revisited: caching strategies and extension with delayed duplicate detection, ToPNOC III, vol.5800, pp.189-215, 2009.

L. Fronc, Analyse efficace des réseaux de Petri par des techniques de compilation, 2010.

L. Fronc and F. Pommereau, Proving a Petri net model-checker implementation, IBISC, 2011.

F. Gava, M. Guedj, and F. Pommereau, A BSP algorithm for the state space construction of security protocols, PDMC'10, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00669177

H. J. Genrich and K. Lautenbach, S-invariance in predicate/transition nets, European Workshop on Applications and Theory of Petri Nets, 1982.

G. J. Holzmann, An improved protocol reachability analysis technique. Software, Practice and Experience, vol.18, 1988.

G. J. Holzmann and . Spin,

J. Kurt, Coloured Petri nets and the invariant-method, Theoretical Computer Science, vol.14, issue.3, 1981.

K. Jensen and L. M. Kristensen, Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 2009.

R. Jourdier, Compilation de réseaux de Petri colorés, 2009.

H. Klaudel, M. Koutny, E. Pelz, and F. Pommereau, State space reduction for dynamic process creation, Scientific Annals of Computer Science, vol.20, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00666663

C. Lattner, The LLVM compiler infrastructure

R. Mahadevan, Python bindings for LLVM

K. J. Millman and M. Aivazis, Python for Scientists and Engineers, vol.13, 2011.

C. Pajault, S. Evangelista, and . Helena,

F. Pommereau, SNAKES is the net algebra

F. Pommereau, Quickly prototyping Petri nets tools with SNAKES. Petri net newsletter, 2008.
URL : https://hal.archives-ouvertes.fr/hal-02309814

F. Pommereau, Algebras of coloured Petri nets, pp.978-981, 2010.
URL : https://hal.archives-ouvertes.fr/hal-02309870

, Python Software Foundation

C. Reinke, Haskell-coloured Petri nets, IFL'99, vol.1868, 1999.

G. Ciardo, G. Lüttgen, and R. Siminiceanu, Efficient symbolic state-space construction for asynchronous systems, Proc. of ICATPN'00, vol.1825, pp.103-122

J. Cicho?, A. Czubak, and A. Jasi?ski, Minimal Büchi automata for certain classes of LTL formulas, Proc. of DEPCOS'09, pp.17-24

J. Couvreur, On-the-fly verification of temporal logic, Proc. of FM'99, vol.1708, pp.253-271

J. Couvreur, Un point de vue symbolique sur la logique temporelle linéaire, Actes du Colloque LaCIM 2000, vol.27, pp.131-140, 2000.

J. Couvreur, A. Duret-lutz, and D. Poitrenaud, On-the-fly emptiness checks for generalized Büchi automata, Proc. of SPIN'05, vol.3639, pp.143-158

J. Dallien and W. Maccaull, Automated recognition of stutter-invariant LTL formulas, Atlantic Electronic Journal of Mathematics, issue.1, pp.56-74, 2006.

A. Duret-lutz and D. Poitrenaud, SPOT: an extensible model checking library using transition-based generalized Büchi automata, Proc. of MASCOTS'04, pp.76-83

J. Geldenhuys and H. Hansen, Larger automata and less work for LTL model checking, Proc. of SPIN'06, vol.3925, pp.53-70

J. Geldenhuys and A. Valmari, Tarjan's algorithm makes on-the-fly LTL verification more efficient, Proc. of TACAS'04, vol.2988, pp.205-219

D. Giannakopoulou and F. Lerda, From states to transitions: Improving translation of LTL formulae to Büchi automata, Proc. of FORTE'02, vol.2529, pp.308-326

H. Hansen, W. Penczek, and A. Valmari, Stuttering-insensitive automata for on-the-fly detection of livelock properties, ) of Electronic Notes in Theoretical Computer Science, vol.66

M. Heiner, D. Gilbert, and R. Donaldson, Petri nets for systems and synthetic biology, Proc. of SFM'08, vol.5016, pp.215-264

J. Hugues, Y. Thierry-mieg, F. Kordon, L. Pautet, S. Barrir et al., On the formal verification of middleware behavioral properties, of Electronic Notes in Theoretical Computer Science, vol.133, pp.139-157
URL : https://hal.archives-ouvertes.fr/hal-01520379

C. Löding, Efficient minimization of deterministic weak ?-automata, Information Processing Letters, vol.79, issue.3, pp.105-109, 2001.

S. Miyano and T. Hayashi, Alternating finite automata on ?-words, Theoretical Computer Science, vol.32, pp.321-330, 1984.

/. Move, . Lrde, and . The, , 2011.

R. Pelánek, Properties of state spaces and their applications, International Journal on Software Tools for Technology Transfer (STTT), vol.10, issue.5, pp.443-454, 2008.

I. Pyarali, M. Spivak, R. Cytron, and D. C. Schmidt, Evaluating and optimizing thread pool strategies for RT-CORBA, Proc. of LCTES'00, pp.214-222

K. Y. Rozier and M. Y. Vardi, LTL satisfiability checking, Proc. of SPIN'07, vol.4595, pp.149-167

S. Schwoon and J. Esparza, A note on on-the-fly verification algorithms, Proc. of TACAS'05, vol.3440

R. Sebastiani and S. Tonetta, more deterministic" vs. "smaller" Büchi automata for efficient LTL model checking, Proc. of CHARME'03, vol.2860, pp.126-140

H. Tauriainen, Automata and Linear Temporal Logic: Translation with Transition-based Acceptance, 2006.

M. Y. Vardi, An automata-theoretic approach to linear temporal logic, Proc. of Banff'94, vol.1043, pp.238-266

Y. Sun, J. Gray, P. Langer, M. Wimmer, and J. White, A WYSIWYG Approach for Configuring Model Layout using Model Transformations. In: DSM'10: Workshop on Domain-Specific Modeling @ Splash, 2010.

. Smv-group, Algebraic Petri Nets Analyzer, 2010.

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.

J. M. Couvreur, E. Encrenaz, E. Paviot-adet, D. Poitrenaud, and P. A. Wacrenier, Data Decision Diagrams for Petri Net analysis, ICATPN '02: 23rd International Conference on Applications and Theory of Petri Nets, pp.101-120, 2002.
URL : https://hal.archives-ouvertes.fr/hal-01544997

B. Bollig and I. Wegener, Improving the variable ordering of obdds is np-complete, IEEE Transactions on Computers, vol.45, issue.9, pp.993-1002, 1996.

D. Buchs, S. Hostettler, A. Marechal, and M. Risoldi, AlPiNA: A symbolic model checker, Petri Nets '10: International Conference on Theory and Applications of Petri nets, pp.287-296, 2010.

M. Rice and S. Kulhari, A survey of static variable ordering heuristics for efficient BDD/MDD construction, 2008.

S. Hong, E. Paviot-adet, and F. Kordon, PNXDD Model Checkers

S. Hong, F. Kordon, E. Paviot-adet, and S. Evangelista, Computing a Hierarchical Static Order for Decision Diagram-Based Representation from P/T Nets, ToPNoC: Transactions on Petri Nets and Other Models of Concurrency, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01270052

L. M. Hillah, E. Kindler, F. Kordon, L. Petrucci, and N. Trèves, A primer on the Petri Net Markup Language and ISO/IEC 15909-2, Petri Net Newsletter, vol.76, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01176321

T. Tantau and C. Feuersaenger, TikZ ist kein Zeichenprogramm

T. Murata, Petri nets: Properties, analysis and applications, Proceedings of the IEEE, vol.77, pp.541-580, 1989.

K. Barkaoui and B. Lemaire, An Effective Characterization of Minimal Deadlocks and Traps in Petri nets Based on Graph Theory, 10th Int. Conf. on Application and Theory of Petri Nets ICATPN'89, pp.1-21, 1989.
URL : https://hal.archives-ouvertes.fr/hal-01125443

J. M. Couvreur, S. Haddad, and J. F. Peyre, Computation of generative families of positive semi-flows in two types of coloured nets, International Conference on Theory and Applications of Petri Nets, 1991.
URL : https://hal.archives-ouvertes.fr/hal-01124761