We propose the notions of "density" and "connectivity" of
infinite process graphs and investigate them in the context of the wellknown
process algebras BPA and BPP. For a process graph G, the density
function in a state s maps a natural number n to the number of states of
G with distance less or equal to n from s. The connectivity of a process
graph G in a state s is a measure for how many different ways "of going
from s to infinity" exist in G.
For BPA-graphs we discuss some tentative findings about the notions
density and connectivity, and indicate how they can be used to establish
some non-definability results, stating that certain process graphs
are not BPA-graphs, and stronger, not even BPA-definable. For BPPgraphs,
which are associated with processes from the class of Basic
Parallel Processes (BPP), we prove that their densities are at most polynomial.
And we use this fact for showing that the paradigmatic process
Queue is not expressible in BPP.
|Title of host publication||CONCUR 2006 - Concurrency Theory (Proceedings 17th International Conference, Bonn, Germany, August 27-30, 2006)|
|Editors||C. Baier, H. Hermanns|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|