Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revision | Both sides next revision | ||
| pn2mc:introduction [2014/11/14 19:37] jbiernacki | pn2mc:introduction [2021/09/23 08:51] (current) | ||
|---|---|---|---|
| Line 6: | Line 6: | ||
| As a result, the tool provides for the automatic model checking of nets created in the TINA and CPN Tools environments. The presented solution provides the possibility of formal verification of Petri nets designed with these environments using model checking techniques and mainstream model checkers - nuXmv for LTL and CTL temporal logics, CADP Evaluator for regular alternation-free mu-calculus. | As a result, the tool provides for the automatic model checking of nets created in the TINA and CPN Tools environments. The presented solution provides the possibility of formal verification of Petri nets designed with these environments using model checking techniques and mainstream model checkers - nuXmv for LTL and CTL temporal logics, CADP Evaluator for regular alternation-free mu-calculus. | ||
| - | PetriNet2ModelChecker integrates [[rtcp_start?&# | + | PetriNet2ModelChecker integrates [[:rtcp_start?&# |
| **[[: | **[[: | ||