1. Property language
1.1. Introduction
1.2. CTL
1.2.1. definitions
1.2.2. methods
1.2.2.1. global/local
1.2.3. global model checking
1.3. LTL
1.3.1. parse and rewrite formula
1.3.2. formula to GBA
1.3.2.1. Tableau method
1.3.2.1.1. Basic (Wolper & Vardi)
1.3.2.1.2. Advanced (Vardi)
1.3.2.1.3. Advanced2 (Giannakopoulou)
1.3.2.2. Very Weak Alternating Automaton (VWAA)
1.3.3. GBA to BA
1.3.4. verification
1.3.4.1. Tarjan
1.3.4.2. Double DFS
1.4. CTL*
1.5. Optimizations
1.5.1. BDD
1.5.2. Partial Order
1.5.3. Memory mgmt
2. Design Language
2.1. Other languages
2.1.1. DEVS
2.1.2. Markov Chain
2.1.3. Automata Theory
2.2. Petri Net
2.2.1. Introduction
2.2.2. Basic PN (=PT-net)
2.2.2.1. marking
2.2.2.2. Firing
2.2.2.3. source & sink
2.2.2.4. incidence matrix
2.2.2.5. conflict, concurrency & confusion
2.2.2.6. Reduction techniques
2.2.3. Structural Properties
2.2.4. Behaviour
2.2.4.1. reachability
2.2.4.2. boundedness
2.2.4.3. coverability
2.2.4.4. liveness
2.2.5. Subclasses
2.2.5.1. Marked Graph (MG)
2.2.5.2. State Machine (SM)
2.2.5.3. Free Choice (CF)
2.2.5.4. Extended Free Choice (EFC)
2.2.5.5. Assymetric Choice (AC)
2.2.6. Extensions
2.2.6.1. Inhibitor Net
2.2.6.2. Priority net
2.2.6.3. Probabilistic
2.2.6.4. Timed PN
2.2.6.4.1. Deterministic
2.2.6.4.2. Stochastic
2.2.6.5. Coloured PN
2.2.6.5.1. Definitions
2.2.6.5.2. Behavioral Properties
2.2.6.5.3. Example
2.2.6.5.4. Applications
2.2.6.6. Modular
2.2.6.6.1. Definitions
2.2.6.6.2. Behavioral Properties
2.2.6.6.3. Example
2.2.6.6.4. Applications
2.2.6.7. Other extensions
2.2.6.7.1. Patil [1970a]: constraints
2.2.6.7.2. Noe 1971: xor-transition
2.2.6.7.3. Baer 1973: switches
2.2.6.7.4. Andrea Asperti Nadia Busi 1996: Mobile PN
2.2.6.7.5. predicate transition
2.2.6.7.6. read / equal / reset / marking-dependent arcs
2.2.7. Applications
3. Tools
3.1. Introduction
3.2. other Tools
3.2.1. PIPE
3.2.2. LoLA
3.2.3. CPN tools
3.2.4. unused tools
3.2.4.1. brandenburg uni
3.2.4.1.1. MARCIE/CHARLIE
3.2.4.1.2. snoopy
3.2.4.2. prod
3.2.4.2.1. difficult to find source: Home Page of PROD
3.2.4.3. TAPAAL
3.2.4.3.1. GUI almost exact copy of PIPE
3.2.4.4. PEP
3.2.4.4.1. problem with tcl/tk library 32-64 bit
3.2.4.5. NuSMV2
3.2.4.5.1. model checking tool, smv input language
3.2.4.6. SPIN
3.2.4.6.1. LTL model checking tool, not Petri net specific
3.2.4.7. MARIA
3.3. Use case
3.3.1. use case MoSIS
3.3.2. dining philosophers
3.3.2.1. apply to all tools
3.3.2.2. increase n to test performance
3.3.2.3. add scripts in paper
3.4. My tool
3.4.1. introduction
3.4.2. manual
3.4.2.1. screenshot and describe functionality
3.4.3. implementation
3.4.3.1. UML diagram
3.4.3.2. analysis algorithms
3.4.3.3. design choises
3.4.3.4. test methods
3.4.3.4.1. LTL verification with LoLA