where \(a\)  is any action in \(A\) ,
nn and vv denote two atomic propositions (which are not tt, for true, and ff, for false),
\(\wedge \)  is the operator of logical conjunction, \(\lnot \)  is logical negation and \(\otimes \)  is the operator of parallel composition of formulae.
A special formula is \(G.F\) , where \(G\)  is a formula composed of a generalization of the diamond operator of Hennessy-Milner Logic [1]} –
parametrized on two natural numbers, \(h\)  and \(k\)  –
possibly composed in parallel with a number of \(\mbox{\em nn}\)  subformulae. The intuitive meaning of the formula \(\mbox{$\langle a \rangle ^h_k$}.F\)  is that, for the current marking of size \(h\) , it is possible to do
a transition labeled \(a\) , with pre-set of size \(h\)  and post-set of size \(k\) , and then to reach a marking where \(F\)  holds.
