Distributed reachability analysis for protocol verification environments, Discrete Event Systems: Models and Application, vol.103, pp.40-56, 1987. ,
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. ,
Distributed LTL model checking in SPIN, Proc. 8th International SPIN workshop on Model Checking Software (SPIN'2001), vol.2057, pp.200-216, 2001. ,
Distributed state space minimization, Electronic Notes in Theoretical Computer Science, vol.80, pp.1-15, 2003. ,
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. ,
Exploiting symmetry in temporal logic model checking, Proc. 5th Int. Conf. Computer Aided Verification (CAV'93), vol.697, pp.450-462, 1993. ,
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
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
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
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. ,
A new partial order reduction algorithm for concurrent systems, Proc. Int. Conf. Hardware Description Languages and their Applications (CHDL'97), 1997. ,
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 stubborn attack on state explosion, Formal Methods in Systems Design, vol.1, issue.4, pp.297-322, 1992. ,
A theory of timed automata, Theor. Comp. Sci, vol.126, pp.183-235, 1994. ,
Partial model checking, Proc. of LICS'95, pp.398-407, 1995. ,
Nivat's processes and their synchronization, Theor. Comp. Sci, vol.281, issue.1-2, pp.31-36, 2002. ,
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. ,
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. ,
Rabbit: A tool for bdd-based verification of real-time systems, Computer-Aided Verification -CAV, vol.2725, pp.122-125 ,
, , 2003.
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
Symbolic model checking: 10 20 states and beyond. Information and Computation (Issue for LICS90 best papers, vol.98, pp.153-181, 1992. ,
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
Timing assumptions and verification of finite-state concurrent systems, Automatic Verification Methods for Finite State Systems, vol.407, pp.197-212 ,
, , 1989.
Roméo: A tool for analyzing time Petri nets, 17th International Conference on Computer Aided Verification (CAV'05), vol.3576, 2005. ,
Hierarchical Set Decision Diagrams and Automatic Saturation, LNCS, vol.5062, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-01303835
Adding Symmetry Reduction to Uppaal, First International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS'03), vol.2791, pp.46-59, 2003. ,
What good are digital clocks, Int. Coll. Automata, Languages, and Programming -ICALP, vol.623, pp.545-558 ,
, , 1992.
Better verification through symmetry, Formal Methods in System Design, vol.9, pp.41-75, 1996. ,
Compositional model checking of real time systems, CONCUR, vol.962, pp.27-41, 1995. ,
UPPAAL in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152, 1997. ,
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
A study of the recoverability of computing systems, 1974. ,
Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams, ENTCS, 1999. ,
Efficient model checking for ltl with partial order snapshots, Theor. Comput. Sci, vol.410, issue.42, pp.4180-4189, 2009. ,
Time Petri Nets State Space Reduction using Dynamic Programming, Journal of Control and Cynernetics, vol.35, issue.3, pp.721-748, 2006. ,
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods, Computer Aided Verification -CAV, vol.2725, pp.154-166, 2003. ,
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
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. ,
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. ,
Nets of active resources for distributed systems modeling, Comp. Science. Novosibirsk, pp.43-54, 2008. ,
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. ,
Petri Net Algebra. EATCS Monographs on TCS, 2001. ,
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. ,
Modular analysis of Petri nets, The Computer Journal, vol.43, issue.3, pp.224-242, 2000. ,
Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, 1994. ,
Theoretical aspects of recursive Petri nets, Proc. of ATPN'99. LNCS 1639, pp.228-247, 1999. ,
URL : https://hal.archives-ouvertes.fr/hal-01574369
A compositional partial order semantics for Petri net components, Proc. of ATPN'1997, vol.1248, pp.235-252, 1997. ,
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
Super-Dual Nets, Proc. of CS&P'2005, pp.271-280 ,
Duality of Marked Place/Transition Nets, Research Report, vol.18, 2003. ,
Nested Petri nets -a Formalism for Specification and Verification of Multi-Agent Distributed Systems. Fundamenta Informaticae, pp.195-214, 2000. ,
Forgotten Topics" of Net Theory, Proc. of ATPN'1987, pp.500-514 ,
Petri Nets as Token Objects: An Introduction to Elementary Object Nets, vol.1420, pp.1-25, 1998. ,
Cython: The best of both worlds, Computing in Science & Engineering, vol.13, issue.2, 2011. ,
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
Model checking: Algorithmic verification and debugging, 2007. ,
Dining philosophers Petri net, 1998. ,
Méthodes et outils de vérification pour les réseaux de Petri de haut niveau, 2006. ,
Syntactical colored Petri nets reductions, ATVA'05, vol.3707, 2005. ,
Search-order independent state caching. ToP-NOC III, 2010. ,
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
Memory efficient state space storage in explicit software model checking, SPIN'05, vol.3639, 2005. ,
URL : https://hal.archives-ouvertes.fr/hal-01125050
The ComBack method revisited: caching strategies and extension with delayed duplicate detection, ToPNOC III, vol.5800, pp.189-215, 2009. ,
Analyse efficace des réseaux de Petri par des techniques de compilation, 2010. ,
Proving a Petri net model-checker implementation, IBISC, 2011. ,
A BSP algorithm for the state space construction of security protocols, PDMC'10, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00669177
S-invariance in predicate/transition nets, European Workshop on Applications and Theory of Petri Nets, 1982. ,
An improved protocol reachability analysis technique. Software, Practice and Experience, vol.18, 1988. ,
,
Coloured Petri nets and the invariant-method, Theoretical Computer Science, vol.14, issue.3, 1981. ,
Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 2009. ,
Compilation de réseaux de Petri colorés, 2009. ,
State space reduction for dynamic process creation, Scientific Annals of Computer Science, vol.20, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00666663
, The LLVM compiler infrastructure
, Python bindings for LLVM
, Python for Scientists and Engineers, vol.13, 2011.
,
, SNAKES is the net algebra
Quickly prototyping Petri nets tools with SNAKES. Petri net newsletter, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-02309814
Algebras of coloured Petri nets, pp.978-981, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-02309870
, Python Software Foundation
Haskell-coloured Petri nets, IFL'99, vol.1868, 1999. ,
Efficient symbolic state-space construction for asynchronous systems, Proc. of ICATPN'00, vol.1825, pp.103-122 ,
Minimal Büchi automata for certain classes of LTL formulas, Proc. of DEPCOS'09, pp.17-24 ,
On-the-fly verification of temporal logic, Proc. of FM'99, vol.1708, pp.253-271 ,
Un point de vue symbolique sur la logique temporelle linéaire, Actes du Colloque LaCIM 2000, vol.27, pp.131-140, 2000. ,
On-the-fly emptiness checks for generalized Büchi automata, Proc. of SPIN'05, vol.3639, pp.143-158 ,
Automated recognition of stutter-invariant LTL formulas, Atlantic Electronic Journal of Mathematics, issue.1, pp.56-74, 2006. ,
SPOT: an extensible model checking library using transition-based generalized Büchi automata, Proc. of MASCOTS'04, pp.76-83 ,
Larger automata and less work for LTL model checking, Proc. of SPIN'06, vol.3925, pp.53-70 ,
Tarjan's algorithm makes on-the-fly LTL verification more efficient, Proc. of TACAS'04, vol.2988, pp.205-219 ,
From states to transitions: Improving translation of LTL formulae to Büchi automata, Proc. of FORTE'02, vol.2529, pp.308-326 ,
Stuttering-insensitive automata for on-the-fly detection of livelock properties, ) of Electronic Notes in Theoretical Computer Science, vol.66 ,
Petri nets for systems and synthetic biology, Proc. of SFM'08, vol.5016, pp.215-264 ,
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
Efficient minimization of deterministic weak ?-automata, Information Processing Letters, vol.79, issue.3, pp.105-109, 2001. ,
Alternating finite automata on ?-words, Theoretical Computer Science, vol.32, pp.321-330, 1984. ,
, , 2011.
Properties of state spaces and their applications, International Journal on Software Tools for Technology Transfer (STTT), vol.10, issue.5, pp.443-454, 2008. ,
Evaluating and optimizing thread pool strategies for RT-CORBA, Proc. of LCTES'00, pp.214-222 ,
LTL satisfiability checking, Proc. of SPIN'07, vol.4595, pp.149-167 ,
A note on on-the-fly verification algorithms, Proc. of TACAS'05, vol.3440 ,
more deterministic" vs. "smaller" Büchi automata for efficient LTL model checking, Proc. of CHARME'03, vol.2860, pp.126-140 ,
Automata and Linear Temporal Logic: Translation with Transition-based Acceptance, 2006. ,
An automata-theoretic approach to linear temporal logic, Proc. of Banff'94, vol.1043, pp.238-266 ,
, A WYSIWYG Approach for Configuring Model Layout using Model Transformations. In: DSM'10: Workshop on Domain-Specific Modeling @ Splash, 2010.
, Algebraic Petri Nets Analyzer, 2010.
Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986. ,
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
Improving the variable ordering of obdds is np-complete, IEEE Transactions on Computers, vol.45, issue.9, pp.993-1002, 1996. ,
AlPiNA: A symbolic model checker, Petri Nets '10: International Conference on Theory and Applications of Petri nets, pp.287-296, 2010. ,
A survey of static variable ordering heuristics for efficient BDD/MDD construction, 2008. ,
, PNXDD Model Checkers
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
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
, TikZ ist kein Zeichenprogramm
Petri nets: Properties, analysis and applications, Proceedings of the IEEE, vol.77, pp.541-580, 1989. ,
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
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