Event
Ph.D. Dissertation Thesis Defense: James Ferlez
Wednesday, December 5, 2018
11:00 a.m.
2168 AVW Bldg.
Maria Hoo
301 405 3681
mch@umd.edu
ANNOUNCEMENT: Ph.D. Dissertation Thesis Defense
Name: James Ferlez
Date/Time: Wednesday, December 5 2018 at 11:00AM
Location: Room 2168, AVW Building
Title: Generalized Synchronization Trees
Abstract:
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.
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.
