Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- rtcp_start [2014/11/20 21:16]
marcin
+++ rtcp_start [2021/09/23 08:51] (current)
@@ Line 71: / Line 71: @@
 Analysis of RTCP-nets may be carried out by the use of **reachability graphs**. The set of reachable states is represented as a weighted, directed graph. Each node corresponds to a unique state, consisting of a net marking and a time vector, such that the state is the result of firing of a transition. Each arc represents a change from a state (//M//_//i//,//S//_//i//) to a state (//M//_//j//,//S//_//j//) resulting from a passage of time τ ≥ 0 and the firing of a transition //t// in one of its bindings. A label of such a graph is written (//t//,//b//)/τ.
+Due to time dependencies a reachability graph for an RTCP-nets may be infinite even though the set of the net markings is finite.
+The **minimal accessibility age** of a place //p// denotes the age when tokens in the place become accessible for at least one output transition of the place (for at least one of its binding).
+The **maximal accessibility age** of a place //p// denotes the age when tokens in the place become accessible for all  output transitions of the place (considering any binding of these transitions).
+Two states of an RTCP-net are considered to cover each other iff both states have the same markings and the same level of tokens accessibility i.e. for each place //p//, //S//_1(//p//) = //S//_2(//p//) or //S//_1(//p//) and //S//_2(//p//) are equal to or less than the maximal accessibility age of //p//.
+If two states cover each other then the same transitions are enabled in both states and the same sequences of actions are  feasible from the states.
+The reachability and coverability graphs are constructed in a similar way. They differ only about the way a new node is added to the graph. For the coverability graph, after calculating a new node, we check first whether there already exists a node that covers the new one. If so, we add only a new arc that goes to the found state (if it does not already exist) and the node is omitted. Otherwise, the new state is added to the coverability graph together with the corresponding arc. The coverability graph contains only one node for each equivalence class of the coverability relation.
-FIXME
 ====== Software tools for RTCP-nets ======
@@ Line 117: / Line 122: @@
 {{ :logo.png |}}
-**PetriNet2ModelChecker** tool deals with the problem of translation of reachability graphs for place-transition, coloured and real-time coloured Petri nets into the NuXMV language and Aldebaran format.
+**PetriNet2ModelChecker** tool deals with the problem of translation of reachability graphs for place-transition, coloured and real-time coloured Petri nets into the nuXmv language and Aldebaran format.
 PetriNet2ModelChecker works with reachability graphs generated respectively by the TINA, CPN Tools and RTCPNC software. Thus, it 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. Thus, a Petri model can be verified using model checking techniques without necessity of learning any additional language for the specification of requirements.
 It also integrates [[rtcp_start?&#cpn2rtcpn|cpn2rtcpn]] and [[rtcp_start?&#rtcpnc|RTCPNC]] software and allows to load RTCP nets modelled in CPN Tools and generate their coverability graphs or simulators.