Counting nondeterministic computations (Q2055958)

A CCS variant called \(\mathrm{CCS}^\mu\) is introduced. It uses only \(\tau\) actions, recursion, nondeterministic choice and prefix. Then special graphs called \textit{D-graphs} are defined, later used with nodes being processes and edges being transitions between them. From D-graphs their special cases \textit{C-graphs} are derived (no two nodes are equal with respect to codivergent bisimulation). The core of the paper is devoted to the study of C-graphs. Namely, the number of C-graphs of height \(n\) is derived. Similarly, for regular C-graphs the relationship between the number of C-graphs counted by graph height and the number of C-graphs counted by graph size is characterized by a set of inequalities, giving both upper an lower bounds for one in terms of the other.