This work is based on Isabelle/HOL-CSP 2.0, a shallow embedding of the failure-divergence model of denotational semantics proposed by Hoare, Roscoe and Brookes in the eighties. In several ways, HOL-CSP is actually an extension of the original setting in the sense that it admits higher-order processes and infinite alphabets. In this paper, we present a particular sub-class of CSP processes which we call Proc-Omata, a fantastic beast between processes and functional automata. For this class of processes, particular proof techniques can be applied allowing for reasoning over unbounded families of sub-processes and similar architectural compositions. We develop the basic theory of deterministic terminating and non-terminating Proc-Omata, both their relation to conventional CSP processes as well as possible transformation operations on them. As an application of Proc-Omata theory, we demonstrate the use of so-called compactification theorems that pave the way, for example, to proofs over process rings of arbitrary size.