The modal logic NML is an extension of TML [1]}, a modal logic characterizing team bisimilarity over BPP nets, which
for the first time featured the atomic propositions vv  and nn  needed to count the size of a marking.
The main difference is the introduction of the modality \(\mbox{$\langle a \rangle ^h_k$}\) , which generalizes the modality \(\mbox{$\langle a \rangle $}\)  with the parameters \(h\)  and \(k\) ,
expressing the size of the pre-set and of the post-set, respectively, of the net transition of interest.
In turn, TML is an extension of Hennessy-Milner Logic [2]} with an operator \(\otimes \)  of parallel composition of formulae,
in the style of Caires' and Cardelli's spatial logic [3]}.
Despite its apparent complexity, NML is rather simple and intuitive, as its operators have a natural operational interpretation on the net model.
Many other truly concurrent modal logics have been proposed for other truly concurrent behavioral equivalences
(see, e.g., [4]}, [5]} and the references therein).
