RTCP-nets (Real-Time Coloured Petri nets) are a subclass of timed coloured Petri nets (CP-nets) defined for modelling and analysis of real-time systems. In comparison to timed CP-nets, RTCP-nets use a different time model, transitions' priorities and they are forced to fulfil some structural restrictions. These characteristics of RTCP-nets enable designers direct modelling of elements typical for concurrent programming such as task priorities, timeouts, etc.

The following differences between timed CP-nets and RTCP-nets can be pointed out:

• Each transition has a priority value attached. The use of priorities allows direct modelling of deterministic choice.
• The set of arcs is defined as a relation due to the fact that multiple arcs are not allowed. Each arc has two expressions attached: a weight expression and a time expression. For any arc, each evaluation of the arc weight expression must yield a single token belonging to the type (colour) that is attached to the corresponding place; and each evaluation of the arc time expression must yield a non-negative rational value.
• The time model used by RTCP-nets differs from the one used by timed CP-nets. Each place has a local clock attached. Any positive value of the clock describes how long tokens in the corresponding place will be inaccessible for any transition. A token is accessible for a transition, if the corresponding clock value is equal to or less than zero. For example, if the clock value is equal to -3, it means the token is 3 time-units old. It is possible to specify how old a token should be so that a transition may consume it.
• Hierarchical RTCP-nets are based on hierarchical CP-nets. Substitution transitions and fusion places are used to combine pages but they are a mere designing convenience. The former idea allows the user to refine a transition and its surrounding arcs to a more complex net, which usually gives a more precise and detailed description of the activity represented by the substitution transition. In comparison with CP-nets general ports are not allowed in RTCP-nets. Moreover, each socket node must have only one port node assigned and vice versa. Thus, a hierarchical net can be easily squash to a non-hierarchical one. A fusion of places allows users to specify a set of places that should be considered as a single one. It means, that they all represent a single conceptual place, but are drawn as separate individual places (e.g. for clarity reasons). The places participating in such a fusion set may belong to several different pages. They must have the same types and initial markings. Global fusion sets only are allowed in RTCP-nets.

An RTCP-net is a tuple N = (P, T, A, Σ, V, C, G, I, E_M, E_S, M_0, S_0), where:

1. P is a non-empty finite set of places.
2. T is a non-empty finite set of transitions such that P ∩ T = ∅.
3. A ⊆ (P × T) ∪ (T × P) is a flow relation.
4. Σ is a non-empty finite set of non-empty types.
5. V is a finite set of variables such that for each variable its type belongs to Σ.
6. C is a type function, which maps each place to its type.
7. G is a guard function, which maps each transition to an expression such that each evaluation of the expression gives a Boolean value.
8. I is a priority function, which maps each transition to a non-negative integer called transition priority.
9. E_M is an arc expression function, which maps each arc to a weight expression such that each evaluation of the expression gives a value belonging to the type attached to the place.
10. E_S is an arc time expression function, which maps each arc to a time expression such that each evaluation of the expression gives a non-negative rational.
11. M_0 is an initial marking, which maps each place to a multi-set over the type attached to the place.
12. S_0 is an initial time function, which maps each place to a rational value called initial place time.

In comparison to coloured Petri nets, a priority value is attached to each transition of an RTCP-net. Moreover, a set of arcs is defined as a relation (multiple arcs are not allowed). Two expressions are attached to each arc: a weight expression and a time expression. For any arc, each evaluation of the arc weight expression must yield a single token belonging to the corresponding type; and each evaluation of the arc time expression must yield a non-negative rational value. Finally, each place has its own local clock attached that measures the place time. Any positive value of a place time describes how long tokens in the corresponding place will be inaccessible for any transition. Negatives values represent tokens age (all token in a given place share the clock value). It is possible to specify how old a token should be so that a transition may consume it.

A marking of an RTCP-net N is a function M defined on the set of places P, such that for each place p, M(p) is a multi-set over the type attached to the place.

A time function is a function S defined on P, such that for each place p, S(p) is a rational value.

A state is a pair (M,S), where M is a marking and S is a time function. The initial state is the pair (M_0,S_0).

Let V(t) be the set of variables that occur in the expressions of arcs surrounding a transition t and in the guard of the transition. A binding of a transition t is a substitution b that replaces each variable of V(t) with a value of the corresponding type, such that the guard evaluates to true.

For a transition t and its binding b, G(t)_b denotes the evaluation of the guard expression in the binding b and E_M(p,t)_b and E_S(p,t)_b denote the evaluation of the weight and the time expression in the binding b, respectively.

A transition t is enabled in a state (M,S) in a binding b iff the following conditions hold:

1. For each input place p of transition t, E_M(p,t)_b ∈ M(p) and E_S(p,t)_b ≤ -S(p),
2. For each output place p of transition t, S(p) ≤ 0,
3. For any transition t' ≠ t that satisfies conditions 1 and 2, I(t') ≤ I(t) or the transition do not have a common input or output place.

If a transition t is enabled in a state (M_1,S_1) in a binding b it may fire, changing the state (M_1,S_1) to another state (M_2,S_2), such that: M_2(p) = M_1(p) - {E_M(p,t)_b} ∪ {E_M(t,p)_b}, ({E_M(x,y)_b} = ∅ if (x,y) ∉ A), and S_2(p) is equal to:

1. E_S(p,t)_b if p is an output place of t,
2. 0 if p is an input place of t, but it is not an output place of t,
3. S_1(p) otherwise.

Every time the clock goes forward, all time stamps are decreased by the same value. Let (M,S) be a state and e = (1,1,…,1) a vector with |P| entries. The state (M,S) is changed into a state (M',S') by a passage of time τ (a rational number), iff M = M' and the passage of time τ is possible, i.e., no transition is enabled in any state (M,S), such that: S = S - τ' e, for 0 ≤ τ' < τ.

For the sake of simplicity, we will assume that there is one passage of time (sometimes equal to 0) between firings of two consecutive transitions.

For more details see presented below papers on RTCP-nets.

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.

Modelling and verification process with RTCP-nets:

CPN Tools is a modelling environment for editing, simulating, and analysing coloured Petri nets. Due to syntax differences CPN tools cannot be use to simulate or verify RTCP-nets. However, the industrial-strength modelling environment can be used for constructing RTCP-net models, which can be later processed with the RTCP-net Compiler. The following editing rule must be obeyed while designing RTCP-nets:

1. A place initial state is written marking@clock_value.
2. The notation for multisets is m_1(e_1) + m_2(e_2) + …, where m stands for multiplicity and e stands for element. The multiplicity equal to 1 and the corresponding brackets can be omitted.
3. Expressions for single direction arcs are written weight_expression@time_expression.
4. Expressions for double direction arcs are written input_weight_exp@input_time_exp | output_weight_exp@output_time_exp, where arcs are consider input or output from the places point of view.
5. Time expressions equal to 0 are omitted.

cpn2rtcpn is a small application enabling RTCP-nets modelling in CPN Tools environment. It translates CPN files into RTCPN models. cpn2rtcpn is integrated into PetriNet2ModelChecker tool. Thus, users can import RTCP-net modelled with CPN Tools, generate its coverability graph and translate it into nuXmv or Aldebaran format for formal verification using a single and intuitive application. The original version of cpn2rtcpn has been developed by Joanna Woźniak.

RTCPNC (Real-Time Coloured Petri Net Compiler) is a compiler for RTCP-nets. It is a simple command line application that takes an RTCP-net model and generates its executable version (a Java project). RTCPNC is integrated into PetriNet2ModelChecker tool which facilitates usage of the compiler by providing intuitive graphical user interface. The original version of rtcpnc has been developed by Przemysław Kowalski.

The latest version of the compiler can be downloaded from the Software page.

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 cpn2rtcpn and RTCPNC software and allows to load RTCP nets modelled in CPN Tools and generate their coverability graphs or simulators.

The tool has been tested against reachability graphs of different sizes and complexity and proved to be quite swift and efficient. Moreover, the integrated algorithms of translation for low and high level Petri nets can be adapt to other classes of Petri nets.

The latest version of the tool can be downloaded from the Software page.

PetriNet2ModelChecker manual can be found here: Online PetriNet2ModelChecker Manual.

@Article{Szp:RTCPnets:FI:06,
author = {Szpyrka, M.},
title = {Analysis of {RTCP}-nets with Reachability Graphs},
journal = {Fundamenta Informaticae},
year = {2006},
volume = {74},
number = {2--3},
pages = {375--390}
}

@Article{Szp:VMEbus:RTS:07,
author = {Szpyrka, M.},
title = {Analysis of {VME-Bus} communication protocol -- {RTCP}-net approach},
journal = {Real-Time Systems},
year = {2007},
volume = {35},
number = {1},
pages = {91-108}
}

@InCollection{SzpSzm:LNCS:06,
author = {Szpyrka, M. and Szmuc, T.},
title = {Verification of Automatic Train Protection Systems with {RTCP}-nets},
editor = {Górski, J.},
booktitle = {Computer Safety, Reliability and Security},
year = {2006},
pages = {344-357},
publisher = {Springer-Verlag},
volume = {4166},
series = {LNCS}
}