We propose a novel framework for modeling cyber-physical systems (CPSs) that we call Generalized Synchronization Trees (GSTs). GSTs provide a rich framework for modeling systems that contain both discrete and continuous behavior in any combination, as well as enabling novel methods for analyzing such systems. GSTs were inspired by Milner's successful use of Synchronization Trees (STs) to model interconnected computing processes, and GSTs afford a means of applying those same perspectives to CPSs. In particular, STs -- and thus GSTs -- provide a very natural setting for studying bisimulation and composition. In this thesis, we study both matters from a number of different perspectives: different notions of bisimulation over GSTs are defined and their (unexpected) semantic differences are established; the relationship of GSTs to behavioral, state-based systems is demonstrated; a simple modal logic for GSTs is defined and its relationship to bisimulation is established, in particular with respect to Hennessy-Milner classes of GSTs; and finally, bisimulation is demonstrated to be a congruence for several different composition operators.

First, we contribute a novel counterexample to the semantic equivalence of two common notions of bisimulation, as they are naturally adapted to GSTs; this is in contrast to the situation for discrete processes, where these two notions of bisimulation coincide. This example -- and the definitions of bisimulation on which it is based -- thus provides crucial guiding intuition for further study.

Second, we demonstrate how GSTs may be regarded as "unrollings" of conventional state-based behavioral systems, in direct analog to the way STs may be regarded as "unrollings" of ordinary labeled transitions systems. Crucially, conditions are established under which this unrolling procedure is shown to preserve a notion of bisimulation, as it does in the discrete case.

Third, we study the relationship between bisimulation for GSTs and a generalization of Hennessy-Milner Logic (HML) that we call Generalized Hennessy-Milner Logic (GHML). In particular, we establish a relationship between maximal Hennessy-Milner classes of discrete structures and maximal Hennessy-Milner classes of GSTs; a Hennessy-Milner class is a class of models for which modal equivalence implies bisimulation equivalence, and this direction of implication is seldom studied in the context of CPSs. Moreover, we translate Linear, Time-Invariant Systems -- regarded as behavioral systems -- into GSTs, and study the relationship between these GSTs and maximal Hennessy-Milner classes.

Finally, we study the congruence properties of bisimulation with respect to several composition operators over GSTs. One such composition operator mirrors a synchronous composition operator defined over behavioral systems, so the relationship between GSTs and state-based systems leads to a natural congruence result. Another composition operator we consider is a novel generalization of the CSP parallel composition operator for discrete systems; for this operator, too, we establish that bisimulation is a congruence, although the operator itself has subtle, implicit restrictions that make this possible. We also show that discrete GSTs can capture the bisimulation semantics of HyPA, a hybrid process algebra; consequently, this is implicitly a congruence result over compositions obtained using HyPA terms for which bisimulation is a congruence.