ABSTRACT Title of dissertation: GENERALIZED SYNCHRONIZATION TREES James R. Ferlez Doctor of Philosophy, 2019 Dissertation directed by: Professor Steven I. Marcus Department of Electrical and Computer Engineering and Professor W. Rance Cleaveland Department of Computer Science We propose a novel framework for modeling cyber-physical systems (CPSs) that we call Generalized Synchronization Trees (GSTs). GSTs provide a rich frame- work 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 demon- strated; 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 com- position 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 con- ventional state-based behavioral systems, in direct analog to the way STs may be regarded as ?unrollings? of ordinary labeled transitions systems. Crucially, condi- tions 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 gen- eralization 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 relation- ship between GSTs and state-based systems leads to a natural congruence result. Another composition operator we consider is a novel generalization of the CSP par- allel 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. GENERALIZED SYNCHRONIZATION TREES by James R. Ferlez Dissertation submitted to the Faculty of the Graduate School of the University of Maryland, College Park in partial fulfillment of the requirements for the degree of Doctor of Philosophy 2019 Advisory Committee: Professor Steven I. Marcus, Chair/Advisor Professor W. Rance Cleaveland, Co-Advisor Professor P.S. Krishnaprasad Professor John Baras Professor Yasser Shoukry Professor Michael C. Fu ?c Copyright by James R. Ferlez 2019 Acknowledgments I would first like to thank my advisors Steve Marcus and Rance Cleaveland for their support, both financial and otherwise, throughout the duration of my PhD. I would also like to thank Professors P.S. Krishnaprasad, John Baras, Yasser Shoukry and Michael C. Fu for agreeing to serve on my committee. I am especially grateful to Michael Fu both for our interactions across many group meetings and for offering me a quiet spot in which to write this dissertation. I also owe an additional debt of gratitude to Professor Krishnaprasad for our many inspiring conversations over the years. I would particularly like to thank Professor Andre? Tits for always taking the time to hear me out on any matter, technical or not, and for his remarkable course on optimal control, which was undoubtedly the single most formative experience in my time here. I am also indebted to Professor C. Robert Warner, not only for teaching a less-than-ideal student three semesters of analysis but also for a thoughtful bit of encouragement that has sustained me in many difficult times. I would like to thank Professor Adrian Papamarcou for mentoring me as a co-teacher of ENEE 222 and for his many kind and thoughtful comments in the time since. This dissertation would not have been possible without the support of my parents, my family and my friends. I am forever indebted to my brother Bryan, whose patience, thoughtfulness and sense of humor turned around many a lousy day for me; my brother Michael who never hesitated to lend his support many times during this process; and my brother Jonathan for his encouraging optimism and ii for helping me get away on a vacation when I needed it most. I particularly want to thank my friends, Graham Kaland (ne? Alldredge), Eduardo Arvelo and Adam Tabeling for always keeping me honest (in matters technical and not) and each for showing me an uncommon humanity at times when my depression nearly got the better of me. I also want to thank Marcos Vasconcelos both for his friendship and for helping me through a health issue. I am also indebted to Andrew Beckwith not only for his friendship but also for a small, innocuous comment that nevertheless sustained my confidence as a writer through many trying times. Finally, I would like to thank all of my other friends and colleagues at UMD for their help and support over the years: Alborz Alavian, Marie Chau, Zamira Daw, Karamatou Yacoubou Djima, Peter Fontana, David Hartman, Meiyun He, Sam Huang, Yunlong Huang, Cheng Jie, Yunchuan Li, Kun Lin, Van Sy Mai, Waseem Malik, Ion Matei, Evripidis Paraskevas, L.A. Prashanth, Huashuai Qu, Bhaskar Ramasubramanian, Christoph Schulze, Guowei Sun, Yongqiang Wang, and David Ward (I apologize in advance to anyone I may have missed!). Finally, I am immensely grateful to the staff in both ECE and ISR who have repeatedly gone out of their way to help me along in my graduate studies. I am particularly indebted to Melanie Prange, who has patiently helped me literally from the time I arrived at UMD until just yesterday. I also want to thank Beverly Dennis, Vivian Lu, Carla Scarbor and Robert McMullen, each of whom has made a special effort on my behalf; I am truly grateful. iii Table of Contents 1 Introduction 1 1.1 Cyber-Physical Systems (CPSs) . . . . . . . . . . . . . . . . . . . . . 1 1.2 Traditional Cyber-Physical System Models . . . . . . . . . . . . . . . 2 1.2.1 Discrete, Labeled-Transition-like CPS Models . . . . . . . . . 3 1.2.2 Continuous-Like Synchronous-Composition Models . . . . . . 5 1.2.3 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3 A New CPS Modeling Framework: Generalized Synchronization Trees 7 1.4 Outline of Contributions . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4.1 System Equivalence for GSTs (Bisimulation) . . . . . . . . . . 9 1.4.2 GST Representations of Existing CPS Models . . . . . . . . . 9 1.4.3 Modal Logic and Bisimulation for GSTs . . . . . . . . . . . . 10 1.4.4 Asynchronous Composition of GSTs (CSP-Parallel Composi- tion) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2 Background 12 2.1 Process Algebra and Synchronization Trees: an Algebraic, Composi- tional Theory for Discrete Systems . . . . . . . . . . . . . . . . . . . 12 2.2 Behavioral Description of Dynamical Systems . . . . . . . . . . . . . 16 2.2.1 Behavioral Dynamical Systems: Definitions . . . . . . . . . . . 16 2.2.2 State Maps and a Notion of Bisimulation for Behavioral Dy- namical Systems . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3 Modal Logic and (Maximal) VHHM Classes of KSs . . . . . . . . . . 22 2.4 Hybrid Process Algebra (HyPA) . . . . . . . . . . . . . . . . . . . . . 26 2.4.1 HyPA Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.4.2 HyPA Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.4.3 Bisimulation for HyPA . . . . . . . . . . . . . . . . . . . . . . 35 3 Generalized Synchronization Trees 37 3.1 Generalized Synchronization Trees . . . . . . . . . . . . . . . . . . . . 37 3.1.1 Generalizing Trees . . . . . . . . . . . . . . . . . . . . . . . . 37 3.1.2 Generalized Synchronization Trees . . . . . . . . . . . . . . . 39 3.2 Bisimulation for GSTs . . . . . . . . . . . . . . . . . . . . . . . . . . 41 iv 3.2.1 Notions of Bisimulation for GSTs . . . . . . . . . . . . . . . . 41 3.2.2 Relating Strong and Weak Simulations . . . . . . . . . . . . . 44 4 Generalized Synchronization Trees and State Systems 48 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.2 Behavioral Dynamical Systems as GSTs . . . . . . . . . . . . . . . . 49 4.3 Comparison of Bisimulation Relations for Behavioral Dynamical Sys- tems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 5 GSTs and Modal Logic 60 5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 5.2 Generalized Hennessy-Milner Logic (GHML) . . . . . . . . . . . . . . 64 5.2.1 GHML for GSTs: Syntax and Semantics . . . . . . . . . . . . 64 5.2.2 VHHM Classes of GSTs . . . . . . . . . . . . . . . . . . . . . 67 5.3 Linear Time-Invariant Systems as GSTs . . . . . . . . . . . . . . . . 71 5.3.1 LTI Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 5.3.2 LTI Systems as GSTs . . . . . . . . . . . . . . . . . . . . . . . 73 5.3.2.1 Admissible Input Functions . . . . . . . . . . . . . . 73 5.3.2.2 Construction of the GSTs . . . . . . . . . . . . . . . 79 5.4 LTI Systems and Order-Equivalence Semantics . . . . . . . . . . . . . 82 5.4.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 5.4.2 LTI Systems and Order-Equivalence Non-determinism: Purely Analytic Inputs and ?Local? Non-determinism Structure . . . 86 5.4.3 LTI Systems and Order-equivalence Non-determinism: Piece- wise Analytic Inputs and ?Global? Non-determinism Structure 106 5.5 Modal Logic and Order-equivalence Induced Nondeterminism . . . . . 111 5.5.1 The Structure of Nondeterminism in LTI-derived Surrogate KSs112 5.5.2 Quasi-discreteness and VHHM Classes for Weak Dense, Tran- sitive, Right-linear Structures . . . . . . . . . . . . . . . . . . 118 5.5.3 Implications for LTI Systems . . . . . . . . . . . . . . . . . . 134 6 Congruence Results 142 6.1 Synchronous Interconnection of GSTs Derived from Behavioral Systems142 6.2 CSP-type Parallel Composition . . . . . . . . . . . . . . . . . . . . . 145 6.2.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 6.2.2 Congruence and Weak Bisimulation . . . . . . . . . . . . . . . 146 6.2.3 Congruence and Strong Bisimulation . . . . . . . . . . . . . . 151 6.2.4 Anomalies in CSP-Parallel Composition for GSTs . . . . . . . 154 6.3 A Process Algebra for Hybrid Systems: HyPA . . . . . . . . . . . . . 159 7 Conclusions and Future Research 165 7.1 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165 7.2 Future Research . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167 Bibliography 169 v Chapter 1: Introduction 1.1 Cyber-Physical Systems (CPSs) The ever-increasing complexity of real-world cyber-physical systems (CPSs) has revealed the inadequacy of traditional design and analysis techniques: neither design techniques from the physical domain (control theory) nor those from the cyber domain (computer science) have been proven to be sufficiently broad and scalable to address modern, real-world CPSs. This is a critical situation, as human safety and well-being increasingly depend on the bug-free design of CPSs. In fact, the failures of modern CPSs are increasingly expensive and newsworthy: for example, Toyota recently recalled nearly 700,000 Prius vehicles to fix a software bug that could cause the hybrid system to ?shutdown while the vehicle is being driven, resulting in a loss of power.? [1] The gulf between traditional design methodologies and modern CPSs is widen- ing largely due to the desire for increased automation both across devices and within them. The number of control laws running simultaneously in real-world devices has been increasing steadily, and those controllers are increasingly tied together by in- expensive wired/wireless networks in addition to the dynamics of the device itself. The automotive industry is one notable example of this trend. The first automo- 1 bile to contain a microcontroller was released in 1977, and it employed a single microcontroller to adjust ignition timing [2]. By contrast, a modern luxury car typ- ically contains in excess of 100 microcontrollers, most of which are interconnected by various networking features in addition to the dynamics of the car itself [2]. The proliferation and interconnectedness of such controllers has exposed the limitations of the traditional design approach where individual subsystems are designed inde- pendently and then subsequently integrated with limited analytical evaluation of the complete system. The complexity of modern CPSs is such that this design strategy increasingly leads to unanticipated emergent behavior, either through software bugs or unanticipated interactions between the control laws themselves. The research in this dissertation is an effort to address deficiency. In particular, we take the point of view that the main impediment to safe, robust CPS design is a dearth of expressive yet composable CPS models. Thus, our approach is to propose a new CPS modeling framework that facilitates the accommodation of composability ideas from the analysis of discrete time systems, specifically process algebra and synchronization trees (STs). To appreciate the value of this approach, though, it is necessary to appreciate the current state of CPS modeling. 1.2 Traditional Cyber-Physical System Models There are abundant CPS models in the literature, but virtually all of these models can be said to fit in at least one of the following categories: either the model and/or composition semantics is discrete and LTS-like, or the model treats 2 composition exclusively through synchronization. Examples of the former include HA [3] and HyPA [4], as well as [5?10]. Examples of the latter include [11, 12]. In this section, we summarize both types of models, and we conclude with a summary of the limitations thereof. 1.2.1 Discrete, Labeled-Transition-like CPS Models Hybrid Automata (HA) [3] were among the earliest system models that were endowed with enough generality to significantly intersect the modern notion of a CPS. A HA specifies the time evolution of a fixed number of continuous (state) variables just like the aforementioned state equations; however, this evolution is not governed by a fixed system of state equations, but rather by a system of state equations that changes with the evolving (discrete) state of an automaton. This automaton can (nondeterministically) make a transition whenever prescribed con- ditions on the continuous state variables are satisfied (these conditions may depend on the state of the automaton); this couples the state of the automaton to the value of the continuous state variables. Thus, HA bridge the gap between differen- tial equation models and discrete computational models, but the semantics of HA can be described by a particular LTS dubbed a timed transition system [3]. In a timed transition system, the set of locations is a subset of the (Cartesian) prod- uct of the automaton?s states and the state space of the continuous state variables: for a discrete state and a continuous state to comprise a location, the continuous states must satisfy all so-called invariant predicates associated with the discrete 3 state. Transitions from the automaton are lifted to transitions in the LTS, provided they emanate from a location that satisfies the transition condition described above. The semantics of the differential equations are captured by incorporating additional transitions. Such a transition is added between a pair of locations if and only if two conditions are met: first, both locations have a common discrete state, and second, the state equations in that discrete state admit a finite-duration solution whose initial and final states are consistent with the continuous states of the source and target locations, respectively. A solution that meets these conditions is called a witness, and each of these additional transitions is labeled with the duration of its witness. Hybrid Process Algebra (HyPA) [4] can be thought of as a process algebra that captures and extends the semantics of Hybrid Automata. As such, HyPA is a compositional algebraic framework for modeling CPSs; the signature of HyPA reflects this by including flow clauses and atomic discrete events. As in traditional process algebra, semantic derivation rules describe how transitions transform one term in the HyPA algebra into another; in HyPA, as with hybrid automata, such transitions correspond to either a discrete action or a finite-duration continuous flow (in HyPA, such transitions are labeled by a witness to the transition). However, the semantics of HyPA, like the semantics of HA, must be sensitive to the valuation of the continuous model variables, so the aforementioned derivation rules deviate from traditional process algebra in that they transform a HyPA term/valuation pair into another HyPA term/valuation pair. This connects the semantic derivation rules of HyPA to the timed transition system in the context of hybrid automata: that is 4 the derivation rules in HyPA can be used to construct a labeled transition system where each state (location) is specified by both a HyPA term and a valuation of the model variables. Though hybrid automata and HyPA do not share strictly identical semantics, this modeling choice clarifies that a HyPA process, like a hybrid automaton, can be semantically captured by a labeled transition system. 1.2.2 Continuous-Like Synchronous-Composition Models Historically, control theorists, physicists and others have regarded dynamical systems as synonymous with differential equations; often, those differential equations are a system of coupled first order differential equations, each of which specifies the first derivative of one variable. Such equations are known as state equations, and each variable that appears in differentiated form is called a state variable. For example, the dynamics of a falling body with mass m can be described in terms of the object?s height above the ground, h, and its vertical velocity, v; for convenience, we define the state variables x1 = h and x2 = v. Using Newton?s laws, we can then write a pair of differential equations in x1 and x2: that is x?1(t) = x2(t) and x?2(t) = g, where the constant g is the acceleration due to gravity near the surface of the earth. Such state equations can also be endowed with free variables that represent external influences on the state: in the previous example, we might instead write x?2(t) = g + (1/m) ? u(t) to indicate that there is a time-dependent external force u(t), which also acts on the falling body. In control theory, such a differential equation is then referred to as (a model of) the plant, and the control problem 5 is to design u(t) in such a way as to beneficially alter the dynamical properties of the state, x1 and x2. Such control problems also typically have constraints on how u(t) may be designed, such as requiring that u(t) = y(x1(t), x2(t)) for some prescribed sensor output function y. Constraints of this sort also suggest a notion of composition, namely that of input to output connection (or synchronization): in the previous example, the states x1 and x2 are fed as inputs into the function y, and the result is connected to the control input u. It is in fact the case that all traditional methods of composition for differential equations are of this type. Recently, Willems et. al. [13, 14] began advocating an alternate point of view where dynamical systems ? including hybrid systems and CPSs ? are defined com- pletely by the time trajectories of the variables involved. From this point of view, a dynamical system is defined in terms of a signal space W, which contains all possible values for the system variables. For an object in free fall (see above), we need to keep track of its height and velocity, so we might take W = R ? R. A dynamical system is also ascribed a totally ordered time set T over which the system variables evolve. The dynamics of the system are then described entirely in terms of the time trajectories of these variables or behaviors, that is functions from T?W (commonly denoted by WT). Such models encapsulate the state equation models described pre- viously, but they can also capture executions of hybrid automata, HyPA processes and other CPS-relevant hybrid frameworks. Unfortunately, composition for behav- ioral models is (to date) restricted to a generalized type of synchronization between variables, much like the input to output connections described in the context of traditional state-space models. 6 1.2.3 Limitations On the one hand, continuous-like CPS models permit rich and expressive ab- stractions of CPS models that capture true continuous behavior and choice, but this traditionally comes with the restriction of synchronous-only composition operators. On the other hand, LTS-like CPS models allow for a broad range of compositional abstractions such as asynchronous composition, but only by forgoing the ability to faithfully represent arbitrary continuous-time behavior and choice. These comple- mentary deficiencies are a serious bottleneck to compositional CPS modeling and hence, to robust, scalable CPS system design. 1.3 A New CPS Modeling Framework: Generalized Synchronization Trees In this context, the goal of this dissertation is to advance the mathematical foundations of CPS modeling by addressing these specific limitations. To this end, we have developed a novel framework that offers two important features for modeling CPSs: enough generality to encompass many different CPS models and enough compositionality to model complex CPSs in a scalable way (i.e. as a composition of smaller, more manageable systems). In other words, the objective is to develop a modeling framework that transcends the deficits of current CPS models, as they are elucidated in Section 1.2. This framework, which we have called Generalized Synchronization Trees (GSTs) 7 [15], was inspired by Milner?s use of Synchronization Trees (STs) to model inter- connected computing processes [16] (see Section 2.1 for background on STs). As such, GSTs generalize the mathematical structure of their forebears to include a wide range of non-discrete systems ? including many classes of CPSs ? while also maintaining the structural compositionality properties that make STs such effective discrete-system models. Together, these features distinguish GSTs from the exist- ing modeling frameworks in the literature, and ameliorate the limitations of those models as described in Section 1.2. This unique generality of GSTs ? both in ability to represent different CPSs and in ability to specify different types of composition ? is in some sense a consequence of the novel choice to mirror the relatively simple tree-like structures that underpin STs. Moreover, with such a simple and flexible underpinning, GSTs are also particularly well suited to studying CPS models in an abstract way: it possible not only to represent many CPSs models as GSTs, but also to imagine GSTs independent of any concrete underlying CPS model. This makes GSTs further valuable as a tool to understand what is possible in very generic dynamical systems, and hence, extremely complicated CPSs. 1.4 Outline of Contributions The core contribution of this dissertation is a new, ST-inspired CPS model in the form of GSTs: this material comprises the initial content of Chapter 3. In addition, this dissertation also contains the following contributions, each of which is identified with its location in this document. 8 1.4.1 System Equivalence for GSTs (Bisimulation) Milner [16] is credited with defining an important notion of system equivalence between discrete systems: this notion would eventually become known as bisimu- lation (see Section 2.1). However, in the context of (non-discrete) CPS models, two main notions of bisimulation developed simultaneously in the literature. It was a central contribution of [15] that these two notions are in fact different, and in general, irreconcilable. This material fills out the remainder of Chapter 3. 1.4.2 GST Representations of Existing CPS Models For GSTs to be a useful tool in the study of specific CPS models, those CPS models must be representable as GSTs in some meaningful ? and precise ? way. In fact, the same sort of reconciliation is necessary between STs and (more) general discrete models; that is a conventional discrete model, a Labeled Transition System (LTS) for example, may be ?unrolled? into a ST that is bisimilar to the original model (again, see Section 2.1). Emulating this connection, we have shown that several different CPS models can be ?unrolled? into bisimilar GSTs : in [15], such a procedure was exhibited for HyPA processes (see Section 2.4), which have essentially Hybrid Automata semantics; and in [17], Behavioral Dynamical System models [13] were likewise shown to be ?unrollable? into bisimilar GSTs. Together, these results establish the validity of GSTs as a tool for studying existing CPS models. This material is found predominantly in Chapter 4; the HyPA related material appears in Chapter 6, since it involves the inherent composition of a process algebra. 9 1.4.3 Modal Logic and Bisimulation for GSTs Hennessy and Milner noticed early on that bisimulation equivalence for a spe- cial class of STs could be characterized in terms of a very simple modal logic, known as Hennessy-Milner logic (HML) [18] (see also Section 2.3); for this reason, HML has become an important tool in the formal description and verification of discrete systems. Of course new tools for the formal description and verification of CPS models are critical, so we developed a generalization of HML for GSTs ? called Gen- eralized Hennessy-Milner Logic (GHML) [19] ? in order to study bisimulation for GSTs in terms of simple, HML-like modal formulas. Importantly, GHML can be shown to (partially) characterize maximal classes of GSTs with respect to bisimu- lation [19]: abstractly, this means that the failure of bisimulation between two such GSTs can be explained by a simple GHML ?witness? formula. However, if one of those GSTs represents a specification and the other an implementation, then such a GHML ?witness? provides a tractable explanation of why the implementation is buggy. Moreover, we have brand new work that describes the relationship between ubiquitous Linear Time-Invariant (LTI) system models and this idea of GST classes where bisimulation is captured by GHML: this is an important bridge between the abstract study of GHML as it pertains to bisimulation and the use of GHML formu- las to get useful debugging information for real CPS models. Together, this material is the subject of Chapter 5. 10 1.4.4 Asynchronous Composition of GSTs (CSP-Parallel Composi- tion) Also in [15] was a generalization of the well-known asynchronous parallel com- position operator for discrete systems (also known as CSP-parallel composition). This parallel composition takes two discrete systems and composes them asyn- chronously to form a third (discrete) system. Importantly, the parallel composition of two particular (discrete) systems will be bisimilar to the result of composing any other pair of systems that are bisimilar to original two. We have proven a simi- lar ?substitutivity? result for our GST generalization of this composition operator, although not without caveats. This is work in preparation for submission, and it appears in Chapter 6 alongside the compositional HyPA results described before. 11 Chapter 2: Background 2.1 Process Algebra and Synchronization Trees: an Algebraic, Com- positional Theory for Discrete Systems Process algebra was born in the early 1980?s out of the then nascent interest in concurrent computing. Because of this heritage, process algebra was a compositional framework from its inception: two independent computing processes can interfere with each other when run concurrently, so it is crucial to model and understand possible interactions between two such concurrently running processes. The study of such interactions motivated the seminal work of process algebra: Milner?s Calculus of Communicating Systems (CCS) [16]. The most important feature of Milner?s work was its algebraic character: the interaction ? or composition ? of two computing processes was described solely by a third computing process. Specifically, Milner semantically formalized computing processes as a set; a particular notion of interaction between two processes is then described entirely by a function that maps two elements from this set into a third. In process algebra, composition operators really are mathematically analogous to other well-known algebraic operators such as addition and multiplication over the reals. 12 Figure 2.1: A labeled transition system and its corresponding synchronization tree This feature is highly desirable in the study of composition, since such operators can be nested : that is the result of one composition may again be composed with another process using exactly the same operators, and the result of that composition may appear in yet another composition and so on. Milner?s particular formalization of computing processes as synchronization trees (STs) was itself a crucial innovation of his theory. As a model for computing processes, STs can be understood conceptually as a special type of nondeterministic labeled transition system (LTS): a ST can be thought of as a loop-free LTS where every location (node) lies on a unique path from a special node called the root. The following quotes the formal, mathematical definition given by Milner on p. 16 of [16]. ?A Synchronization Tree (ST) of sort L is a rooted, unordered, finitely branching tree each of whose arcs is labelled by a member of L? {?}.?1 Consequently, a ST contains an explicit prefix hierarchy ? formally, a partial 1 Milner also introduces the notion of rigid synchronization tree, which limit edge labels to the set L. We elide this distinction, as we do not consider ? in this thesis. 13 order ? on its nodes: each node in a ST represents a unique sequence of transitions, and the children (or successors) of a node represent extensions of this sequence. An ordinary LTS can be represented as a ST by simply tracing every one of its executions while uniquely relabeling each location every time it is visited. Conceptually, this amounts to ?unrolling? a LTS as depicted in Fig. 2.1. The advantage of this structure is that every node in a ST can be viewed as the root of another ST; thus, the semantics of the underlying LTS can be encoded by rules that transform one ST into another. These rules are called semantic derivation rules, and they can also be used to describe the semantics of certain composition operators as transformations over STs. The self-similar structure of STs also led Milner to define the concept of bisimu- lation equivalence between computational processes; this equivalence expresses pre- cisely when one ST has the same behavior as another. Specifically, two STs are bisimilar if they simulate each other: given two STs A and B, B simulates A if every possible transition from the root of A can be matched by a transition from the root of B that has the same label, and after executing these transitions, the sub-ST of A is again simulated by the sub-ST of B. Bisimulation can be specified as in the following definition, adapted from [20]; recall that if R is a binary relation on a set S ? T then R?1, the inverse of R, is binary relation on T ? S defined by R?1 , {?t, s? | ?s, t? ? R}. Definition 1 (Simulation and Bisimulation for Synchronization Trees). Let L be a set of labels, and let STL be the set of STs whose labels come from L. 14 a 1. Let T, T ? ? STL and a ? L. Then T ?? T ? if there is an edge labeled by a from the root of T to the root of T ?. a 2. Relation R ? STL?STL is a simulation if, whenever ?T1, T2? ? R and T1 ?? a T ?1, then there exists T ? 2 such that T ?? T ?2 2 and ?T ?1, T ?2? ? R. 3. Relation R ? STL?STL is a bisimulation if both R and R?1 are simulations. 4. Let T1, T2 ? STL. Then T1 is simulated by T2 (notation T1 v T2) if there is a simulation relation R with ?T1, T2? ? R. 5. Let T1, T2 ? STL. Then T1 and T2 are bisimulation equivalent, or bisimilar (notation T1 ? T2), if there is a bisimulation R with ?T1, T2? ? R. The relation v is often called the simulation preorder. It can be shown that the simulation preorder (bisimulation equivalence) itself is a simulation (bisimulation) relation, and indeed is the unique largest such relation. Note, however, that Milner?s definition was only semi-formal: other authors [21?24] subsequently developed the underlying mathematics fully through coinductive constructions. Conceptually, two bisimilar STs can certainly process the same sequences of labels, but crucially, both STs are able to process any such sequence and then extend it in the same way. Thus, bisimulation is an interactive equivalence that is stronger than language equivalence: this has ramifications specifically for system composition. For a number of interesting composition operators, this equivalence also describes precisely when one ST can be exchanged by another as an operand: Milner?s synchronous composition and Hoare?s asynchronous parallel composition 15 are notable examples. 2.2 Behavioral Description of Dynamical Systems Since we will be working extensively with behavioral systems in Chapter 4, we repeat a number of crucial definitions and results that will be necessary for regarding such systems as GSTs. 2.2.1 Behavioral Dynamical Systems: Definitions Historically, control theorists, physicists and others have regarded dynamical systems as synonymous with differential equations. Recently, however, Willems et. al. (see e.g. [14] for a summary) began advocating an alternate point of view wherein dynamical systems are defined completely by the time trajectories of the variables involved. From this point of view, a dynamical system is defined in terms of a signal space W, which contains all possible values for the system variables, and a totally ordered time set T over which those system variables evolve. The dynamics of the system are then described entirely in terms of the time trajectories of these variables or behaviors, that is functions from T?W (commonly denoted by WT). Definition 2 (Behavioral Dynamical System [14]). A dynamical system ? is a triple ? = (T,W,B) where T is a totally ordered time set and W is the space in which the system variables take their values. The set B ?WT is the set of behaviors of the system and contains all possible time evolutions of the variables in the system. We make several remarks about Definition 2. First, systems defined in this way 16 need not distinguish between input and output variables. However, we?re interested in bisimulation, which is an interactive notion, so we will often partition the signal space into input variables that take values in V and internal/output variables that take values in D; hence, W = V?D. Finally, we make the further assumption that the time set T can be embedded in a set which has an additive group structure (e.g. the integers or the reals), as in [25] where the definition of bisimulation depends on this fact in a strong way. In particular, that definition employs time-shifted behaviors: see Definition 11. Functions play a crucial role in the behavioral treatment of dynamical systems, so we introduce some convenient notation to facilitate manipulation of trajectories. With the exception of Definition 4, all of this notation comes from [25]. Definition 3 (Truncation). Given a behavior w : T ? W and a time t ? T, we define the truncation of w to t as that w| ?W{??T:??t}t such that w|t(?) = w(?) for all ? ? t. Definition 4 (Function with restricted domain). We denote a function w : {? ? T : ? ? t} ?W with the notation w|t. The additional notation in Definition 4 is meant to serve as a reminder that the values of w|t beyond t are treated as forgotten; in other words, w|t agrees with w on times up to t, but its domain cannot be expanded to get agreement with w for times later than t. Definition 5 (Concatenation). Given two behaviors w1 : T?W and w2 : T?W as well as two times t1, t2 ? T, we introduce the following notation for the function 17 obtained by gluing the suffix of w1 starting at t1 to the prefix of w2 ending at t2. That is, we define ?????w2(?) ? ? t2 w t22 ?t w1 1 := ???? .w1(? + t1 ? t2) ? > t2 Definition 6 (Projection). In the sequel, ? will denote a projection that returns a particular element of a tuple. There will be two varieties of this notation: ? when ? is specified with a natural number, ?n will return the nth element in the tuple; and ? when ? is specified with a set A, ?A will return the element of the tuple taking values in the set A. We use this form only for readability: it is meant to have an exact counterpart in the other version of this notation. 2.2.2 State Maps and a Notion of Bisimulation for Behavioral Dy- namical Systems In order to define a notion of bisimulation for behavioral dynamical systems, Julius et. al. [25] worked not with the raw trajectories, but rather with the output of a so-called state map. The reason for this will become clear subsequently. We repeat the definition below. Definition 7 (State Map [25]). A state map for a dynamical system ? = (T,W,B), is a surjective map d : B ? T? ? with the following property: 18 ? Let w1 ? B and t1 ? T. Then for all w2 ? B and t2 ? T such that d(w1, t1) = d(w2, t2), there exists a w ? 1 ? B with the property that w?1(t) = w1(t) ?t ? t1 and w?1(t) = w2(t+ t2 ? t1) ?t > t1; in other words, w ?t11 t w2 ? B.2 ? is a set associated with the state map d and that different state maps are allowed to have different codomains. ? is called the state space of the state map d; elements of ? are called states. Definition 8 (State System [25]). A state system (?, d) is a behavioral system ? = (T,W,B) along with a state map d : B ? T? ?. The general idea of Definition 7 can be summarized as follows. When a state system is in a certain state, it doesn?t matter what trajectory the system followed to get there: the legitimate future trajectories are always the same. This is also independent of when the system enters the state. In the sequel, we will need to refine the notion of a state map further in order to obtain meaningful results. Hence, we re-introduce the following two definitions from [25]. Definition 9 (Past induced state map [25]). Let ? = (T,W,B) with a state map x : B ? T? X. The state map x is past induced if for any w1, w2 ? B and t ? T, w1|t = w2|t implies that x(w1, t) = x(w2, t). Definition 10 (Markovian state map [25]). Let ? = (T,W,B) with a state map x : B ? T ? X. The state map x is Markov if for any w1, w2 ? B and t1, t2 ? T, then x(w1, t1) = x(w2, t2) and w1(? ? t2 + t1) = w2(?) ?? ? [t2, t2 + ?t] implies that x(w1, ? ? t2 + t1) = x(w2, ?) for all ? ? [t2, t2 + ?t]. 19 Now we introduce the definition of bisimulation presented in [25]. However, we take a somewhat different approach: we bootstrap that definition of bisimulation from an appropriate definition of a simulation relation. In this way, the development parallels the previous discussion of bisimulation. Definition 11 ((Bi)Simulation for Behavioral Systems with State Maps [25]). Let ?1 = (T,V?D1,B1) and ?2 = (T,V?D2,B2) be two dynamical systems which share the same external signal space V. Further suppose that each dynamical system has an associated state map xi : V?Di ? Xi. Then a binary relation x1Rx2 ? X1?X2 is a simulation relation (indicating ?2 simulates some portion of ?1) if and only if the following statement holds. ? For any (?1, ?2) ? x1Rx2, w1 := (v1, d1) ? B1, t1 ? T, w2 := (v2, d2) ? B2 and t2 ? T such that (x1(w1, t1), x2(w2, t2)) = (?1, ?2), there exists a d?2 ? ?D2B2 such that: 1. w?2 := (v2 ?t2 ?t v1, d2) ? B1 2 2. x2(w ? 2, t2) = ?2 3. d?2|t = d |2 2 t2 4. (x1(w1, ? ? t2 + t1), x (w?2 2, ?)) ? x1Rx2 ?? ? t2. If such a simulation relation x1Rx2 has the property that ??1 ? X1 there exists ?2 ? X2 such that (?1, ?2) ? x1Rx2, then we say (?2, x2) simulates (?1, x1). For such relations we will usually use the notation xvx , and write ?1xvx ?2 to indicate that ?1 is1 2 1 2 simulated by ?2. 20 A bisimulation relation is a simulation relation x1Bx2 ? X1 ?X2 for which the relation B?1x x := {??2, ?1? ? X2 ? X1 : ??1, ?2? ? x1Bx2} is also a simulation1 2 relation. (?1, x1) and (?2, x2) are then said to be bisimilar if there is a bisimulation relation x1?x2 such that (?2, x2) simulates (?1, x1) according to x1?x2 and (?1, x1) simulates (?2, x2) according to ?1 x?x .1 2 Intuitively, Definition 11 says the following about states ?1 and ?2 that are related according to x1Rx2 : whenever a behavior from ?1 passes through state ?1, any behavior in ?2 that passes through the related state ?2 ? no matter when it does so ? will have a kind of parity with the behavior from ?1. In particular, the portion of the trajectory from ?1 that comes after state ?1 can always be matched to a (possibly different) continuation of the trajectory that led to ?2 in ?2; the ?matching? is with respect to the external variables (item 3 in Definition 11) and membership of intermediate states in the relation x1Rx2 (item 4 in Definition 11). The system ?2 simulates ?1 when we have a simulation relation with the additional property that every state from ?1 is related to some state in ?2. Thus, ?2 can match the external behavior of ?1 no matter what state ?1 is in; in this sense, ?2 contains something like a ?superset? of the (external) behavior of ?1. Given this idea of what it means for one system to be a ?superset? of the external behaviors of another, it is natural to specify a relation that indicates when two systems are externally ?equivalent? to each other. This is the idea behind bisimulation. Definition 11 appears to be agnostic to the state map property of x1 and x2, however this is actually not the case. If x1 and x2 weren?t state maps, then it might 21 be possible for two states ?1 and ?2 to satisfy the properties of Definition 11 for some behaviors and times but not others. In fact, the state map property is necessary to assert that bisimulation is an equivalence relation because it assures the existence of certain trajectories; see Lemma 8 in [25]. 2.3 Modal Logic and (Maximal) VHHM Classes of KSs In this section, we describe the relevant background on HML, modal logic and (maximal) Hennessy Milner Classes. The material in this section is based largely on [26, 27]. To assist with the intelligibility of this and subsequent sections, we reintroduce notation from [19] in Table 2.1. Hennessy-Milner Logic is defined as follows, and it is interpreted with the usual semantics over STs or Kripke Structures. Note that HML lacks propositional variables, so we have the subsequent definition for an HML-like logic that does include propositional variables. Definition 12 (Hennessy-Milner Logic (HML)/Modal Logic). Given a set of labels, L, Hennessy-Milner Logic (HML) [18] is the set of formulas ?HML(L) specified s ?X t : t simulates s (w.r.t. simulation notion X) s ?X t : s and t are bisimilar (w.r.t. simulation notion X) s ?Y t : s and t satisfy the same formulas of logic Y Table 2.1: Notation for simulation, bisimulation and modal equivalence. 22 as follows, where ` ? L: ? := > | ?? | ?1 ? ?2 | ?`??. (2.1) When propositional variables are added to HML the result will be called a modal logic; the modal formulas with propositional variables ? and labels L will be denoted by ??(L). Of course in this chapter, we are primarily interested in studying the rela- tionship between modal logics like HML and bisimulation: in particular, we are interested in when modal equivalence (according to HML, say) implies bisimulation equivalence. Hence we have the following definition. Definition 13 (Visser/Hollenberg Hennessy-Milner Property [27]). Let H be a set of Kripke structures. H is said to satisfy the Visser/Hollenberg Hennessy- Milner Property (VHHM property) with respect to ??(L) if for any two Kripke structures S,T ? H and any two states s? ? S and t? ? T s? ? t? ? s? ? ?? (L) t . (2.2)? The foundation of maximal VHHM classes over KSs is the so-called canonical model [26], alternately referred to as the Henkin model in [27]. The canonical model is a special KS that is one of the most important tools in the study of (normal) modal logics. The most important feature of the canonical model is that its states (worlds) are maximally consistent sets of formulas, and the outgoing transitions from a particular state are selected in a way so as to be consistent with the formulas in that state: see the Henkin property in Theorem 1. 23 Definition 14 (Canonical (Henkin) Model [26, 27]). Let ? ? ??(L) be a normal logic. Then the canonical model is the Kripke structure C? = (S?, {R?` : ` ? L}, V ?) defined as follows: ? the set of states (worlds), S?, is the collection of maximally consistent sets of formulas with respect to the logic ?; ? for each ` ? L, the transition relation R? ?` ? S ?S? is defined such that sR`t if and only if ? ? t implies that ?`?? ? s. ? the valuation V ? : ?? S? is defined such that V (p) = {s ? S? : p ? s}. As alluded to above, the primary reason to care about the canonical model is that the constituent formulas of a state tell you something about the formulas that are true in that state. This is the so called Henkin property : that is a world in S? satisfies a modal formula if and only if that formula is an element of the world (recall that S? is a collection of sets of formulas; that is s ? S? is a maximally consistent set of formulas with respect to the logic ?). Theorem 1 (The Canonical Model Satisfies the Henkin Property [26,27]). For any state s in the canonical model C? and any formula ? ? ??(L): s |= ? ?? ? ? s (the aforementioned Henkin property). Importantly, though, the canonical model is not the unique KS over S? to satisfy the Henkin Property. Thus we refer to such models using the following terminology from [27]. 24 Definition 15 (Henkin-like model [27]). Let CK be the canonical model associated with the smallest normal logic K. Then a Henkin-like model is any Kripke struc- ture HCK = (SK , {RHK` ? RK : ` ? L}, V K` ) that satisfies the Henkin property (see Theorem 1 and the discussion preceding it). It is through such Henkin-like models that an elegant characterization of max- imal VHHM classes is possible, as reported in [27]. Theorem 2 (Maximal VHHM Classes [27]). Let HCK be any Henkin-like model, and let S(HCK) be the set of generated sub-models of HCK. Then 1. The set of all Kripke structures that are bisimilar to a model in S(HCK) is a maximal VHHM class; that is it is maximal in a set-theoretic sense. We denote such a class by BS(HCK) . 2. Let H be any set of Kripke structures that satisfies the VHHM property. Then H ? BS(HCK) for at least one Henkin-like model HCK. [19] offer the following description of the essence of Theorem 2: ?... a class of models BS(HCK) is necessarily a VHHM class because modal equivalence is a bisimulation relation over a single Henkin-like model (each maximal set of formulas is satisfied only by its own unique state in the model). Thus, Henkin-like models effectively ?canonicalize? different VHHM classes because a given Henkin-like model associates a particular transition structure with each and every (maximal) set of formulas that can be satisfied in any Kripke structure (K is sound and complete with respect to Kripke structures).? [19] 25 2.4 Hybrid Process Algebra (HyPA) Hybrid Process Algebra (HyPA) [4] is a compositional algebraic framework for modeling hybrid systems that permit instantaneous jumps in their continuous model variables; the signature of HyPA reflects this by including reinitialization operators, flow clauses and disrupt operators. As in traditional process algebra, semantic derivation rules describe how transitions transform one term in the HyPA algebra into another; in HyPA, such transitions correspond to either a discrete action or a finite-duration continuous flow. However, the semantics of HyPA must be sen- sitive to the valuation of the continuous model variables in order to be meaningful: transitions must be enabled only for certain valuations of the model variables, and transitions must also be able to alter the model variables when they execute. Thus, the aforementioned derivation rules actually transform a HyPA term, valuation pair into another HyPA term, valuation pair. This makes it possible to use the semantic derivation rules of HyPA to construct a labeled transition system where each state (location) is specified by a HyPA term and a valuation of the model variables. These labeled transition systems are coined hybrid transition systems in [4]. 2.4.1 HyPA Syntax Broadly speaking, a HyPA process (or term) is defined as a (nested) algebraic expression formed by composing HyPA operators; there are several ?atomic? pro- cesses that form the leaves of such expression trees ? that is such atomic processes can be viewed as algebraic operators with arity zero. In HyPA, an atomic process 26 is one of the following: the deadlock process, ?; the empty process, ?; an atomic (discrete) label a ? A; or a flow clause. Flow clauses are defined in terms of the valuations for ?continuous? (usually real-valued) variables: flow clauses specify dif- ferential equations that induce a ?flow? over those variables. Continuous model variables also appear in reinitialization predicates: such a predicate is defined by a reinitialization maps that ?reset? the valuation of the continuous variables. The terminology for defining flow predicates and reinitialization predicates is described below in Table 2.2. 27 Vm Model variables. V?m = {x?|x ? Vm} ?Derived? (differentiated) model variables. V?m = {x?|x ? Vm} Variables ?storing? the current value of model vari- ables. V+m = {x+|x ? Vm} Variables ?storing? the immediate future values of model variables. V(x), x ? Vm Domain of the model variable x. V = ?x?VmV(x) The union of all variable domains. V al = Vm ? V The set of all variable valuations. T { Time set; totally ordered set with a least element, 0. F = f ? (T ? V al) | The set of all flows. dom(f) = [}0, t) for some t ? T Pf Set of flow predicates (i.e. differential equations). |=f? F ? Pf Satisfaction relation for a flow predicate. The flow false satisfies no flow predicates. R = V al ? V al The set of reinitializations. Pr Reinitialization predicates. |=r? R?Pr Satisfaction relation for a reinitialization predicate. Assume true, false ? Pr. Table 2.2: Modeling notation for HyPA [4]. 28 Given these definitions, the syntax of HyPA is specified inductively accord- ing to the following table, Table 2.3. Flow and reinitialization clauses are defined explicitly in the subsequent Table 2.4. p := ? deadlock  empty process a ? A discrete action ? c = ?V |P ??f ? C flow clause (d >> p)d?D reinitialization operator (where d = [V |Pr] ? D is a reinitialization clause) p ? q alternative composition p q sequential composition p I q disrupt p . q left-disrupt p ? q parallel composition p T q left-parallel composition p | q forced-synchronization ?H(p)H?A encapsulation operators Table 2.3: HyPA syntax; p and q are arbitrary HyPA processes. [4] 29 To be precise, the flow clauses and reinitialization clauses used in Table 2.3 are defined in terms of flow and reinitialization predicates (see Table 2.2); both types of clau{ses are defi?ned specifically in}the following table, Table 2.4.? C = ? ?V |P ???f ?V ? Vm, Pf ? Pf Set of flow clauses. A flow clause is a pair in Vm ? Pf ; the specified model variables { ?? } are not allowed to jump. D = [V |Pr] ??V ? Vm, Pr ? Pr Set of reinitialization clauses. A reinitial- ization clause is a pair in Vm ? Pr; the specified model variables are the only ones that are allowed to change. Table 2.4: Flow and Reinitialization Clauses [4]. 2.4.2 HyPA Semantics The semantics of HyPA is defined in terms of hybrid transition systems [4]. Definition 16 (Hybrid Transition System [4]). A hybrid transition system is a tuple (X,A,?, 7?, ,X), consisting of a state space X, a set of action labels A, a set of flow labels ?, and transition relation 7?? X?A?X and ? (X???X). Lastly, there is a termination predicate X ? X. If the set of all HyPA processes over a set of recursive process variables Vp is given by T (Vp), then we can define the semantics of a HyPA process in terms of a specific Hybrid Transition System. 30 Definition 17 (Hybrid Transition System for a HyPA Process [4]). A Hybrid Tran- sition System for a HyPA process has constituents defined as follows: ? X = T (Vp)? V al; ? A = A? V al; ? ? = F (the set of flows; see Table 2.2). Then the transition relations 7? and and the termination operator X will be denoted by: ? ? ? 7?ax ?x?? for x, x? ? X and a ? A to signify (x, a, x?) ?7?; ? ? ?x? ?x?? for x, x? ? X and ? ? ? to signify (x, ?, x?) ? ; and ? ?x?X for x ? X to signify x ? X. The actual constituents of 7?, and X will of course be specified by the subsequent interpretation of HyPA terms. Now, it is only left to define the interpretation of flow clauses and reinitial- ization clauses before the remaining semantics of HyPA can be specified using SOS rules. Definition 18 (Solution of a Flow Clause [4]). A pair (?, ?) ? V al ? F is defined to be a solution to a flow clause c ? C, i.e. (?, ?) |= c, if: ? ? (?, ?) |= ?V |P ??f if ? |=f Pf and for all x ? V , ?(x) = ?(0)(x); and ? (?, ?) |= c ? c? if (?, ?) |= c and (?, ?) |= c?. 31 Definition 19 (Solution of a Reinitialization Clause [4]). A reinitialization (?, ? ?) ? R is defined to be a solution of a reinitialization clause d ? D, i.e. (?, ? ?) |= d, if: ? (?, ? ?) |= [V |Pr] if (?, ? ?) |=r Pr and for all x ?/ V , ?(x) = ? ?(x); ? (?, ? ?) |= d? ? d?? if (?, ? ?) |= d? or (?, ? ?) |= d??; ? (?, ? ?) |= d? ? d?? if (?, ? ?) |= d? and (?, ? ?) |= d??; ? (?, ? ?) |= d? ? d?? if there exists v ? V al with (?, v) |= d? and (v, ? ?) |= d??; ? (?, ? ?) |= d?? if ? = ? ? and there exists v ? V al with (?, v) |= d?; and ? (?, ? ?) |= cjmp if there exists ? ? ? such that (?, ?) |= c and ?(0) = ? ?. The remainder of the HyPA semantics is defined by SOS rules. For completeness, these are reproduced from [4] in Table 2.5 - Table 2.9. 32 Table 1 Operational semantics of HyPA (?, ? ) |= c, dom(? ) = [0, t] (1) a,? (2) ? (3) Tab?le1, ? ? ? a, ? ? ? ? , ? ? ? c, ? ?  ? c, ? (t) ? Operational semantics of HyPA (?, ??) |= d, ?p, ?? ? (?, ??) |=(?d, ?, )? |p=, ?c,? ?do?lm(??p) ?=, ?[??0?, t] ? , ? ?? (1)d p?, ? ? (4) a (2) (5)(3)? ?,? ? ? ? ? ? ??l ?a, ? , ? d p,c?, ? ?p? ?c,,????(?t) ? l Ta(b?l,e? ? 2).5|=: Od,pe?p, ?? ? ? ? ??? ra?tion ?al (?(S4)eman,t?ic)s|=ofdH, y?PpA, ?. R? e?pro?dpuc,t?ion? (5o)f Table 1 in [4]. Table 2 d p, ?  ? d p, ? ? ?l ?p?, ??? ? Operational semantics of HyPA, alternative and sequential composition ?p, ? ? ? lp, ? ? ? ?p?, ?? ? ?p, ? ?, ? q, ? ? ? ? ? (6) (7) (8)Tablep2 q, ? l ? ? ?p q, ? ? Op?erqatio?nalpse,m?a?ntics of HyP?Ap, a?lternqa,ti?ve?an?d seq?upent,ia?l c?omposition? ? ? ?lq p, ? ? ? ?? lp, ? ? ?p, ? ? ? ?p? p ?,?? ?? ? ?l ? ? , ? ?p, ? ?, ? q, ? ?? ? p,?? (6) p , ?? ? ?p, ? ?7 ? ? ? l ( ,) q, ?? ? q ?,???? (8)p q, ? ? ? ?(9?)l ? ? ? ? p q, ?p q, ? p , ? (10)? q?p? l lp,q?,??? ? ?p?? ? ? ? q ? q, ? ?p, ? ? ?l ? ??p? ? q, ? ? ? ? q , ? ?p , ? ?p, ? ? ?l ?p?, ?? ? ?p, ? ?, ? q, ? ? ?l ? q ?, ?? ? (9) (10) ? ? ?lp q, ? ?p? q, ?? ? ? lp q, ? ? ? ? q ?, ?? ? Table 2.6: Operational Semantics of HyPA: alternative and sequential composition. Reproduction of Table 2 in [4]. Table 3 Operational semantics of HyPA, disrupt ?p, ? ? ?p, ? ? ?l ?p?, ?? ? ?  ? (11) (12)p q, ? ? ?p  q, ? ? ? l ?p?  q, ?? ? p  q, ? ? ?p  q, ? ? ?l ?p?  q, ?? ? ? lq, ? ? ? q, ? ? ? ? q ?, ?? ? ?  ? (13) (14)p q, ? ?  ? ?lp q, ? ? q ?, ?? ? TaTbalbele24.7: Operational Semantics of HyPA: disrupt operator. Reproduction of Table Operational semantics of HyPA, parallel composition 3 in [4]. ? ?p, ? ?, ? q, ? ? ?p, ? ?  ?p?, ?? ?, ? q, ? ? ? ? q ?, ?? ? ?p ? q, ? ? (15) ? (16)?p ? q, ? ?  ?p? ? q ?, ??? | ? ?p q, ?  ? | ?p q, ? ?  ?p? ? q ?, ?? ? ?p, ? ? ? 33 a,?? ?p?, ?? ?, ? q, ? ? ?p, ? ? ? ?p?, ??? ? ? (17) (18)?p ? q, ? ?  ?p?, ?? ? ?p ? aq, ? ? ?,?? ?p? ? q, ??? ? ? ? ? ?q p, ?  ?p?, ?? ? ? ? ? a?,??q p, ? ? q ? p?, ??? ? ? | ?p q, ? ?  ?p?, ?? ? ?p ? a,??q, ? ? ? ?p? ? q, ??? ? ? q | ?p, ? ?  ?p?, ?? ? ? ? ap, ? ?,?? ?p?, ??? ? ? a?,??, q, ? ? ? ? q ?, ??? ?, a?? = a ? a? ? ? ? a??? (19) ,?? p q, ? ?p? ? q ?, ??? ? ? | a??,??p q, ? ? ? ?p? ? q ?, ??? ? Table 5 Operational semantics of HyPA, encapsulation and recursion ? a,??p, ? ? ? ?p?, ??? ?, a ? H (20) ? a,?? ( )?H (p) , ? ? ? ? ? p? , ???H ? ? ?p, ? ?  ?p?, ?? ? ?p, ? ? (21) (22) ? ? ? ( ) ? ? ? ? ? ?H (p) , ? ??H (p) , ? ?H p , ? ? lp, ? ? ? ? ? ? (23) X ? p ? ?p, ? ? ? ?p , ? ? E (24) X ? p ? E X, ? ? ? ?lX, ? ?p?, ?? ? Table 3 Operational semantics of HyPA, disrupt ?p, ? ? ?p, ? ? ?l ?p?, ?? ? ?  ? (11) (12)p q, ? ? ? ?p  l q, ? ? ? ?p?  q, ?? ? p  q, ?  ?p  lq, ? ? ? ?p?  q, ?? ? Table 3 Operation?al sema?ntics of HyPA, disr?uptq, ?  lq, ? ? ? ? q ?, ?? ? ?? ? ? (13)pp, ? q, ? ?p? l (14) p, ? ? ? l?p?, ?? ? ? ? ?  ? (11 q, ? ? ? ? q , ? ? ) (12) p q, ? l ? ? ? ? ?p  q, ? ? ? ?p  q, ? ?p  q, ?  ?p  q, ? ? ?l ?p?  q, ?? ? Table 4 Operation?alqs,em?a?ntics of HyPA, para?llqel,c?om? p?olsitio?nq ?, ?? ? ? (13) (14)? p ? q?, ? ? ? l ?p, ? , q, ? ? ?p?p,q?,??? ??p?? q ? ?, ?,? ??, ?? q, ? ?  ? q ?, ?? ? ?p ? q, ? ? (15) (16) ? | ? ?p ? q, ? ? ?  ?p? ? q ?, ?? ? p q, ?  ? | ? ?p q, ?  ?p? ? q ?, ?? ? Table 4 Operational se?mantics? of H? yPA, parallel composition?p, ? ?  ?p , ? ?, ? q, ? ? ? ? a?,??p, ? ?p?, ??? ? ? ? ?p, ?p?? q, ,??q,????p?, ?? ?? (1?7)?p, ?  ??p??, ??p q,??, ?? ? ? (18) qa,,?? ? ? ? q ?, ??? ? ? ? ? ? (15) ? ?p ? q, ? ?? (16)?p ?q, ? ? a,??? ? ??pq | qp, ???  ?p?, ?? ? ?p ? q? q, ???p, ? ??p?? q? q, ?? p?, ?  ?, ??? ? ?p | q, ? ? ? ?p?, ?? ? ?p | ?qp, ??? ? ? q, ? ??pa??,?? q??,p?? ???q, ??? ? ? ?? q? | p? , ?? ?  ?p ?, ?? ? a,?? p, ?  p?? ? a?,?,? ? ? ? ?,? ? q??,?? ?? ? a??,?? ? ??p, ? ? ? ?p ?, ??? ? ? p?, ? ? ? p , ?? ?, q, (?17) q , ??? ?, ?? ? (18)aa,?? = a p q, ?  ? ? a (1?9?) ? ? ? ? ? ?p?, ? ? a??,?? ?? p ??q, ??? ? ? ?p ? q, ? ?p q q p, ?  ?p?, ??,?? ? ? ?p ? q , ? ? a,?? ? ??? | ? a???,?? ? ???q ??p,??? ?? ? ? q ? p , ? ?? | ? ? ? p? q?,?? p? q? , ? ap q, ?  p , ? p q, ? ? ?,?? ?p? ? q, ??? ? ? q | p, ? ? ? ?p?, ?? ? TaTbalbele 25.8?: Op?era?,t?i?o?nal? Se??mantics ofa?,H?? yPA? : p??arall?e? l compo? sition. Reproduction ofOperationalps,em?antics of HpyP,A?, en?c,ap?suqla,t?ion? an?d rec?uqrsi,on? ?, a = a ? a a??,?? (19) Table 4 in [4]. ? ??pa??,?q? ,?? ?? ? ?p ? ? q ?, ??? ? p, ?? | p ,a??? ?? ,???, a ? H ? p q? ,a??,??? ?? (?p??)? q ?, ?(?2?0?)?H (p) , ? ? ??H p , ? ? Table 5 ? ?Operational sempa,n?tic?s of Hy?PpA?,,e ? ? ( ?nc? a?p)sulation and recurs?iopn, ? ?(21) ? (22)? (p) , ? ? ?H (p) , ? ? ? ? H?  ???aH?,??pp, ? ? ,p? ?, ???? ?, a ? H (20) ? a,?? ( )?H (p) , ? ? ? ? ? p? , ??? ??p, ? ? ?p, ? ?H?l ?p?, ?? ? ? ? (23) X ? p ? E (24) X ? p ? EX, ? l ? ? ? ? ? ? ??X, ? ? ? ?p ?, ?? ? p, ?  p ,(? ) ?p, ? ?? (21) ? ? (22)? ?H (p) , ? ?  ? ? ? ? ?H (p) , ??H p , ? ? lp, ? ? ?p, ? ? ? ?p?, ?? ? ? ? (23) X ? p ? E (24) X ? p ? EX, ? ? lX, ? ? ? ?p?, ?? ? Table 2.9: Operational Semantics of HyPA: encapsulation and recursion. Repro- duction of Table 5 in [4]. 34 2.4.3 Bisimulation for HyPA In the context of hybrid transition systems, the standard notion of bisimula- tion for labeled transition systems with marked states may be trivially applied; this appears as Definition 4 in [4]. However, bisimulation as such is not a congruence for HyPA processes, because the valuation of the model variables plays a funda- mental role in the semantic derivation rules of HyPA (see Table 2.5 - Table 2.9 in Section 2.4.2). This nuance has two specific facets. First, the semantics of HyPA are such that the label on a transition determines exactly the valuation of the model variables after such a transition is performed (this appears inconspicuously in Ap- pendix A of [4] as Lemma A.1). This feature of the HyPA semantics considerably prunes the reachable states in a hybrid transition system; it also forces synchrony of valuations between processes that perform the same sequence of labels, and reduces nondeterminism in the valuation of the model variables to a choice that is made be- fore a process starts performing transitions. Second, HyPA operators operate only on process terms, so non-unary operators are unable to maintain distinct trajecto- ries of the model variables for each of the subprocesses supplied as operands. This is in stark contrast to traditional processes algebra, where all of the state informa- tion is contained in an algebraic expression; in that setting, a non-unary operator effectively maintains separate state spaces for each of the subprocesses supplied as operands. These factors work in concert to break bisimulation as a congruence for HyPA: two processes which are bisimilar need only agree about behavior on their reachable states (the first point), yet the parallel composition operator allows a third 35 process to introduce new states from which the original processes can execute by influencing the common (i.e. global) model valuations (the second point). Unfortunately, it is a reasonable, even necessary, choice to require global vari- able valuations. This inflexibility suggests only one means to obtain congruence with respect to HyPA: in order to substitute a process q for a process p, a bisimulation relation must be exhibited that includes all of the subprocess, valuation pairs that are hidden by an initial choice of valuation. This is exactly the idea behind stateless bisimulation, which is indeed a congruence for HyPA [4]. This is an important con- clusion in [4], although it appears only in relation to a more complicated notion of congruence, called robust bisimulation; it is proved in [4] that robust bisimulation is equivalent to stateless bisimulation in the context of HyPA. For this reason, we confine ourselves to the consideration of stateless bisimulation. The definition of stateless bisimulation is repeated below. Definition 20 (Stateless bisimulation [4]). Given a hybrid transition system with state space T (Vp) ? Val, a stateless bisimulation relation is a binary relation R ? T (Vp)? T (Vp) such that for all ?, ? ? ? Val and pRq, ? ?p, ?? ? X implies ?q, ?? ? X, ? ?q, ?? ? X implies ?p, ?? ? X, ? ? ? ?` `p, ? ?p?, ? ?? implies ?q? ? T (V ) such that ?q, ?? ? ?q?p , ? ?? ? p?Rq? and ? ?q, ?? ?` ?q?, ? ?? implies ?p? ? T (Vp) such that ?p, ?? ?` ? ? ?? ? p , ? p?Rq?. 36 Chapter 3: Generalized Synchronization Trees 3.1 Generalized Synchronization Trees This section contains the foundational ideas on which much of the remainder of this dissertation depends: it is here that we formally define Generalized Synchro- nization Trees as a modeling structure that generalizes Milner?s Synchronization Trees. 3.1.1 Generalizing Trees This section presents basic background on partial and total orders and reviews a classical definition of tree in this setting. Definition 21 (Partial Order). Let P be a set, and let ? P ? P be a binary relation on P . Then  is a partial order on P if the following hold. 1.  is reflexive: for all p ? P, p  p. 2.  is anti-symmetric: for all p1, p2 ? P , if p1  p2 and p2  p1 then p1 = p2. 3.  is transitive: for all p1, p2, p3 ? P , if p1  p2 and p2  p3 then p1  p3. We abuse terminology and refer to ?P,? as a partial order if  is a partial order over set P . We write p1 ? p2 if p1  p2 and p1 6= p2 and p2  p1 if p1  p2. 37 We adapt the usual interval notation for numbers to partial orders as follows. [p1, p2] , {p ? P | p1  p  p2} (p1, p2) , {p ? P | p1 ? p ? p2} Half-open intervals, e.g. [p1, p2) and (p1, p2], have the obvious definitions. Definition 22 (Upper/Lower Bounds). Fix partial order ?P,? and P ? ? P . 1. p ? P is an upper (lower) bound of P ? if for every p? ? P ?, p?  p (p  p?). 2. p ? P is the least upper (greatest lower) bound of P ? if p is an upper (lower) bound of P ? and for every upper (lower) bound p? of P ?, p  p? (p?  p). When set P ? has a least upper bound (greatest lower bound) we sometimes use supP ? (inf P ?) to denote this element. Definition 23 (Total Order). Let ?P ? be a partial order. Then  is a total or linear order on P if for every p1, p2 ? P , either p1  p2 or p2  p1. If ?P,? is a partial order and P ? ? P , then we sometimes abuse notation and write ?P ?,? for the partial order obtained by restricting  to elements in P ?. We say that P ? is totally ordered by  if  is a total order for P ?. We refer to P ? as a linear subset of P in this case. Trees may now be defined as follows [28]. Definition 24 (Tree [28]). A tree is partial order ?P,? such that for each p ? P , the set {p? ? P | p? - p} is totally ordered by . If there is also a p0 ? P such that p0 - p for all p ? P , then p0 is called the root of the tree, and ?P,, p0? is said to be a rooted tree. 38 In [29], these structures are referred to as prefix orders. The distinguishing feature of a tree implies that - defines a notion of ancestry. In a rooted tree, the root is an ancestor of every node, so every node has a unique ?path? to the root. Since the subsequent development is modeled on synchronization trees, we will consider only rooted trees in the sequel. We conclude this section by discussing a notion of discreteness for trees. Definition 25 (Discrete Tree). A tree ?P,, p0? is discrete if and only if for every p, the set [p0, p] is finite. The following alternative characterization of discreteness is sometimes useful. Proposition 1. A tree ?P,, p0? is discrete if and only the following all hold. 1. For every p 6= p0, sup[p0, p) ? [p0, p). 2. For every p ? P and p?  p, inf(p, p?] ? (p, p?]. 3. Every nonempty linear subset P ? of P has a greatest lower bound. 3.1.2 Generalized Synchronization Trees The impact of Milner?s work is hard to overstate; process algebra is a major field of study in computing, and the notions of simulation and bisimulation have had a substantial influence on other areas such as control-system modeling and systems biology, where the focus is on continuous, rather than discrete, behavior. However, the rich array of composition operators, and associated elegant metatheoretical re- sults [30, 31] found in traditional process algebra have yet to emerge in these more 39 general contexts. Our motivation for generalized synchronization trees is to provide a flexible framework analogous to synchronization trees over which composition op- erations may be easily defined, and their algebraic properties studied, for this more general setting. Synchronization trees are intended to model discrete systems that evolve via the execution of atomic actions. This phenomenon is evident in the fact that trees have edges that are labeled by these actions; each node in a tree is thus at most finitely many transitions from the root. For systems that have continuous as well as discrete dynamics, synchronization trees offer a problematic foundation for system modeling, since the notion of continuous trajectory is missing. Generalized synchronization trees are intended to provide support for discrete, continuous, and hybrid notions of computation, where nondeterminism (branching) may also be discrete, continuous, or both. Definition 26 (Generalized Synchronization Tree). Let L be a set of labels. Then a generalized synchronization tree (GST) is a tuple ?P,, p0,L?, where: 1. ?P,, p0? is a tree in the sense of Definition 24; and 2. L ? P\{p0} ? L is a (possibly partial) labeling function. A GST differs from a synchronization tree in two respects. On the one hand, the tree structure is made precise by reference to Definition 24. On the other hand, labels are attached to (non-root) nodes, rather than edges; indeed, a GST may not in general have a readily identifiable notion of edge. 40 In the rest of this section we show how different classes of systems may be encoded as GSTs. These example contain different mixtures of discrete / continuous time and discrete / continuous nondeterminism (called ?choice?). 3.2 Bisimulation for GSTs Section 2.1 defined standard notions of equivalence (bisimulation) and refine- ment (simulation) on synchronization trees. The goal of this section is to study adaptations of these notions for generalized synchronization trees. In the process of doing so, we highlight a subtlety that arises because of GSTs? capability of modeling non-discrete time. As the notions of simulation and bisimulation are closely linked (see Definition 1), in what follows we focus our attention on simulation. 3.2.1 Notions of Bisimulation for GSTs Simulation relations in Definition 1 rely on a notion, labeled edges, that syn- chronization trees possess but GSTs do not. However, an intuition underlying the simulation relation is that if T1 v T2, then every ?execution step? of T1 can be matched by T2 in such a way that the resulting trees are still related. This observa- tion provides a starting point for simulations on GSTs; rather than relying on edges to define computation, use the notion trajectory instead. Definition 27 (Trajectory). Let ?P,, p0,L? be a GST, and let p ? P . Then a trajectory from p is a linear subset P ? ? P such that for all p? ? P ?: 1. p?  p and 41 2. (p, p?] ? P ?. A trajectory from a node p in a GST is a path that starts from p, but for technical reasons, does not include p. A trajectory can be bounded with a maximal element as in the case of the interval (p, p?], or it can be bounded with a least upper bound as in the case of (p, p?). It is also possible for a trajectory to be bounded without a least upper bound or even unbounded. Trajectories are analogous to computations and thus will form the basis of the simulation relations given below. In order to determine when two trajectories ?match?, we introduce the concept of order-equivalence. Definition 28 (Order Equivalence). Let ?P,P , p0,LP ? and ?Q,Q, q0,LQ? be GSTs, and Tp, Tq be trajectories from p ? P and q ? Q respectively. Then Tp and Tq are order-equivalent if there exists a bijection ? ? TP ? TQ such that: 1. p1 P p2 if and only if ?(p1) Q ?(p2) for all p1, p2 ? TP , and 2. LP (p) = LQ(?(p)) for all p ? TP . When ? has this property, we say that ? is an order equivalence from TP to TQ. Two trajectories that are order-equivalent can be seen as possessing the same ?content?, as given by the labeling functions of the trees, in the same ?order?. Note that in general, the bijections used to relate two order-equivalent trajectories need not be unique, although when the trees in question are discrete, they must be. The first notion of simulation may now be given as follows. 42 Definition 29 (Weak Simulation for GSTs). Let G1 = ?P,P , p0,LP ? and G2 = ?Q,Q, q0,LQ? be GSTs. Then R ? P ?Q is a weak simulation from G1 to G2 if, whenever ?p, q? ? R and p?  p, then there is a q?  q such that: 1. ?p?, q?? ? R, and 2. Trajectories (p, p?] and (q, q?] are order-equivalent. G1 vw G2 if there is a weak simulation R from G1 to G2 with ?p0, q0? ? R. Weak bisimulation equivalence can be defined easily. Call a weak simulation R from G1 to G2 a weak bisimulation if R ?1 is a weak simulation from G2 to G1. Then G1 ?w G2 iff there is a weak bisimulation R with ?p0, q0? ? R. Weak simulation appears to be the natural extension of simulation to GSTs: for one node to be simulated by another, each bounded trajectory from the first node must be appropriately ?matched? by an equivalent trajectory from the second node. However, one may impose a stronger condition on the trajectories emanating from related nodes, as follows. Definition 30 (Strong Simulation for GSTs). Let G1 = ?P,P , p0,LP ? and G2 = ?Q,Q, q0,LQ? be GSTs. Then R ? P ? Q is a strong simulation from G1 to G2 if, whenever ?p, q? ? R and Tp is a trajectory from p, there is a trajectory Tq from q and bijection ? ? Tp ? Tq such that: 1. ? is an order equivalence from Tp to Tq, and 2. ?p?, ?(p?)? ? R for all p? ? Tp. G1 vs G2 if there is a strong simulation R from G1 to G2 with ?p0, q0? ? R. 43 Strong simulations strengthen weak ones by requiring that matching trajecto- ries also pass through nodes that are related by the simulation relation, and by also considering potentially unbounded trajectories as well as bounded ones. 3.2.2 Relating Strong and Weak Simulations This section now considers the relationships between weak and strong simula- tion. The first result indicates that the latter is indeed stronger than the former. Theorem 3. Let G1 and G2 be GSTs with G1 vs G2. Then G1 vw G2. The proof follows from the fact that every strong simulation is a weak simu- lation. The next result, coupled with the previous one, establishes that for discrete trees, the two simulation orderings in fact coincide. Theorem 4. Suppose that G1 and G2 are discrete GSTs, and that G1 vw G2. Then G1 vs G2. The proof uses induction on transitions to show that any weak simulation is also strong. We now show that vw / vs coincides with the simulation ordering, v, given for synchronization trees (i.e. discrete, finite-branching GSTs) in Definition 1. The next definition defines a notion of ??a for discrete GSTs. Definition 31 (Transitions for Discrete GSTs). Let G = ?P,, p0,L? be a GST, with p, p? ? P . 44 1. p? is an immediate successor of p if p?  p and there exists no p?? ? P such that p?  p??  p. 2. Gdp, the subtree of G rooted at p, is ?P ?,?, p,L??, where P ? = {p? ? P | p  p?}, and ? / L? are the restrictions of  and L to P ? / P ?/{p}. 3. Let G? = ?P ?,?, p? ,L?? ??a0 be a GST. Then G G? exactly when p?0 ? P , p?0 is an immediate successor of p0, G ? = Gdp? ?0, and L(p ) = a. a Intuitively, G ?? G? if G? is an immediate subtree of G? and the root of G? labeled by a. Based on this notion, Definition 1 may now be applied to discrete GSTs. We have the following. Theorem 5. Let G1, G2 be discrete GSTs. Then the following are equivalent. 1. G1 v G2. 2. G1 vw G2. 3. G1 vs G2. One might hope that vw and vs would coincide for general GSTs, thereby obviating the need for two notions. Unfortunately, this is not the case. Theorem 6. There exist GSTs G1 and G2 such that G1 vw G2 but G1 6vs G2. Proof. Consider the GSTs depicted in Fig. 3.1. It turns out that the trees G1 and G2 are such that G1 vw G2, but G1 v6 s G2. Both G1 and G2 use a label set {?, ?}, and both are discrete except for their start states. Each tree is constructed from a basic ?time axis? T = {1/n | n ? 45 ? ? ? ? k, 1 ? ? ? k k, 1 1 ? 3 k, 2 k,1 ? ? ? ? ? k, 1 k, 1 k, 1 1k+1 k 3 k, 2 k,1 ? ? ? ? 3, 1 3, 1 ? 3 2 3,1 ? ? ? ? ? ? 3, 1 3, 1n 4 3, 1 3 3, 1 2 3,1 T3 p02 ? ? ?2, 12 2,1? ? ? ? ? ? 2, 1 1 1 1n 2, 4 2, 3 2, 2 2,1 G T2 2 ? 1,1? ? ? ? ? ? 1, 1 1 1 1n 1, 4 1, 3 1, 2 1,1 T1 ? ? ? ? ? 1 ? 1 ? 1 ? 1 ? ? n 4 3 2 1 ? ? ? ? ? p01 1 1 1 1n 4 3 2 1 S1 S2 G1 S3 Figure 3.1: Visualization of the GSTs used in proof of Theorem 6. N\{0}}?{0}, with the usual ordering ?. The start state G1 corresponds to time 0; each subsequent node is labeled by ? if there is an edge to the next time point, or ? if the node is maximal. In traditional synchronization-tree terms, each (non-start) node has an outgoing labeled ? and another labeled ?. G2 is similar to G1 except it contains an infinite number of branches from the start state, with branch k only enabling ? transitions for the last k nodes. The shading in the diagram illustrates a weak simulation that may be con- structed and used to show that the start states in G1 and G2 are indeed related by 46 1 ... ... a weak simulation. Intuitively, every trajectory from the start node of G1 leads to a node from which a finite number of ?s are possible, with a ? possible at each step also. This trajectory can be matched by one from the start state of G2 that leads to a branch from which enough ?-less nodes can be bypassed. On the other hand, no strong simulation can be constructed relating the start node of G1 with G2. The basic intuition is that any trajectory leading from the start node of G1 has ?s enabled at every intermediate node, and this behavior does not exist in any trajectory leading from the start node of G2. The preceding result suggests that simulation is more nuanced for GSTs than for synchronization trees. One naturally may wonder which of the two notions proposed in this section is the ?right? one. Our perspective is that the strong notion possesses a sense of invariance that one might expect for simulation; if one system is simulated by the other then any execution of the former can be ?traced? by the latter following only related states. In this sense, strong simulation may be seen to have stronger intuitive justifications than the weaker one. 47 Chapter 4: Generalized Synchronization Trees and State Systems 4.1 Introduction The advantages of STs have thus far been throughly celebrated. However, these advantages would do little good if STs bore no relationship to the study of other, more traditional discrete models. Thankfully, and as their popularity attests, this is not the case: as we have described already, an ordinary Labeled Transition System (LTS) that possesses an initial state may be ?unrolled? into a ST ? recall the example in Fig. 2.1. The value of this procedure, however, is that a LTS and its ?unrolling? (as a ST) are bisimilar. Thus, we can study bisimulation-invariant properties ? including composition ? with whichever structure is more convenient. And because each node in a ST has a unique incoming edge, ?unrolling? a discrete system into a tree (or ST) also ?unrolls? all of the loops in the former. This is an extremely useful structural alteration for various purposes, e.g. as a proof technique in modal logic [32]. Since the selling point of GSTs is to have a ST-like analog for continuous and hybrid system models, it is natural to ask whether GSTs, too, can be viewed as an ?unrolling? of continuous system models ? with some notion of bisimulation preserved in the process. This chapter addresses that question by showing how to 48 ?unroll? system models from a modeling framework with a fully non-discrete seman- tics : that is the behavioral framework of Willems et. al. [14]. Most importantly, we also examine how bisimulation for such behavioral systems (see [25]; see also Section 2.2) is preserved by this unrolling procedure. On one hand, conversion to a GST is demonstrated to respect bisimulation between two behavioral systems: that is two behavioral systems with bisimilar state spaces are unrolled into GSTs that are bisimilar according to the definition of strong bisimulation in [15]. On the other hand, we exhibit a condition under which strong bisimulation between two unrolled behavioral systems implies that they have bisimilar state spaces. In this latter case, strong bisimulation between the GSTs is insufficient because GSTs (and their bisimulations) have no inherent awareness of (real) time; the extra condition requires that time information be preserved by the bisimulation relation. Others have recognized the importance of time in the context of bisimulation for CPSs (see e.g. [33]), but our work remains unique in the context of GSTs, and indeed, tree-like CPS models. 4.2 Behavioral Dynamical Systems as GSTs In this section, we present a method for constructing a GST from a behavioral system ? = (T,V? D,B). As before, V represents the external signal space and D represents the internal signal space of ?. With a view to comparison with [25], we further assume that T = R?0. According to Definition 26, we need to identify a set P with a tree partial order, a set of labels L and a labeling function L. 49 In order to create a tree partial order from a behavioral system, we appeal to the intuition of unrolling a LTS into a ST. This procedure, described in the intro- duction, establishes the nodes of the ST (i.e. its states) as sequences of transitions from the underlying LTS; moreover these nodes can be partially ordered by prefix- ing. This idea generalizes to a state map that can be defined for any behavioral system; this canonical state map then captures the possibility of partially ordering states by prefixing. Proposition 2. Let ? = (T,W,B) be a dynamical system, and let B? := {f |t : ?f ? ? B, t ? T s.t. f |t = f ?|t}. For ? = B??T, the map p : B??T? ?, p : ?f, t? 7? ?f |t, t? is a state map with state space ?. Proof. This follows because ?(f, t1) = ?(g, t2) if and only if t1 = t2 and f |t1 = g|t2 = g|t1 . Thus, any trajectory which extends f must also extend g, because f and g have exactly the same values for all times up to t1 = t2. Definition 32 (Canonical Partial-Order State Map). We call the state map p of Proposition 2 the canonical partial-order state map. For a given dynamical system ?, we will denote this state map by p? and its state space by ??. The state map p is clearly past-induced and Markovian; this is an easy con- sequence of Definition 7. These properties will be important subsequently in the context of bisimulation. For now, though, the fact that states of p? are partial tra- jectories means that they can easily be ordered by prefixing; that is two states will be ordered if the function in one is a prefix of function in another. This captures 50 the unrolling idea mentioned before, and it further implies a tree partial order over the states ? the precursor to a GST. This is made precise in the following definition. Definition 33 (GST Representation of a Behavioral Dynamical System). Let ? = (T,V?D,B) be a behavioral dynamical system with external variable space V. Then the GST representation of ? is given in terms of p? as follows: ? The tree partial order is defined over the set P P = {?f |t, t? : f ? B, t ? T} ? {p0} = {p?(f, t) : f ? B, t ? T} ? {p0}, where p0 will be the root of the tree, and is chosen to make the union disjoint. ? The set P is partially ordered by  where p?(f1, t1)  p?(f2, t2) = ?f |t11 , t |t21?  ?f2 , t2? ? iff t1 ? t f |t1 = (f |t22 1 2 )|t1 and p0  p?(f1, t1) for all ?f1, t1? ? B ? T. ? The labeling function is defined for the set of labels L = V by L : p?(f1, t1) = ?f |t11 , t1? 7? ? (f |t1V 1 (t1)). Proposition 3. The partial order defined in Definition 33 is a tree partial order, and hence, (P, p0,,L) as defined therein is a GST. 51 While Definition 33 in some sense captures the idea of ?unrolling? a LTS, it does so without considering any state information about the dynamical system. No such extra consideration is need in the LTS case because trajectories consist of the states themselves (through the sequences of valid transitions). However, for behavioral systems, the trajectories under consideration do not necessarily consist of states. Nevertheless, the canonical partial order state map p? is by its nature enough to represent ? up to bisimulation ? any other past-induced, Markovian state map over the same system. The following proposition makes this clear. Proposition 4 (Bisimilarity between (?, x) and (?, p?)). Let ? be a behavioral dy- namical system with a past induced, Markovian state map x. Then the state systems (?, x) and (?, p?) are bisimilar according to Definition 11. Proof. We seek a bisimulation relation xBp ? X ??? where x : B?T? X and p? ? is the canonical partial order state map for ? (see?Definition? 32). We propose the following xBp as such a bisimulation relation: let ?, ?f |t, t? ? xBp if and only if? ? ? = x(g, t) for some ?g, t? ? B ? T such that g|t = f |t. We note that this definition is well-posed, since the state map x is past-induced : in other words, any behaviors g, h ? B for which g|t = h|t = f |t will have the property that x(g, t) = x(h, t). We start by showing xBp is a simulation relation indicating that (?, p?) sim-? ulates (?, x). Thus, let ??, ?? ? xBp where ? ? X and ? := ?f |t, t? ? ??. Then? take any w := ?v1, d1? ? B and t1 ? T such that x(w, t1) = ?; also, take any w2 := ?v2, d2? ? B and t2 ? T |tsuch that p?(w2, t2) = ?w 22 , t2? = ?. Of course p?(w2, t2) = ? implies that t = t2 and w | = f |t2 t . Thus, we have to show that 52 there exists a d?2 ? ?D(B) such that properties 1 through 4 of Definition 11 hold. However, since we are simply looking at two state maps on the same system, the natural choice for d?2 is simply d ? = d ?t22 2 t d1, and hence property 3 is immediately1 satisfied. This makes w?2 = (v t2 ? 2 ?t v1, d2) = w2 ?t2t w1; of course we know that w?1 1 2 is in B because w | = f |t2 , so x(w , t ) = x(f |t22 t2 1 1 , t2) = x(w2, t2) by the asserted membership in xBp . The extension as w1 then follows from the state map property? (see Definition 7). The preceding also trivially shows property 2 of Definition 11 is satisfied. This, taken with the fact that the state map x is Markovian, directly implies that w?2 also satisfies property 4 Definition 11. This establishes that xBp is? a suitable simulation relation; that it is also a simulation follows from the fact that the state map x is defined for all B ? T. Using almost exactly the same proof, it can be shown that xBp establishes? that (?, x) simulates (?, p?). In particular, membership of a pair of states (?, ?) in xBp asserts that the trajectories emanating from both ? and ? are the same; the? resulting states that those trajectories pass through will also be the same because the state map x is Markovian. Proposition 4 is of obvious relevance to the task at hand: recall that the state space of the state map p? is exactly the set of nodes in the GST representation of ?! Thus, because bisimulation is an equivalence over behavioral systems, Proposition 4 will allow us to chain a bisimulation relation between two GST representations of a behavioral system with any other bisimulation relation on one of the underlying behavioral systems. This is essentially the outline of the next section. 53 4.3 Comparison of Bisimulation Relations for Behavioral Dynamical Systems In this section, we demonstrate that when behavioral systems are converted to GSTs according to Definition 33, the notion of bisimulation between the trees matches the notion of bisimulation for the original behavioral systems. The cen- tral tools of this section will be Proposition 4 and the fact that bisimulation over behavioral systems is an equivalence. The comparison of bisimulation between GSTs and behavioral systems is mostly direct, but we will need the following definition, which establishes an ad- ditional property for bisimulation relations between GSTs generated according to Definition 33. Definition 34 (Time Shifting Property). Let ?1 = (T,V?D1,B2) and ?2 = (T,V? D2,B2) be two dynamical systems which share the same external signal space V. Further suppose that each dynamical system has an associated state map xi : V ? Di ? Xi. Furthermore, let G1 and G2 be the associated GSTs constructed according to Definition 33. A bisimulation relation ? between G1 and G2 is said to have the time-shift property if the following condition and its symmetric version hold: ? For each ?p1, p2? ?? and q1 %1 p1 there exists a q2 ? P2 and an order- preserving bijection ? : (p1, q1] ? (p2, q2] such that both ?p?, ?(p?)? ?? and ? ?T(p1)? ?T(p1) = ?T(?(p?1))? ?T(p2) hold for all p?1 ? (p1, q1]. Lemma 1 (Behavioral systems with bisimilar state spaces have bisimilar GSTs). 54 Let ?1 = (T,V?D1,B2) and ?2 = (T,V?D2,B2) be two dynamical systems which share the same external signal space V. Further suppose that each dynamical system has an associated state map xi : V?Di ? Xi. If (?1, x1) and (?2, x2) have bisimilar state spaces according to Definition 11, then the GSTs constructed from ?1 and ?2 (according to Definition 33) are bisimilar according to Definition 30. Moreover, it is possible to choose a bisimulation relation with the time-shift property. Proof. The proof consists mostly of applying Proposition 4 and using the fact that bisimulation is an equivalence between behavioral systems [25]. That is (?1, p?1) is bisimilar to (?1, x1) by Proposition 4, and likewise, (?2, x2) is bisimilar to (?2, p?2). Since (?1, x1) and (?2, x2) are bisimilar by assumption, we conclude that (?1, p?1) is bisimilar to (?2, p?2). In the notation from Section 2.2.2, we can express this chain of bisimulation equivalence as: ?1 p ?? x1 ?1 x1?x2 ?2 x2?p ?2. (4.1)1 ?2 Thus, the transitivity property of bisimulation as an equivalence relation [25] implies that there exists a relation p ?p ? ??1 ? ??2 for which ?? ? 1p ?? p ? .1 2 1 ? 22 However, if G1 = (P1,-1, p01,L1) and G2 = (P2,-2, p02,L2) are the GSTs constructed from ?1 and ?2 according to Definition 33, then P1 = ??1 ? {p01} and P2 = ??2 ? {p02}. Thus, we claim that ?:= p ?p ? {?p01, p02?} is a strong?1 ?2 bisimulation between G1 and G2 (with the time shifting property). It is immediately clear that this definition of ? matches each node in P1 to at least one node in P2 and conversely: p ?p is a bisimulation between (?? ? 1, p?1 2 1) and (?2, p?2), and so matches each state in ??1 to at least one state in ??2 and 55 conversely. Thus, it is only left to show that the trajectories emanating from related states satisfy the properties of Definition 30. We will show only that G2 strongly simulates G1 using ?; the proof in the other |t |t direction will be similar. To begin, suppose that ??w 1 21 , t1?, ?w2 , t2?? ? p ?? p ??1 ?2 ? |tand let w be any behavior such that w 11 1 = w ? 1|t1 to establish an maximal trajectory |t from ?w 11 , t1?. We can obtain an appropriate maximal trajectory from G2 directly from (4.1). In particular, the middle bisimulation of (4.1) and the fact that w?1 |t extends w 1 from t together imply that x (w? , t ) ? x (w? ?1 1 1 1 1 x1 x2 2 2, t2) for any w2 that |t agrees with w 22 up to time t2. If we let w ? 1 be such a trajectory in ?1, then the definition of bisimulation for behavioral systems (Definition 11) implies that there exists such a w?2 in ?2 for which the states that w ? 1 traverses after t1 can be matched bijectively ? through the time axis ? to the states that w?2 traverses after t2; hence, if we call this time-based bijection ?, then ? in fact bijectively matches each ?w?1, t?  ? |t1 ? ? ? ?  ? |tw1 , t1 to w2, ?(t) w 22 , t2? where x1(w?1, t) x1? x (w?x2 2 2, ?(t)). But employing ? |t ? |?(t) (4.1) again, we see that the latter implies ?w1 , t? p ?p ?w2 , ?(t)?, and hence,?1 ?2 ? ? |tw1 , t? ? ? ? |?(t)w2 , ?(t)?. Of course the labels along these trajectories match by construction of the GSTs and the preservation of external variables in the behavior asserted by bisimulation between behavioral systems. Consideration of trajectories emanating from ?p01, p02? follows directly from the above, since all the immediate successors of p01 and p02 have time index t = 0. Lemma 2 (Behavioral systems with bisimilar GSTs have bisimilar state spaces). Let ?1, ?2, x1 and x2 be as in Lemma 1. Suppose the GSTs constructed from ?1 and 56 ?2 (according to Definition 33) are bisimilar according to Definition 30. Moreover, suppose that the bisimulation relation satisfies the time-shift property. Then (?1, x1) and (?2, x2) have bisimilar state spaces according to Definition 11. Proof. As before, let G1 = (P1,-1, p01,L1) and G2 = (P2,-2, p02,L2) be the GSTs constructed from ?1 and ?2 according to Definition 33; furthermore, let G1 ? G2 be the claimed bisimulation relation between them. The proof then follows from the observation that ? effectively defines a bisimulation relation between the behavioral systems (?1, p?1) and (?2, p?2); the existence of this bisimulation follows from an argument that is similar to the one in the proof of Lemma 1, only in the other direction. The time-shifting property of the bisimulation is necessary here to ensure that the GST bisimulation relation translates to a behavioral-system bisimulation. Thus, the assumptions of the Lemma ? combined with Proposition 4 ? effec- tively create the following bisimulation chain (compare to (4.1): ?1 x1?p ?? 1 p ?p ?2 p ?x2 ?2. (4.2)1 ?1 ?2 ?2 The equivalence property of bisimulation for behavioral systems completes the proof by asserting the existence of a bisimulation x1?x2 . Theorem 7. Let ?1 = (T,V? D1,B2) and ?2 = (T,V? D2,B2) be two dynamical systems which share the same external signal space V. Further suppose that each dynamical system has an associated state map xi : V? Di ? Xi, which is both past induced and Markovian. Then (?1, x1) and (?2, x2) are bisimilar in the sense of Definition 11 if and only if the GSTs constructed according to Definition 33 from 57 the state systems are strongly bisimilar and are related by a bisimulation relation with the time-shift property. Proof. Lemma 1 and Lemma 2 establish the claimed necessary and sufficient condi- tions for the conclusion. It is important to note that the time-shifting property in Definition 34 really is necessary to prove Lemma 2. The following example indicates how it is possible to have bisimilarity between GSTs constructed from behavioral systems, but not between the original behavioral systems. Example 1. Let ?1 = (T,V ? D1,B1) and ?2 = (T,V ? D2,B2) be two behavioral systems such that T = R?0, V = R and D1 = D2 = {0}. Then let B1 = {w1} where w 21 = ?v1, d1? with v1 : t 7? t and d1 : t ?7 0; similarly, let B2 = {w2} where w2 = ?v2, d2? with v2 : t 7? (t/2)2 and d2 : t 7? 0. Finally, let xi : Bi ? T ? Xi, i = 1, 2 be state maps such that xi : ?wi, t? 7? 0. According to the procedure for constructing GSTs from behavioral systems, G1 = (P1, p01,-1,L1) and G2 = (P2, p02,-2,L2) are trees with a only a single branch each. That is Pi\{p0i} = {wi|? : ? ? R?0}, i = 1, 2. We claim that {?p01, p02?} ? {??w1|? , ??, ?w2|2? , 2??? : ? ? T} =? (4.3) is a bisimulation relation between G1 and G2 according to Definition 30. This is easy to establish because the trees have only one branch and we have used the time axis to suggest which order-preserving bijections to use. Moreover, this is the largest bisimulation relation between G1 and G2; this is because L1(?w1|? , ??) = ? 2 and 58 L (?w | , ??) = (?/2)22 2 ? , so (4.3) is the only way to pair nodes so that they satisfy the label matching property of Definition 30. Importantly, ? fro?m Example 1 does no?t have the time-shifting property. Indeed, let ?p1, p2? := ?w1|t1 , t1?, ?w2|2t1 , 2t1? ?? and let q1 := ?w1|t1+1, t1 + 1? %1 ?w1|t1 , t1?. Then it is obvious that any appropriate order-preserving bijection must have ?(p1) = ?w2|2(t1+1), 2(t1 + 1)? =: q2, since ?q1, q2? is the only pair in ? such that ?1?q1, q2? = q1. However, this implies that ?T(q1) ? ?T(p1) = 1 and ?T(?(q1)) ? ?T(p2) = 2(t1 + 1) ? 2t1 = 2. As ? is the largest bisimulation relation between G1 and G2, there is no bisimulation relation between those trees with the time-shifting property. Finally, we note that (?1, x1) and (?2, x2) are not bisimilar in the sense of Definition 11. Let ?1 = p?1(w1, t1) = ?w1|t1 , t1? be any element in the state space of (?1, p?1) and let ?2 = f?2(w2, t2) = ?w2|t2 , t2? be any element in the state space of (?1, p?2). We claim that ??1, ?2? cannot be in a simulation relation. In particular, observe that v ?t22 t v 2 t2 21 1 = (t/2) ?t t cannot be matched to a valid behavior in ?2,1 hence property 1 of Definition 11 cannot possibly be satisfied. Thus, there is no simulation relation which contains ??1, ?2?. Since we chose ?1 and ?2 arbitrarily, we conclude that (?1, p?1) and (?2, p?2) cannot possibly be bisimilar, and hence, neither can (?1, x1) and (?2, x2) by Lemma 1. 59 Chapter 5: GSTs and Modal Logic 5.1 Introduction One important and well known tool in the formal description and verification of discrete processes is the simple modal logic known as Hennessy-Milner Logic (HML) [18] (HML, modal logic and associated notions are summarized in Sec- tion 2.3). This is in large part because Hennessy and Milner noticed a relationship between HML and bisimulation in the context of image-finite processes: that is two image-finite processes are bisimilar if and only if they satisfy the same HML formu- las [18]. However, it?s possible to study broader classes of processes for which modal equivalence ? that is satisfying the same modal formulas ? implies bisimulation; such classes of processes are usually called Hennessy-Milner (HM) classes, although there are different variations of the main idea. In this chapter, we will concern ourselves with a notion that we call Visser-Hollenberg Hennessy-Milner (VHHM) classes after the work in [27]. Specifically, a VHHM class of Kripke Structures (KSs) is a class of KSs with the following property: whenever two worlds (or states) from any of the constituent KSs satisfy all the same modal formulas, they are necessarily bisimilar to each other [27]; this specifically includes the case when both nodes come from the same tree. Importantly, however, [27] proceeds to define and characterize max- 60 imal VHHM classes of KSs. Maximal VHHM classes are particularly interesting from the point of view of system composition, because that maximality circum- scribes the operations one can perform and still be able to distinguish bisimulation non-equivalence with modal formulas. In other words, composition operations that preserve membership in a VHHM class will produce KSs that remain distinguishable by modal formulas if they become non-bisimilar; by contrast, composition opera- tions that ?spill out? of a maximal VHHM class obviously lose that property. [27] considered some basic process-algebraic-like operations with respect to the VHHM class of m-saturated KSs. A result like this for continuous and hybrid systems models would have ob- vious implications for the design and diagnosability of CPSs, particularly in the context of systems whose behavior is difficult to reason about. GSTs are a natural substrate from which to begin such a generalization: in Section 5.2, we begin this project by first proposing a Generalized Hennessy-Milner logic (GHML) ? that is a modal logic like Hennessy-Milner Logic (HML) but with semantics specific to GSTs ? and consider its relationship to maximal VHHM classes of GSTs with respect to weak bisimulation [19]. As in the discrete case, then, whenever CPS systems can be modeled using composition operators that are consistent with a maximal VHHM class of GSTs, the design-test-redesign iteration benefits from valuable additional information: a design or implementation that fails to meet a specification (relative to bisimulation) will have a GHML witness to that deviation. As GHML, like HML, is a quite simple logic, a GHML witness offers an easy-to-interpret description of how the specification is violated. Consider for example the value of such a witness in 61 the context of a modern networked control system that combines software, network effects and real-world dynamics in a very complicated way: in such a circumstance, a GHML formula could explain a specification violation in terms of network delays that affect a feedback loop around physical dynamics, ultimately leading to insta- bility. Likewise, modern machine learning algorithms are increasingly implemented in real-world-connected CPSs such as autonomous vehicles, yet those algorithms produce classifiers whose decisions inherently lack ?explainability? on their own, let alone as part of a larger, more complicated system. In such a situation, a GHML formula could clarify how undesirable decisions from a road-sign classifier, say, lead to unexpected behavior from the physical dynamics of the car as whole. However, to reach this end goal for GSTs, there is an important additional consideration relative to the discrete case: GSTs have the flexibility to capture all sorts of continuous and hybrid behavior, so it is not immediately clear what sorts of practical ?dynamical? behaviors are associated with any particular VHHM class, especially as this involves translating ?timed? LTI systems into the domain of GHML and weak bisimulation, which lack a comparable, inherent notion of ?clock? time. That is: describing a VHHM class of surrogate KSs ? and hence a VHHM class of GSTs ? says nothing about the sorts of practical dynamical-system models that will end up in that class; this is in contrast to the discrete case where the characterization of VHHM classes is in terms of the very models of interest, KSs. Put another way, there are likely to be some subclasses of GSTs that are of significantly more practical importance than others, and their relationship to surrogate KSs and maximal VHHM classes is an important consideration for practical reasons at least. 62 Specifically, this immediately begs the basic question of whether any reasonable classes of dynamical system models fit inside a single maximal VHHM class of GSTs to begin with. And if a particular class of dynamical systems is not encompassed by a single VHHM class, then we can simply ask what further specifications are needed to select a sub-class that is so encompassed. These (and other similar) questions get at the heart of which continuous-time dynamical behaviors can be captured by the expressiveness of the clock-time-unaware weak bisimulation and GHML. Of course, these questions necessarily address as a special case the continuous behaviors that are captured by m-saturated surrogate KSs composition directed questions, and as such, must form the basis for compositional results of the sort alluded to above. The remainder of this chapter, then, is devoted to specifying a class of finite- dimensional, Linear Time-Invariant (LTI) control systems, along with a suitably constrained class of inputs, that have this property. Unfortunately, we cannot con- sider either arbitrary LTI systems or arbitrary inputs: this is because even the relative specificity of LTI dynamics is not enough to result in surrogate KSs that have some manageable structure (viz. nondeterminism). Indeed, this project first involves considering the structure of the surrogate KSs obtained from the GST encodings of such systems. Importantly, however, weak bisimulation essentially ignores real (clock) time information, so the surrogate KSs obtained from deterministic LTI systems will have interesting and non-trivial non- determinism, despite the above mentioned restrictions. The conversion of LTI systems to GSTs is the topic of Section 5.3; the structure of the resultant nonde- terminism is characterized in Section 5.4. As mentioned before, we will introduce 63 restrictions on the LTI conversion process so as to end up with specific and man- ageable nondeterminism in the resultant GSTs and their surrogate KSs. Of course the nature of this nondeterminism has implications for the VHHM classes to which such LTI systems may belong; this is addressed in Section 5.5, which connects the prequel to GHML and modal logic specifically. 5.2 Generalized Hennessy-Milner Logic (GHML) 5.2.1 GHML for GSTs: Syntax and Semantics Since KSs and STs have well-defined ?outgoing edges? from their states, the label inside the HML diamond modality can be naturally matched to those edges (or transitions). As noted before, though, nodes in GSTs generally lack immediate successors. Thus, the project of generalizing HML is essentially one of generalizing the label in the diamond modality, so that it can be appropriately matched to the semantics of GST trajectories (see Definition 27). The proposed mechanism for this is to define the logic in terms of a linear, total order, called a domain of modalities, that can then be compared to GST trajectories via order equivalences [19]. Definition 35 (Domain of modalities [19]). A domain of modalities is a totally ordered set, (I,I), together with a set of labels L. Of course the bounded GST trajectories used in the definition of weak bisim- ulation have both a ?starting? point and an ?ending? point, so we should confine ourselves to such subsets of a domain of modalities. 64 Definition 36 (Left-open subset [19]). A subset I of a totally ordered set I is left open (and right-closed) if it satisfies the following two conditions: ? it has both a least upper bound (LUB) and a greatest lower bound (GLB) in I; and ? it contains its LUB but doesn?t contain its GLB. Importantly, the preceding definition allows left-open subsets to have ?gaps? in them. This is meant to facilitate the treatment of hybrid systems with more complicated time constructs; see for example [33]. Left-open subsets capture the essence of GST trajectories, but they don?t capture the external interactions (labels) associated with those trajectories. Hence, the following definition, which forms the basis for our generalized diamond modality. Definition 37 (Modal execution [19]). Let (I, L) be a domain of modalities. A modal execution is a map from a left-open subset of I to the set of labels, L. The set of modal executions over (I, L) will be denoted M(I, L). Of course different modal executions may represent essentially the same ?se- quence? of external interactions in much the same way order-equivalent trajectories do. Hence we extend the idea of order equivalence to modal executions in the sequel. Definition 38 (Order Equivalent Modal Executions [19]). Let E1 : I1 ? L and E2 : I2 ? L be two modal executions from a domain of modalities (I, L). We say o.e that E1 is order equivalent to E2 or E1 ? E2 if there exists an order preserving bijection ? : I1 ? I2 such that E1(i) = E2(?(i)) for all i ? I1. The collection of o.e equivalence class of M(I, L) under ? will be denoted |M(I, L)|. 65 To maintain consistency with the semantics of GSTs, we will have to impose the following additional condition on domains of modalities; we will assume it applies to all domains of modalities considered henceforth. Definition 39 (Closed under left-open concatenation [19]). We say that a totally ordered set I is closed under left-open concatenation if for any two left-open o.e subsets I1, I2 ? I, there exists another left-open set I3 ? I such that I3 ? I1; I2 where I1; I2 , ({1} ? I1) ? ({2} ? I2) is totally ordered under the lexicographic ordering. A totally ordered set I that is closed under left-open concatenation will be denoted I?. We are now in a position to write down the syntax of GHML in terms of |M(I?, L)|; the use of such equivalence classes will be important in the subsequent development of VHHM classes of GSTs. Definition 40 (Set of Generalized HML (GHML) formulas [19]). Given a domain of modalities (I?, L) that is closed under left-open concatenation, the set of Gener- alized HML (GHML) formulas is the set of formulas, ?GHML(I?, L), inductively defined according to the following rules: ? := > | ?? | ?1 ? ?2 | ??|E|??? (5.1) where |E| ? |M(I?, L)| is an equivalence class of modal executions over the domain of modalities (I?, L). The use of double angle brackets in Definition 40 may seem redundant, but it will be an important distinction in the future, since we will eventually consider ordinary HML modalities with the same sorts of labels; see the sequel, Section 5.2.2. 66 Finally, the semantics of GHML (over GSTs) is defined in more or less the expected way: that is in terms of order equivalences between trajectories in the GST and modal executions over a given domain of modalities. The details are available in [19]. 5.2.2 VHHM Classes of GSTs The important realization in [19] is that, as far as weak bisimulation and GHML are concerned, we can work with certain discrete structures instead of GSTs. These structures were dubbed surrogate Kripke structures, and they are the basis for the main results in [19]. Definition 41 (Captured by a Domain of modalities [19]). Let U be a set of GSTs. We say that U is captured by a domain of modalities (I?, L) if every trajectory from every GST in U is order equivalent to some modal execution over (I?, L). Definition 42 (Surrogate Kripke Structure [19]). Let U be a set of GSTs that is captured by a domain of modalities (I?, L). For any GST G = (P,P , p0,L) in U , we define a surrogate Kripke structure, G = (P, {RG|E| ? P ? P : |E| ? M(I?, L)}, V ), as follows: ? the set of states is P ; and ? ?|E|p1 p2 ? i.e. p1RG|E|p2 ? if and only if p1 P p2 and (p1, p2] is order equivalent to an element of |E|; and ? V : ?? {P} indicates all propositional variables are true in all states in P . 67 The importance of surrogate KSs is revealed by the following two theorems, both with rather straightforward proofs [19]. Theorem 8 (Relating GHML formulas on G to HML formulas on G [19]). Let (I?, L) be a domain of modalities, and let U be a set of GSTs captured by (I?, L). Furthermore, consider HML over the set of labels given by |M(I?, L)|. Then for every G = (P,P , p0,L) ? U , 1. for all ? ? ?GHML(I?, L), G |= ? ? p0 |= ??? and 2. for all ? ? ?HML(|M(I?, L)|), p0 |= ? ? G |= ??? ??. The notation ??? indicates that the GHML formula ? is converted to an HML for- mula by replacing each ??|E|?? modality with the corresponding HML modality ?|E|?. ??? ?? indicates an analogous conversion from an HML formula to a GHML formula. Theorem 9 (Weak bisimulation between GSTs and bisimulation between surrogates [19]). Let U and (I?, L) be as in Theorem 8. Furthermore, let G1 = (P,P , p0,LP ) and G2 = (Q,Q, q0,LQ) be two GSTs in U . Then G ?1 w G2 ?? p ?0 q0. (5.2) where the bisimulation p ?0 q0 is taken in the context of the surrogate Kripke struc- tures G1 and G2. Thus, as far as GHML and weak bisimulation are concerned, we may as well work with surrogate KSs instead of GSTs! This connection to KSs, though, leads to another important consequence: it allows us to define and constrain maximal VHHM classes of GSTs in terms maximal 68 VHHM classes of KSs. We begin with the following predictable definition of VHHM classes for GSTs. Definition 43 (VHHM class for GSTs [19]). Let U be a set of GSTs, and let (I?, L) be a domain of modalities that captures U , so that ?GHML is interpreted with respect to ?GHML??(I?, L). Then we say that a subset h ? U satisfies the VHHM property for GSTs if for any two sub-GSTs G1|p and G2|q from the set h (possibly with G1 = G2), G1| ?p w G2|q ?? G1|p ?GHML G2|q. (5.3) Note, however, that we can go from modal equivalence for two nodes in a GST to bisimulation for those two nodes by going through the surrogate KSs for the respective GSTs. Since the GST semantics imposes certain characteristics on the transition structure of the surrogate KSs, we may then further constrain maximal VHHM classes of GSTs in terms of maximal VHHM classes of KSs that contain as theorems the appropriate schemata. Theorem 10 (Maximal VHHM classes for GSTs and refined Henkin-like models). Let U and (I?, L) be as in Definition 43, and let h ? U be a VHHM class of GSTs. Furthermore, let ? be the smallest normal logic that contains all of the following: ? the propositional variables ?; ? ?|E1|, |E2| ? |M(I?, L)|, the schema ?|E1|??|E2|??? ?|E1;2|?? ; and ? ?|E|, |E1|, |E2| ? |M(I?, L)| such that there is an order equivalence ? : I1; I2 ? dom(E) with E ? ?(1, ?) ? |E1| and E ? ?(2, ?) ? |E2|, the schema ?|E|?? ? 69 ?|E1|??|E2|??. Then {G : G ? h} ? BS(HC?) for some Henkin-like model HC? that preserves the first-order transition-relation properties imposed on C? by the schemata above. Furthermore, if there is a set h? ? U such that h ? h? and {G : G ? h?} ? BS(HC?), then h? is a VHHM class of GSTs. Given the relationship between surrogate KSs and both weak bisimulation and GHML (Theorems Theorem 9 and Theorem 8, respectively), Theorem 10 seems to be a rather straightforward bound on the ?size? of VHHM classes of GSTs. However, this superficial simplicity belies two important subtleties that ultimately have to do with the fact that VHHM classes are characterized by Henkin-like models, which in turn are obtained by removing transitions from the Henkin model. First, the stipulation that HC? preserve the appropriate first-order transition- relation properties is essential. C? necessarily satisfies the transitivity and weak- density properties imposed by the schemata in Theorem 10, essentially because the canonical model contains enough transitions to ensure that this is the case; see [26]. However, after removing transitions from the canonical model to get an arbitrary Henkin-like model, these first-order properties need not hold! Of course we know that the surrogate KSs generated from GSTs must satisfy these first-order properties by the nature of their semantics, so we should confine ourselves to such Henkin- like models in order to ensure the bisimulation inclusion (operator B) captures the surrogate KSs. Second, using equivalence classes of modal executions to label GHML modal- 70 ities is also important relative to the characterization of VHHM classes in terms of Henkin-like models. Had we not chosen to use such equivalence classes, then we could generate Henkin-like models by removing transitions reflecting one modal execution but not some other order-equivalent modal executions! Such a situation would reflect a deviation from the semantics of GHML with respect to GSTs, for it would be possible to assert the existence of a trajectory through one diamond modality and simultaneously the lack of such a trajectory through another, simply by choosing modal executions with different domains! 5.3 Linear Time-Invariant Systems as GSTs In this section, the objective is to represent the ubiquitous finite-dimensional LTI control system models as GSTs. This section will be a middle ground between background material and novel content. On the one hand, we will follow a well- established approach to obtain GST representations from LTI control systems ? see [15, 17] and Chapter 4; on the other hand, we introduce here some novel but non-trivial constraints on the LTI systems and their admissible input functions that will prove relevant in subsequent sections. The universal aim of these restric- tions will be to alter the nondeterminism that appears in the resultant surrogate KSs, so that the resulting surrogate KSs have a manageable (but still nontrivial) structure. The consequences of these assumptions will extend through the remainder of this work. 71 5.3.1 LTI Systems In this chapter, we will use the terminology ?LTI system? as a short hand for finite-dimensional LTI systems that admit a state-space representation; we will further confine ourselves to LTI systems that evolve over a real-valued time axis. LTI systems of this form can be described in terms of three quantities: the state, the input and the output. The state of such a system at any particular time will be given by a vector in Rn, and that state will evolve (in time) according to a system of first-order ordinary differential equations (ODEs) that are written in terms of the component-wise derivatives of the state evolution function. The inputs to the system at a particular time will be given by a vector in Rm, and those inputs as a function of time affect the evolution of the state through the aforementioned ODEs. The outputs of the system at a particular time are given by a vector in R`, and they will be specified as an appropriate function of only the current value of the state. Thus, for our purposes an LTI system will be described by a set of equations like this: x?(t) = Ax(t) +Bu(t) (5.4) y(t) = Cx(t) where A, B and C are constant, real-valued matrices with dimensions n? n, n?m and `?n, respectively. In keeping with the above, x(?) is called the state trajectory (with codomain Rn), u(?) is called the input trajectory (with codomain Rm), and y(?) is called the output trajectory (with codomain R`). As a matter of future convenience, we will impose the following assumption on the structure of the LTI systems that we will consider: 72 (A1): The matrix CB is full column rank. The reason for this assumption will become clear later, in Section 5.4; however, like all of the assumptions we make, it is directed at eliminating a particular source of non-determinism in the surrogate KS. 5.3.2 LTI Systems as GSTs The most natural way of converting an LTI system like (5.4) into a GST involves regarding such a system as a set of functions (or trajectories): one vector- valued function each for the state, the input and the output. This trajectory view of dynamical systems was an insight that was pioneered by [13] ? though it was closely related to a similar ideas for discrete systems ? and it formed the basis of the GST constructions in both [15] and [17]. We will essentially replicate that type of construction below. 5.3.2.1 Admissible Input Functions As we are considering LTI systems in terms of their trajectories, it is first necessary to specify exactly what input trajectories we will permit. We will not, however, consider the same broad class of input functions described in the above references. The restrictions that we will impose on the admissible input functions directly service the goal of minimizing the non-determinism in the GST conversion; this will become clear in Section 5.4. First and foremost, we will confine ourselves to inputs u that are piecewise 73 analytic; for real-valued functions, we mean by this that about each point in its domain, u is (component-wise) representable by a convergent power series (with a non-trivial region of convergence); see also [34]. This forms the first rather strong assumption that we will make on the input functions: (A2): u : R?0 ? Rm is piece-wise analytic and continuous from the right (also with well-defined limits from the left). Note the assertion that an input signal starts at time t = 0; however, it is the analyticity assumption that is most important. Indeed, the latter leads to the immensely useful consequence in the following proposition. Proposition 5. For any (piece-wise) analytic input, u (with an appropriate region of convergence), both the resultant state trajectory and output trajectory of the LTI system (5.4) are also (piece-wise) analytic. Proof. Analytic functions may be added, multiplied, integrated and differentiated on their regions of convergence (or the intersections thereof) to obtain further analytic functions. Since ? t x(t) = eAtx + eA(t??)0 Bu(?)d? (5.5) 0 where eAt is the usual (matrix) exponential power series, both x and y are specified by such operations on (piece-wise) analytic functions; hence, they are also (piece- wise) analytic. This assumption will help eliminate non-determinism in the surrogate KS through a very special property of non-constant analytic functions: such functions 74 are known to have isolated zeros ? that is each zero of such a function is contained in an open interval that contains no other zeros. The usage of this fact will be made clear in Section 5.4. We will now introduce a second and final restriction on the allowable input functions, u, that concerns how such inputs interact with their associated LTI sys- tems response. This interaction will be defined in terms of the following property of system states. Definition 44 (Output Invariant). We say that two states x1 and x2 (from a com- mon LTI system) are output invariant if ?t ? 0 . CeAt(x1 ? x2) = 0. (5.6) Equivalently, x1 ? x2 ? N (O), where N (O) is the null space of the usual n ? ` ? n observability matrix matrix, O. The matrix O is defined as usual according to: [ ] O = C;CA;CA2;CA(n?1) . (5.7) Remark 1. At no point will we assume that O is full rank: i.e. we consider even systems that are not observable! Note: the system may still be unobservable, even though (A2) asserts that CB is full rank! Note that the above definition of output invariance defines an equivalence relation on states in Rn: moreover, the set of output invariant states with respect to any particular x ? Rn is given by x+N (O). In particular, any such equivalence class of output invariant states can be identified with a linear space, and such equivalence classes modulo a subspace are easily given a vector space structure themselves; this 75 is a common construction that is usually described as a quotient vector space. For convenience, we denote the quotient space Rn/N (O) by N (O)? and the equivalence class associated with a particular vector x by [x]. The assumption we make on the inputs is then described in terms of an a priori specified function that will ultimately constrain the (analytic) input segments allowed for any given value of state and input to the LTI system. Definition 45 (Branching Choice Function). A branching choice function for an LTI system (A,B,C) is a (pair of) (total) functions F = (F0,F 6=0), defined over a partition of D = {([x], u) ? N (O)? ? Rm : CA[x] + CBu = 0}: F 2 m0 : {([x], u) ? D : CA [x] + CABu = 0} ? R \{0} (5.8) F 6=0 : {([x], u) ? D : CA2[x] + CABu 6= 0} ? (Rm)N. (5.9) Now, we may specify the relevant assumption on the inputs in terms of an a priori fixed branching choice function, F : 76 (A3): Let F be our given, fixed branching choice function, and let x and y be the state and output trajectories for some (admissible) input trajectory, u. For any t ? 0, if ([x(t)], u(t)) ? D and y and u are not constant on some interval [t, t+ ), then the following conditions must be satisfied. ? If ([x(t)], u(t)) is in the domain of F0, then ? u?(t) = F0([x(t)], u(t)). ? If ([x(t)], u(t)) is in the domain of F 6=0, then ? if u?(t) 6= 0, then for some component of the output, 1 ? k ? ` sign([[CA2[x(t)] + CABu(t) + CBu?(t)]]k) = sign([[CA2[x(t)] + CABu(t)]]k) (5.10) and for all integers j ? 3, j ? [[CA2[x(t)] + CABu(t) + CBu?(t))]]k ? [[CBu?(t)]]k 6= 0; (5.11) ? if u?(t) = 0, then let {Uk} = F 6=0([x(t)], u(t)) and require ?? u(?) = u(t) + Uj?2(? ? t)j for ? ? [t, t+ ?]; (5.12) j=2 that is u has the particular form of the power series given above in some neighborhood of t. It is because of this interpretation that we call F a branching choice function: it 77 constrains the allowable input functions u (through their first derivatives or the power series above) at any particular state. These particular constraints are rather unintuitive, but it will become clear subsequently how compliance with these constraints will reduce the nondeterminism in LTI-derived GSTs. For now, though, it is important to recognize that, through the use of a branching choice function, these constraints are imposed identically throughout the evolution of the LTI system, no matter when or how particular states/inputs are reached. On the other hand, (A3) does not require the same inputs to be enabled in all such ([x], u) pairs! Note also that F0 merely constrains u?(t) to be a fixed, common value any time the system passes through a particular ([x], u) in the domain of F0; the higher derivatives of u are unconstrained by this requirement. Likewise, the constraints on ([x], u) pairs in the domain of F 6=0 generally leave the higher derivatives of u free, except in the final case where u?(t) = 0; there all of the derivatives of u are essentially fixed through the power series expression as described above. There is an important consideration relative to assumption (A3) that must be addressed, though, since (A3) involves the interaction between inputs, states and outputs. In particular, one must take care to be ensure that there are is a reasonable ? and consistent ? collection of system trajectories that satisfies (A3)! We will address this issue in the next subsection, where we take up the question of specifying the set of behaviors for an LTI system. 78 5.3.2.2 Construction of the GSTs The assumptions in the previous subsection specify the set of input functions we consider admissible, and hence the trajectories generated by a particular LTI system. As a matter of convenience, we will generate one GST per LTI system per initial condition, so we describe the set of behaviors of a particular LTI system as follows: Definition 46 (Behaviors of an LTI System). An LTI system (as in (5.4)) that satisfies (A1) will have a set of behaviors (from initial condition x0) specified by: { Bx0(?A,B,C) = (u, y, x) ? (R ?0 ? Rm)? (R?0 ? R`)? (R?0? ? ? R n) :}x(0) = x0 x?(t) = Ax(t) +Bu(t) y(t) = Cx(t) u, x and y satisfy (A2) . (5.13) Following terminology in [13] and [17], the trajectories u and y will be associated with external variables, and the trajectory x will be associated with an internal variable. A set of behaviors like Bx0 is adequate to specify a GST using the subsequent methodology; see also [15, 17] as noted above. However, in the spirit of reducing nondeterminism in the resultant surrogate KSs (for the purposes elucidated in the introduction), we also need to incorporate the restrictions of (A3) in a consistent way. We can accomplish this by indexing Bx0 further by a particular branching choice function, F = (F0,F 6=0), and then truncating behaviors in Bx0 that fail to comply with (A3) (as it is specified by F). Thus, we proceed inductively along the sequence of isolated zeros of y? in a behavior (u, y, x) ? Bx0 in order to evaluate that behavior?s candidacy in a new set (of behaviors) that complies with (A3), BFx .0 79 Definition 47 (Choice-Restricted Behaviors of an LTI System). Let Bx0 be as in Definition 46, and let F = (F0,F=6 0) be a given branching choice function as de- scribed in Definition 45 and (A3). Furthermore, for a given behavior b = (u, y, x) ? Bx0, define { (b)Tk } to be the (possibly empty) sequence of times corresponding to the isolated zeros of the function y?(t) = Cx(t) = CAx(t) + CBu(t). Then the set of choice-restricted behaviors is given by { ? BFx (A,B,C) ={ b|)T : b = (u, y, x) ? B0 x0 }} (b) (b) (b) T = min Tk : ([x(Tk )], u(Tk )) fails to satisfy (A3) under F (5.14) where the notation |)T indicates that the truncation operator excludes T itself (and so restricts b to a right-open interval of the time line, R). In the case that T =?, the restriction operation is ignored, and the behavior is included unmodified; if T = 0, then the entire behavior is considered to be excluded. Given such a set of choice-restricted behaviors, we can follow the straight- forward procedure in [15, 17] to create a GST; the only material difference is in the restrictions we have placed on the input functions (encapsulated as it is in the specification of the the choice-restricted set of behaviors, BFx (A,B,C)).0 Definition 48 (GST representation of an LTI system). Given a set of behaviors derived from an LTI system, Bx0(A,B,C), we construct a GST Gx0(A,B,C) = (P,, p0,L) according to the following. 80 ? The set P is given by { P = (t?, f | ?0 ? m+`+n[0,t?]) ? R ? ([0, t ]? R ) : } { } ?f = (u, y, x) ? BFx (A,B,C) ?t ? [0, t?] . f(t) = f |[0,t?](t) ? p0 0 where p0 is the root of the tree, and it is chosen to make the union disjoint. ? The set P is partially ordered by  using trajectory prefixing as follows: ?(t?1, f | ), (t?1 [0,t? ] 2, f2|[0,t? ]) ? P\{p1 2 0} : ? (t?1, f ? 1|[0,t? ])  (t2, f2| ) ? t? ? t?[0,t? ] 1 2 ?t ? [0, t?1 2 1] . f1|[0,t? ](t) = f2|1 [0,t?2](t) and ?(t?1, f1|[0,t? ]) ? P\{p0} : p0  (t?1 1, f1|[0,t? ]).1 ? The labeling function L : P\{p } ? R`+m0 is given by L : (t? , (u, y, x)| ) ? P\{p } 7? (u(t?), y(t?1 [0,t?1] 0 )). It is important to note that the possibility of choosing among piece-wise ana- lytic input functions will generate ?asymptotic? branching behavior: in particular, such an input function can be ?interrupted? with a new piece-wise analytic input function at any time to obtain a new piece-wise analytic input function! This means that at any given time there are executions of the system with multiple different control inputs allowed, and this is possibility is reflected in the GST by the existence of different nodes with the same (partial) state and output trajectories. 81 Another important observation about this construction is that it reflects the nature of LTI systems as past-induced and Markovian state-based systems. In par- ticular, the elements of P themselves can be regarded as having the property of states for the underlying LTI system; this is explained more precisely in [17]. 5.4 LTI Systems and Order-Equivalence Semantics The goal of this section is to describe the fundamental nature of order equiva- lences between LTI-derived trajectories; this is an important way point on the path to characterizing surrogate KSs of LTI-derived GSTs. The restrictions described in Section 5.3 play a special role here, as they have the effect of restricting the possi- ble order-equivalences between LTI-derived trajectories in some manageable ? even minimal ? way. Understanding the nature of these order equivalences is of course a necessary prerequisite to understand VHHM classes of such systems in the context of GHML and weak bisimulation, since those notions are defined in terms of order equivalent trajectories. Moreover, this task will ultimately be easier because we have created context where there is some minimal, manageable characterization of order equivalences. Importantly, the weak bisimulation/GHML semantics ? essentially the seman- tics of order equivalences (see Definition 28) ? can be seen to turn essentially deter- ministic GSTs into non-deterministic surrogate Kripke Structures; this fundamental fact has significant consequences as far as surrogate KSs are concerned. To get a sense of this phenomenon, recall the following example of a GST from [19] and 82 jEj jEj jEj jEj G[0;1] : : : : : : : : : 0 x yjEj 1 jEj G[0;1] 0 x y 1 Figure 5.1: GST and surrogate KS from Example 2; define E : (0, 1]? {?}. depicted in the lower portion of Fig. 5.1. Example 2 ( [19]). Consider the following GST defined over the unit interval [0, 1] ? R: G[0,1] := ([0, 1],?R, 0, (0, 1]? {?}). (5.15) Note that the GST G[0,1] is about as deterministic as one could hope for, since it has essentially no branching behavior at all: indeed, the tree partial order is itself also a linear order ! However, when we consider G[0,1] in the context of a natural domain of modalities, (I? ,?R) = (R,?R), the surrogate KS exhibits explicit non-determinism: see the surrogate KS in the upper portion of Fig. 5.1! Of course this feature will inevitably manifest itself even in deterministic LTI systems when they are converted into GSTs using the methodology of the previous section; thus, the results of this section may be regarded as ultimately describing the nondeterminism of the those GSTs under this order-equivalence semantics. Indeed, the restrictions we imposed on our LTI systems and their inputs will eventually result in surrogate KSs that have some minimal amount of non-determinism; this effort makes the nondeterminism more tractable going forward, but even so, it leaves behind the essential character of nondeterminism described above, which seems prac- 83 tically unavoidable. In the subsequent section, then, we will examine VHHM classes associated with such GSTs by studying the special and specific modal properties of this nondeterminism (as these nondeterministic structures appear throughout such GSTs). 5.4.1 Preliminaries Before we begin the primary enterprise, we use this opportunity to introduce some important facts and notation about order equivalences in LTI-derived GSTs. First, we note that trajectories in an LTI-derived GST Gx0(A,B,C) have a natural order-preserving bijection between half-open subintervals of the real-line; this is simply by the nature of the tree partial order in terms of partial time trajectories, ordered by prefixing. Hence, we have the following remark. Remark 2. Let Gx0(A,B,C) be a GST created according to Section 5.3, and con- sider a pair of trajectories in Gx0(A,B,C) that are specified by left endpoints p ? i = (t?i, (ui, yi, xi)|t? ) and right endpoints p??i = (t??i , (ui i, yi, xi)|t??) for i = 1, 2. Withouti loss of generality, we will generally describe an order equivalence between (p? , p??1 1]? (p?2, p ?? 2] using a state-trajectory-specific function that is an order-preserving (mono- tonic) bijection from one half-open subinterval of the real line to another: ? : (t? , t??]? (t? ??x1,x2 1 1 2, t2]. (5.16) Such a ? is thus ?localized? to a particular pair of state/input trajectories, so that times can be uniquely associated with GST nodes; however, we will often omit the state subscripts for readability. Of course this ? should preserve GST labels as 84 expected: (u1(t), y1(t)) = (u2(?(t)), y2(?(t))) for t ? (t?1, t??1]. (5.17) Given this remark, we can state two further useful facts based on what we know about monotonic functions defined over the reals and the assumptions we have made about our GSTs. Proposition 6. Let ? : (t? , t??] ? (t? , t??1 1 2 2] be an order equivalence between two tra- jectories (u1, y1, x1) and (u2, y2, x2) in a GST Gx0(A,B,C). Then we can uniquely extend the domain and codomain of ? so that ? : [t? , t??1 1] ? [t?2, t??2] is an order- preserving bijection. In particular, u1(t ? ) = u (t?1 2 2) and y1(t ? 1) = y(t ? 2). Proof. This follows from the assumed right-continuity of the inputs (A2) and the continuity of the outputs; the latter is a consequence (5.5). Proposition 7. An order-preserving (monotonic) bijection ? : [t? ??1, t1] ? R ? [t?2, t ?? 2] ? R is continuous at every point in its domain and differentiable at almost every point in its domain. Proof. First, we know that any monotonic function ? : [t?1, t ??]? [t? , t??1 2 2] is continuous at all but countably many points in its domain [35]. But if such a function is, in addition, bijective, then it is necessarily continuous at every point in its domain; this follows from the special nature of the discontinuities for monotonic functions on R [35]. Thus, such an order equivalence function is in fact continuous at every point in its domain and differentiable almost everywhere, the latter being an explicit claim in [35]. 85 5.4.2 LTI Systems and Order-Equivalence Non-determinism: Purely Analytic Inputs and ?Local? Non-determinism Structure Now consider an arbitrary LTI system started from the initial condition x0 = 0. Irrespective of the choice of A, B and C, the output at time t = 0 is necessarily y(0) = 0; moreover, the point x = 0 makes Ax = 0 for any such LTI system, so the output will continue to remain at zero for as long as the input is set to zero! Of course these trajectories also satisfy assumptions (A1)-(A3) ((A3) in particular doesn?t apply since we?ve posited constant input/output trajectories). Thus, if we retain the natural domain of modalities, (I? ,?R) = (R,?R), then the surrogate KS for G0(A,B,C) will share a structure like that in Example 2 for all of the GST nodes specified by the state/input trajectories (u, x) : [0, t?] ? [0, t?] ? {0} ? {0} ? all of which have (GST) labels (u(t?), y(t?)) = (0, 0). In other words, for any t? < t??, the surrogate KS will have a transition |Z : (0, 1] ? {0} ? {0}| from the node specified by (u, x1) : [0, t ?] ? [0, t?] ? {0} ? {0} to the node specified by (u, x2) : [0, t ??] ? [0, t??] ? {0} ? {0}! In particular, the surrogate KS exhibits nondeterminism in this |Z| transition at each such GST node, including the one for the associated singleton state/input trajectory that ends at t = 0 (the ?beginning? of this constant input/output trajectory in the GST/LTI system). So it is quite clear that even for our deterministic LTI systems, constant inputs that yield constant outputs will generate some kind of nondeterminism in the corre- sponding surrogate KS: this is through the (above described) possibility that differ- ent trajectories may be order equivalent even though they end up in different states. 86 Moreover, constant inputs are included in most practical classes of input functions, so this type of constant-input/constant-output nondeterminism would seem to be un- avoidable for all intents and purposes. Hence, the goal of this section can be recast as answering the question of whether or not there are other possible sources of nondeterminism in such surrogate KSs ? manifest as they must be in more diverse order equivalences between LTI-system trajectories. In particular, the possible al- ternatives are order equivalences between non-constant input/output trajectories or order equivalences between trajectories that don?t start at t = 0. However, as we have alluded to earlier, the assumptions (A1)-(A2) were chosen quite deliber- ately to avoid nondeterminism in these situations. And it is in this sense that we have specified the minimum amount of nondeterminism that can emerge in an LTI system?s surrogate KS. Thus, given a GSTGx0(A,B,C), we outline a proof that this constant-input/constant- output nondeterminism is essentially the only nondeterminism in the transitions em- anating from a given node in the surrogate KS; this will be a specific consequence of the assumptions we have made in Section 5.3. Hence, we suppose that we have a fixed node ? or more generally, a fixed initial condition ? for the aforementioned LTI system, and we attempt to characterize all of the order equivalent trajectories emanating from that point. Overall, the strategy is to build order equivalences by using induction on the time intervals associated with the analytic segments of a particular input u. Initially, though, we will consider only order equivalences that begin at time t = 0 and span a single analytic segment of input. This will prove to be without loss of generality, since the time invariance of the underlying dynamics 87 will allow us to consider nodes elsewhere in Gx0(A,B,C), or equivalently, analytic input segments that start at later times. However, there is a further important prerequisite for an inductive argument that incorporates a sequence of analytic seg- ments of input: unfortunately, an order equivalence really only supplies first-hand knowledge about inputs and outputs ? rather than states ? so we must first spec- ify a state-based invariant that will be preserved under order equivalence, at least for any order equivalence between trajectories whose initial conditions satisfy the invariant. This is indeed essential, because even order equivalent trajectories ema- nating from the same initial condition can leave the system in different states. This consideration means that as we characterize order equivalences, we will also have to show that any candidate order equivalence preserves the aforementioned invari- ant (as a prelude: we will consider order equivalences for all of the permutations of constant/non-constant inputs with constant/non-constant outputs). As claimed, this will allow us to build order equivalences between arbitrary trajectories by in- duction. Of course the invariant we?re going to use was already introduced (with some prescience) in Section 5.3: we?re going to work in terms of output invariance between states. As indicated in the program above, we will initially consider trajectories start- ing at time t = 0 and emanating from states that are output invariant, since this will prove to be an invariant with respect to all of the possible order equivalences. Now, to characterize order equivalent trajectories under these assumptions, we will further divide the problem into consideration of the following permutations of constant/non- constant inputs and outputs: the constant-input/constant-output order equiva- 88 lences from the example above; the non-constant-output/non-constant-input order equivalences; the constant-output/non-constant-input order equivalences; and the non-constant-output/constant-input order equivalences. For all but the constant- input/constant-output case, the task will be to show that whenever the initial states satisfy the claimed invariant, then the only possible order equivalence is the identity. We begin this sequence with the order equivalences we already know to exist from the discussion above, viz. the constant-input/constant-output case: in this case, though, we need only confirm that output invariance is indeed preserved by valid order equivalences. Throughout the rest of this section, we will use the following notation for the derivative of a function; this will eliminate any confusion between orders of differentiation and exponents. ??? y(t) , ?? ?t? y(t) Table 5.1: Special notation for derivatives. Lemma 3 (Constant Input/Constant Output). Let x0,1 and x0,2 be output invariant states from an LTI system; also let yi be the constant output trajectory and xi be the state trajectory obtained from initial condition xi,0 and constant input u (where i = 1, 2). Then for any order equivalence ? : [0, t1]? [0, t2], it is the case that x1(t) and x2(?(t)) are output invariant for all t ? [0, t1]. Proof. We first note that since the outputs y1 and y2 are constant on [0, t1] and [0, t2], respectively, all of their derivatives are zero on those intervals. 89 Using this fact on the first derivative of the outputs yields: y?1(t) = Cx?1(t) = 0 = Cx?2(?)|?=?(t) = y?2(?)|?=?(t). (5.18) But filling in the values of the derivatives according to the state equation (5.4), we get: CAx1(t) + CBu = 0 = CAx2(?(t)) + CBu (5.19) which by linearity, implies that: CA(x1(t)? x2(?(t))) = 0. (5.20) A similar argument for the kth derivatives leads to an equation like the preceding, only with the kth power of A. Hence, CAk(x1(t)? x2(?(t))) = 0 (5.21) for all k ? 1. On the other hand, we have assumed that ? is an order equivalence, so by necessity y1(t) = y2(?(t)) and C(x1(t) ? x2(?(t))) = 0. This shows the required property of the difference x1(t)? x2(?(t)). This certainly suggests that we have chosen a reasonable invariant! But of course that prescience will be even more clear after we consider the case when we allow the outputs to be non-constant (and the inputs to be constant or not): in such a case, the output invariance will lead to the claimed unique order equivalence. Before we take up the proof of our claim for this case, we make one important comment about order equivalences. In particular, given the variation of constants 90 formula, (5.5), two order equivalent LTI trajectories (u1, y1, x1) and (u2, y2, x2) can also be specified in terms of (u2, y2, x2), the initial condition x0,1 and an order equivalence function, ?. That is given a trajectory (u2, y2, x2), an initial condition x0,1 and an order equivalence, ?, we have the following alternate specification of the LTI trajectory (u1, y1, x1): ? t x1(t) = e Atx0,1 + e A(t??)Bu2(?(?))d?. (5.22) 0 Of course an x1 specified in this way need not be analytic, since we have not con- strained the choice of ? in any way that ensures this; indeed the function u2?? might not even be piece-wise analytic and hence inadmissible. However, in the trivial por- tions of the subsequent proof, we will be able to easily conclude that ? ? and hence u2 ? ? and y2 are analytic; in the rest, analyticity of ? will be one of the crucial implications of (A3). At any rate, if there is an order equivalence between two admissible (analytic) trajectories (u1, y1, x1) and (u2, y2, x2), then (5.22) specifies x1 just as well. Given this fact, we proceed with the statement of our claimed result for order equivalences between non-constant-output trajectories, though we first introduce the following small lemma to aid this endeavor. Proposition 8. Let u : [a, b]? R be analytic and non-constant. Then the functional equation u(t) = u(?(t)) has one and only one continuous solution, ? = ?id : t 7? t. Proof. We consider first the case when u? is non-constant on [a, b]. In this case, we observe that u? is also analytic, and hence, has isolated zeros in [a, b]. Thus, 91 we can divide [a, b] into finitely many adjacent, open intervals on which u? is non- zero. But by a generalization of the inverse function theorem, u is invertible in the neighborhood of each point t? within these intervals, and the inverse function is analytic. Hence, ?(t) = u?1(u(t)) = t in the neighborhood of each t? for which u?(t?) 6= 0. But since the solution to this equation is the same for each such t?, and there are only finitely points at which we cannot apply this reasoning (those where u? = 0), we conclude by assumed continuity of ? that ? = ?id : t 7? t on all of [a, b]. The case where u? is constant and zero is excluded by the assumption that u is non-constant, so the only remaining case is when u? is constant and non-zero. But in this case the aforementioned inverse function theorem may be applied in the neighborhood of every point in the interval [a, b], and we obtain the same result as above. Lemma 4 (Non-constant Output/Non-constant Input). Let yi, xi and xi,0 be as in Lemma 3, only with respective inputs ui : [0, ti]? Rm analytic on their domains and with the yi and ui non-constant. If the state trajectories xi and input trajectories ui satisfy (A3) with respect to the outputs yi (in particular at time t = 0), then ? : [0, t1]? [0, t2] is an order equivalence between the aforementioned trajectories if and only if it is the identity order equivalence, ?id : t 7? t. Proof. The essence of this proof will be to ?assemble? the identity order equiva- lence by induction on the time-intervals for which a particular output trajectory?s derivative, y?i, is non-zero (note: this induction is separate from the one claimed above, which assembles analytic segments of a piece-wise analytic function). We 92 can accomplish this by first showing that the only valid order equivalence between the (ui, yi, xi) in some neighborhood of t = 0 is the identity order equivalence, ?id : t 7? t. If we do this for both the case when the y?i(0) = 0 and the case when the y?i(0) 6= 0, then we are essentially done: since the identity order equivalence preserves output-invariance of the states, we can ?propagate? the claimed identity order equiv- alence from t = 0 (for as long as it?s valid) to get two new output-invariant states at a later time. But time invariance allows us to recycle our claims for time t = 0 at this new time, so we can again claim necessity and uniqueness of the identity order equivalence for some extended interval of time. If the y?i(0) were zero, then because non-constant analytic functions have isolated-zeros1, this ?propagation? can be used to transfer the system state to one where the output derivatives are non-zero; of course, if the original states had non-zero output derivatives, then continuity allows us to assert that this ?propagation? must be extendable at least until the first zero of the output derivative(s). Together, these two observations allow us to claim by induction that these entire analytic segments of the trajectories have between them a unique order equivalence, the identity order equivalence. We proceed with the proof as outlined above, and first consider the case where y1(0) = y2(?(0)) 6= 0. From this, note that any order equivalence ? is necessarily analytic in some neighborhood of t = 0: an order equivalence by definition satisfies y1(t) = y2(?(t)), which can be solved for ?(t) as ?(t) = g(y1(t)) for some analytic function g by a generalization of the inverse function theorem for analytic functions 1The case where the derivative is constant (but still non-zero by stipulation) is an obvious special case. We omit it from this top-level discussion for clarity. 93 y1 and y2 [34] (this of course requires the non-zero derivative y?2(0)). Thus, we need only search for analytic order equivalences in the neighborhood of t = 0, so our strategy will be to treat the analytic order equivalence function ? as a ?variable? in an equation y1(t) = y2(?(t)) obtained by assuming u1 = u2 ? ? ? that is ? satisfies the requirement of an order equivalence between the inputs by construction (and with the initial conditions as described in the statement of the lemma); see also the prefatory comment preceding this lemma. If ? = ?id is the only possible solution to the aforementioned equation, then we conclude that when (u1, y1, x1) and (u2, y2, x2) are order equivalent, the order equivalence between them is necessarily ?id. This description is thus one of establishing ? = ?id as a necessary condition for order equivalence under the conditions of the lemma. Since ? is analytic near t = 0 in this case, we can establish it uniquely by characterizing all of its derivatives at time t = 0, near which it necessarily agrees with its power series expansion about the same point, t = 0. Moreover, analyticity of ? implies y2 ? ? is also analytic, so the equality y1 = y2 ? ? implies equality of coefficients in the power series expansions of y1 and y2?? (about t = 0 is the natural choice). Of course this means we are considering ? ??? d y1(0) = y2(?(0)) (5.23) dt? for all ? ? N (the normalization 1/?! is common to both, and hence may be omitted). Since we?re working with linear dynamics, (5.4), and we have assumed that u1 = 94 u2 ? ?, we can further note that ???1??? ?j? y1(t) = CA ?x ??1?j1(t) + CA Bu1(t) ?j=0??1 dj = CA?x (t) + CA??1?j1 B (u2 ? ?)(t). (5.24) dtj j=0 On the other hand, by Faa? di Bruno?s formula [34], we note that d? y2(?(t)) dt? ? ( ) ( ) ( ???k k )k?! ??? ??(t) 1 ??(t) 2 ?(t) ? = y2(?(t)) . . . (5.25) k1!k2! . . . k?! 1! 2! ?! k1+2k2+...?k?=? where the variable ? = k1 +k2 + ? ? ?+k?, and the sum is over the variables k1, . . . , k? subject to the indicated constraint (we will use this formula several times in the sequel). We thus create a necessary conditions for an analytic order equivalence ? by simply substituting (5.24) and (5.25) into (5.23) for ? = 1, 2, . . . (in that order), and setting t = 0 to get the relevant power series coefficients; naturally, we will apply Faa? di Bruno?s formula as needed to the derivatives of u2 ? ? in (5.24). Considering (5.23) first for ? = 1 we obtain simply ( ) CAx1,0 + CBu2(?(0)) = CAx2,0 + CBu2(?(0)) ? ??(0). (5.26) But as we have assumed that x1,0 and x2,0 are output invariant, we note that x1,0 = x2,0 + ? for some ? ? N (O); considering this fact in the above, we obtain ( ) ( ) (CAx2,0 + CBu2(?(0))) ? (1? ??(0)) + CA? ? ??(0) = 0 =? CAx2,0 + CBu2(?(0)) ? (1? ??(0)) = 0 (5.27) since ? ? N (O) and hence CA? = 0. Of course, we have assumed that y2(?(0)) = CAx2,0 +CBu2(?(0)) 6= 0, so already we see that ??(0) = 1 is the only possible choice 95 for ??(0) under the assumptions that we have made. Now we proceed inductively through the remaining values of ?. We take ? = 2 as the base case, and claim that given (5.27), the only possible solution for ??(0) is ??(0) = 0; then as an induction ?j? ??? step, we claim that ?j ? ?? 1.? (0) = 0 implies that ?(0) = 0. This will identify ? as ?id : t?7 t in some neighborhood of t = 0. The base case can be established by considering the relevant forms of (5.24) and (5.25) and taking into account the unique solution ??(0) = 1: CA2x1,0 + CABu2(?(0)) + CBu?2(?(0))??(0) = y?2(?(0))?? 2(0) + y?2(?(0))??(0) =? CA2x1,0 + CABu2(?(0)) + CBu?2(?(0)) = y?2(?(0)) + y?2(?(0))??(0) =? CA2x1,0 + CABu2(?(0)) + CBu?2(?(0)) = CA2x2,0 + CABu2(?(0)) + CBu?2(?(0)) + y?2(?(0))??(0) (5.28) Noting again that x1,0 = x2,0 + ? for some ? ? N (O) we see immediately that the last equation above simplifies to y?2(?(0))??(0) = 0. (5.29) But of course y?2(?(0)) 6= 0 by assumption, so the only solution for ??(0) is ??(0) = 0, and this establishes the base case. The induction step can be established by careful book-keeping, and using Faa? j di Bruno?s formula to expand d j (u2 ? ?) in (5.24); of course the assumption thatdt higher derivatives of ? are zero makes this considerably easier to do. To start, we take ? to be fixed and the induction hypothesis to be true. By Faa? di Bruno?s 96 formula, we expand the final term in (5.24) as promised by noting that dj (u2 ? ?)(t) dtj ? ( ) ?j?k ( )k ( )kj! ??? ??(t) 1 ??(t) 2 ?(t) j = u2(?(t)) . . . k1!k2! . . . kj! 1! 2! j! k1+2k2+...jkj=j ?j? ?j? = u2(?(t)) ?? j(t) = u2(?(t)) (5.30) where ? = k1 + k2 + ? ? ? + kj as before; this clearly follows from the induction ... ?j? assumption that ??(0) = ? (0) = ? ? ? = ? (0) = 0 for j ? ? ? 1 and ??(0) = 1. On the other hand, applying the induction assumption to (5.25), we see that the only (possibly) nonzero terms occur when the indexes k2 = k3 = ? ? ? = k??1 = 0. In this case there are only two solutions to the constraint equation, which becomes k1 + ?k? = ?: namely, k1 = ?, k? = 0 and k1 = 0, k? = 1. Thus, we can simplify (5.25) to be simply d? ??? ??? y2(?(t)) = y2(?(0))?? ?(0) + y? ? 2 (?(0))? (0) dt ??? ??? = y2(?(0)) + y?2(?(0))? (0). (5.31) But when we consider (5.23) under the conclusions derived above, we get ???1 ?j? ??? ??? CA?x ??1?j1,0 + CA Bu2(?(0)) = y2(?(0)) + y?2(?(0))? (0). (5.32) j=0 However, as before x1,0 = x2,0 + ? for ? ? N (O), so that we observe in the preceding that the left-hand side cancels exactly the first term on the right-hand side, and 97 that leaves the following simple equation: ??? y?2(?(0))? (0) = 0. (5.33) ??? Of course this equation has as a unique solution ? (0) = 0, since we have assumed that y?2(?(0)) 6= 0. This completes the induction and this portion of the proof, so we conclude that when y?1(0) = y?2(?(0)) =6 0, the only possible order equivalence between the specified trajectories is ? = ?id. Now we proceed with the case when y?1(0) = y?2(?(0)) = 0. First of all, we can no longer apply the (more general) inverse function theorem to the equation y1(t) = y2(?(t)) in order to confine our attention to only analytic functions ?. However, we have designed (A3) in such a way as to ensure that the only valid inputs allow us to draw a similar conclusion. We have two cases now: either the ([x1,0], u1(0)) = ([x2,0], u2(?(0))) are in the domain of F0, or else they are in the domain of F=6 0. In the former case, by (A3), we see that u?1 = u?2(?(0)) =6 0, so we may directly apply the aforementioned inverse function theorem to conclude we should restrict our attention to analytic order equivalences ?. The latter case is more complicated, since (A3) allows a single, albeit unique input u for which u?(0) = 0. Clearly, then, when we consider any possible order equivalence between allowable inputs we have a number of different scenarios. In the most obvious case, u?1(0) and u?2(?(0)) are both nonzero, and earlier arguments show that ? must be analytic in a neighborhood of t = 0. Another scenario has u?1(0) = 0 and u?2(?(0)) 6= 0 or visa versa. But in this case, we can clearly choose either ? or ??1 to be analytic in a neighborhood of t = 0 according to the inverse function theorem, and we can 98 simply swap the order of the initial conditions in the sequel accordingly. In the final case, both u?1(0) = 0 and u?2(?(0)) = 0. But by (A3) this means that u1 = u2, and Proposition 8 ensures that the only possible order equivalence between them is ?id, hence analytic. Having established that we may confine ourselves to analytic order equivalence functions we proceed largely as above: we will use exactly versions of (5.23) to solve for derivatives of the order equivalence function, ?, only the equations will (unsurprisingly) look somewhat different. Unfortunately, the assumed situation that y?1(0) = CA[x1,0] + CBu1(0) = y?2(?(0)) = CA[x2,0] + CBu2(?(0)) = 0 (5.34) means that we cannot begin an inductive proof in the same way as above. In particular, adapted to the current setting, (5.27) does not have a unique solution! In fact, 0?(1???(0)) = 0 is no constraint at all on ??(0)! So we have to use some of the other consequences of (A3) to first establish that ??(0) = 1 is the unique choice for our analytic order equivalence. In the case that ([x1,0], u1(0)) = ([x2,0], u2(?(0))) ? dom(F0), the stipulation of (A3) that u1(0) = u2(?(0)) ensures (by the chain rule) that ??(0) = 1. On the other hand, if ([x1,0], u1(0)) = ([x2,0], u2(?(0))) ? dom(F 6=0), then either u1(0) = u2(?(0)) = 0 and u1 = u2, in which case we have already argued that ??(0) = 1, or else one of the ui has non-zero derivative at t = 0, say u?2(?(0)) =6 0 without loss of generality. But in this case, we can consider using (5.23) with ? = 2 in an attempt to create an equation that has ??(0) = 1 as a unique solution; of course (A3) has just the right restrictions to make this possible (although those restrictions are clearly not the only ones to achieve this objective!). To wit, after 99 expanding (5.23) with ? = 2 using (5.24), the first line of (5.30) and (5.25), we get CA2x ?(1,0 + CABu2(?(0)) + CBu?2(?(0))?(0) ) ( ) = CA2( x2,0 + CABu2(?(0)) + CBu?2(?(0)))?? 2(0) + CAx2,0 + CBu2(?(0)) ??(0) = CA2x2,0 + CABu2(?(0)) + CBu?2(?(0)) ?? 2(0) (5.35) since by assumption, CAx2,0+CBu2(?(0)) = 0. If we let v = CA 2x2,0+CABu2(?(0)) and w = CBu?2(?(0)), then this gives us the following quadratic equation in ??(0): (v + w)??2(0)? w??(0)? v = 0. (5.36) Note that since we are working with ([x2,0], u2(?(0))) ? dom(F 6=0), we can be assured that v 6= 0. Thus, if v + w = 0, then the above reduces to a linear equation in ??(0) that has a unique solution ??(0) = 1; otherwise, the above has as solutions the following: ? [[v]]k??(0) = 1 or ??(0) = . (5.37) [[v]]k + [[w]]k If u?2(?(0)) = 0, then clearly the only solution that yields an increasing order equiv- alence ? i.e. ??(0) > 0 ? is ??(0) = 1; otherwise, (A3) ensures that ? [[v]]k is [[v]]k+[[w]]k negative for some k, hence ??(0) = 1 is the only solution to yield an increasing order equivalence. Thus, under the conditions of the lemma and the assumptions we have made, we conclude that ??(0) = 1. Since we used equation (5.23) with ? = 2 to establish that ??(0) = 1, it makes ?j? sense to start an induction to establish ? (0) = 0, j = 2, 3, . . . with ? = 3. This difference aside, we proceed largely as before: the induction step will be to assume ?j? ?j? that ? (0) = 0 for all j < ?? 1 and show that this implies ? (0) = 0 for all j < ?, or 100 ??? 1? equivalently, that it implies ? (0) = 0. Starting with the base case of ? = 3, we see that (5.23) and ??(0) = 1 together with the usual substitutions gives us ( ) 3y?2(?(0))? CBu?2(?(0)) ??(0) = 0. (5.38) Of course (A3) indicates that the above will have a unique, non-zero coefficient of ??(0) both when u?2(?(0)) = 0 and otherwise: we simply consider all of the cases described in (A3), starting with the case when ([x2,0], u2(?(0)) ? dom(F0) and then both proscribed sub-cases when ([x2,0], u2(?(0)) ? dom(F 6=0). In the domain of F0, u?2(?(0)) =6 0, so of course there will necessarily be a component of (5.38) with a non-zero coefficient for ??(0). In the domain of F 6=0, the situation where u?2(?(0)) = 0 poses no problem at all since the coefficient for ??(0) reduces to simply v, which is non-zero by assumption. In the case that u?2(?(0)) = 0, (A3) contains the explicit requirement that there is a component k for which 3[[y?2(?(0))]]k? [[CBu?2(?(0))]]k 6= 0, so again we conclude that the only possible solution for ??(0) is 0. This completes the proof of the base case. ?j? The induction step now proceeds as suggested before: assume that ? (0) = 0 ?j? for all j < ?? 1 and show that this implies ? (0) = 0 for all j < ?, or equivalently, ??? 1? that it implies ? (0) = 0. The crucial difference here relative the prior induction proof is the offset of the indexes: whereas before we were specifying the ?th derivative of ? at index ?, here we will be specifying the ? ? 1th derivative of ? at index ?. At index ?, then, we have to adjust (5.30) at j = ? ? 1 to account for the weaker ??? 2? induction hypothesis, which only asserts up to ? (0) = 0. In this situation, we have two solutions to the constraint equation: k1 = ?? 1 and k??1 = 0; and k1 = 0 101 and k??1 = 1, so that d??1 ? ??? 1? ??? 1? ? (u2 ?)(0) = u2 (?(0))?? ??1(0) + u?2(?(0)) ? (0) (5.39) dt? 1 Recall that we only have to consider a maximum index of ?? 1 because the highest derivative of u2 ? ? lags behind the derivative of highest derivative of y2 ? ? by one; j ?j? of course d j (u2 ? ?)(0) = u2(?(t)) for all j < ? ? 1 by the same arguments above.dt ? In expanding d ?y2(?(t)) as in (5.25), we also see fewer terms disappear due to ourdt ... ??? 2? induction assumption. Indeed, we see that since only ??(0) = ? (0) = . . . = ? (0) = 0, we have to consider different solutions of the constraint equation: i.e. we should allow k1, k??1 and k? to be non-zero. This leads to exactly three solutions to the constraint equation: k1 = 0, k??1 = 0 and k? = 0; k1 = 1, k??1 = 1 and k? = 0; and k1 = 0, k??1 = 0 and k? = ?. Thus, we simplify (5.23) to be ???1 ?j? ??? 1? CA?x1,0 + CA ??1?jBu2(?(0))?? j(t) + CBu?2(?(0)) ? (0) j=0 ??? ??? 1? ??? = y?2(?(0))? (0) + ?y?2(?(0)) ? (0) + y2(?(0))?? ?(0). (5.40) But using ??(0) = 1 again, noting that y?2(?(0)) = 0, and using the equality x1,0 = x2,0 + ?, we can reduce the above to simply: ( )??? 1? ?y?2(?(0))? CBu?2(?(0)) ? (0) = 0. (5.41) Finally, then, (A3) tells us that the preceding has a unique solution whenever ? ? 3, so this completes our proof of the induction step. Thus, we conclude that ? = ?id in a neighborhood of t = 0 when y?1(0) = y?2(?(0)) = 0, at least when (A3) is satisfied. The rest of the proof follows straightforwardly from the arguments laid out in the introductory paragraphs. 102 Now that we have completed proofs for both the constant-input/constant- output case and the non-constant-output case, we can consider the remaining cases: that is when the output is constant but the input is non-constant and when the input is constant but the output in non-constant. Lemma 5 (Constant Output/Non-constant Input). Let x0,1 and x0,2 be output in- variant states from an LTI system; also let y1 be a constant output associated with state trajectory x1, initial condition x0,1 and non-constant input u1. Under assump- tion (A2), u1 is the unique input that generates the output y1 from any initial condition that is output invariant with respect to x0,1; hence, any order equivalence ? : [0, t1] ? [0, t2] to a trajectory (u2, y2, x2) (from initial condition x0,2) is neces- sarily the identity order equivalence. Proof. We begin by considering the uniqueness assertion of the lemma. First, note that by constancy of the output y1, we can conclude that y?1(t) = Cx?1(t) = 0 and d [ ] y?1(t) = Cx?1(t) = C Ax1(t) +Bu1(t) dt = CA2x1(t) + CABu1(t) + CBu?1(t) = 0. (5.42) Of course the latter allows us to write down a linear ODE in u1: CBu?1(t) = ?CA2x1(t)? CABu1(t). (5.43) Here we see the reason for assumption (A2): under that assumption, this equation can effectively be solved uniquely for u?1 using a pseudo-inverse; for simplicity, we simply call this operator (CB)?1. 103 Now, since the trajectory x1 is obtained from the input u1 driving our LTI system (from initial condition x0,1), we can augment the dynamics (as before) to obtai?n a?self-c?ontained ODE for u1 and x1:? ???u? ??? ????(CB)?11 CA2x1(t)? (CB)?1CABu1(t)= ??? x?1 ? Ax1(t) +Bu1(t)? ?? ? ? ????(CB)?1CAB ?(CB)?1CA2?= ?????u1(t)??? ?, A???u1(t)??? . (5.44) B A x1(t) x1(t) Because it?s a linear ODE, we know that (5.44) has a unique solution for each particular initial condition. However, to get the claimed uniqueness result, we have to show that it produces the same solution ? at least for u1 ? for any two output invariant initial conditions (that the initial condition for the variable u1 must be the same is the only relevant situation because of the conditions of an order equivalence). Using the variation of constants formula (5.5), we can write the solution to the (autonomous) linear ODE (5.44) in terms of a matrix exponential in the matrix A?: ?? ???u1(t)? ? ? ?? ???u1(0)??? ?? ? ? ? ?? ??ti ???u1(0)?= eA?t = ? A?i ????? . (5.45)i! x1(t) x i=00,1 x0,1 So we can effectively verify that x0,1 and x0,2 lead to the same solution u1 by checking that multiplying by successive powers of A? preserves equality of the u1 components and output invariance o?f the ?x1 comp?onents?. That is for? ? ??? (k,i)?? ?? ?? ?? (k?1,i)u1 ? ?u1(0)? u, k 1 ?A? = A?? ?? (5.46) (k,i) (k?1,i) x1 x0,i x1 (k,1) (k,2) (k,1) (k,2) we should verify that for all k ? N, u1 = u1 and the ?states? x1 and x1 104 are output invariant. This is, of course, best accomplished by induction on the exponent, k, with the base case given by the assumed initial conditions. Thus, (k?1,1) (k?1,1) (k?1,2) (k?1,2) suppose that [u1 ;x1 ] and [u1 ;x1 ] satisfy the claimed properties, and observe that (k,1) ? (k,2)u1 u1 = ( ) ( ) ? (CB)?1 (k?1,1) (k?1,2) (k?1,1) (k?1,2)CAB u1 ? u1 ? (CB)?1CA2 x1 ? x1 = 0 (5.47) and ( ) ( ) (k,1) ? (k,2) (k?1,1) ? (k?1,2) (k?1,1)x1 x1 = B(u1 u1 ) + A x1 ? (k?1,2) x1 (k?1,1) ? (k?1,2)= A x1 x1 . (5.48) But in the latter case, we note that the null space of O is A-invariant, so (5.48) (k,1) (k,2) implies that in fact, x1 and x1 are output invariant as well. Consequently, (5.44) results in a unique solution for u1, given any two x1 initial conditions that are output invariant. However, the preceding gives us directly the claim for the order equivalence ?. For if there were a non-trival order equivalence, then there would in fact be two distinct input functions that yield the same constant output (from output invariant initial conditions x0,1 and x0,2): namely u1 6= u2 (with u1 = u2 ? ? for ? 6= ?id)! Lemma 6 (Non-constant Output/Constant Input). Let x0,1 and x0,2 be output in- variant states from an LTI system; also let y1 be the non-constant output associated with state trajectory x1, initial condition x0,1 and constant input u1. Any input that 105 is order equivalent to u1 generates the output y1 from any initial condition that is output invariant with respect to x0,1; hence, any order equivalence ? : [0, t1]? [0, t2] to a trajectory (u2, y2, x2) (from initial condition x0,2) is necessarily the identity order equivalence. Proof. Since we?re considering inputs that have a singleton codomain, it is clear that the system outputs will necessarily be the same for all order-equivalent inputs, given output-invariant initial conditions. The conclusion about uniqueness of the identity order equivalence then follows from the non-constancy of the output and Proposition 8. 5.4.3 LTI Systems and Order-equivalence Non-determinism: Piece- wise Analytic Inputs and ?Global? Non-determinism Structure In the previous subsection, we characterized order equivalences within the four different classes of input/output pairs that are possible with a purely analytic input. In this subsection, we will concatenate those ?local? order equivalences into ?global? order equivalences: that is we will consider which order equivalences are possible when we string together purely analytic inputs in order to make piecewise analytic inputs. This allows us characterize order equivalences between trajectories that can reach all of the nodes in a GST constructed according to Section 5.3. Importantly, the assumptions of Section 5.3 allowed us to show that in all such cases but one ? the constant-input/constant-output case ? the only possible order equivalence is the identity order equivalence, ?id : t 7? t. Of course the identity order 106 equivalence preserves output invariance of trajectory states, so given Lemma 3, we conclude that all order equivalent trajectories started from output invariant states lead to output invariant states; hence, output invariance is an invariant with respect order equivalence along analytic segments, at least under the assumptions we have made (i.e. (A1) - (A3)). Thus, given that the lemmas in the previous subsection are stated in terms of output invariant initial conditions, we have done essentially all of the hard work in characterizing such order equivalences: we need only observe that by construction, all trajectories emanating from a single GST node start in a single, specified initial condition, which is of course order equivalent to itself. Then we may proceed inductively along analytic segments, using the fact that output invariance is preserved in the terminal states of each. This concept is formalized in the following theorem; see also Fig. 5.2. Theorem 11 (The Character of Order Equivalences in LTI Systems). Let p = (t, (u, y, x)|t) ? Gx0(A,B,C) be a fixed node, and suppose that q1 = (t1, (u1, y1, x1)|t1) and q2 = (t2, (u2, y2, x2)|t2) are nodes for which (p, q1] and (p, q2] are order equivalent trajectories (from p). Then there exists an order equivalence ? : [t, t1]? [t, t2] such that for all t? ? [t, t1]: ? if there exists an  > 0 and an interval [t?, t? + ) over which both u1 is analytic and either u1 or y1 is non-constant, then ?(? ?)? ?(? ??) = ? ?? ? ?? for all ? ?, ? ?? ? [t?, t? + ). Proof. The proof proceeds along the lines suggested in the preceding paragraph. The input u1 is piecewise analytic, so divide it into analytic segments over a sequence of 107 adjacent time intervals Ji = [?i, ?i+1] with ?0 = t. Then proceed by induction along the Ji. The first analytic ?segment? of input is either constant or non-constant, and leads to either a constant or non-constant output. In the case where either u1|J0 or y1|J0 are non-constant, then we can appeal to Lemmas Lemma 4, Lemma 5 or Lemma 6 as necessary to show that the only possible order equivalence between (u1|J0 , y1|J0) and (u2, y2) is the identity order equivalence; no matter what, then, at the end of the segment J0, the order equivalence pairs output invariant states from x1(?1) and x2(?(?1)). In the case where u1|J0 or y1|J0 are both constant, then the order equivalence may be selected arbitrarily as a monotonic bijection that spans the segments; by Lemma 3, though, the resultant states are still output invariant. Since x1(?1) and x2(?(?1)) are necessarily output invariant, we may use time- invariance of the underlying dynamics to repeat the above analysis on the next interval, J1, using x1(?1) and x2(?(?1)) as ?initial conditions? at ?time 0?. Given this fact, we may clearly proceed inductively through the rest of the intervals Ji using the same type of argument, and hence, we can assert the claim of the theorem for the entire trajectories (u1, y1, x1) and (u2, y2, x2) started from the specified time t. The claim of Theorem 11 is illustrated in Fig. 5.2 using cartoon trajectories: during non-constant trajectories, we see that all order equivalences preserve time differences through the (appropriately shifted) identity order equivalence, whereas during constant-input/constant-output trajectories, the choice of order equivalence 108 y1(t) u1(t) 0 t1 y1, u1 constant ? : [0, t1] ? ?(t?)? ?(t??) = t? ? t?? ?(t?)? ?(t??) =6 t? ? t?? ?(t?)? ?(t??) = t? ? t?? [0, t2] y2(t) u2(t) 0 t2 y2, u2 constant Figure 5.2: Cartoon of order equivalent LTI trajectories (single input/single output). 109 is essentially unconstrained. The fact that such constant-input/constant-output tra- jectories may appear in the middle of the response to an arbitrary piecewise analytic input means that even trajectories that have known starting and ending states may have different order equivalences between them. However, the character of these or- der equivalences is entirely determined by (the arbitrariness of) order equivalences along the constant-input/constant-output sub-segments of the trajectory. Indeed, given two order-equivalent trajectories with at least one such sub-segment, there are infinitely many ways to create order equivalences between them, each one of which is a different function from one trajectory to the other; on the other hand, one can achieve any particular one of these order equivalences by merely composing it with another order equivalence. This foreshadows in part the relevance of consid- ering equivalence classes of modal executions that we have used as a foundation for GHML: recall Definition 38 and Definition 40. Despite seriously constraining the potential order equivalences between LTI- system trajectories, Theorem 11 still seems to permit a hopelessly intractable mess of trajectories that are comparable by order equivalence. There is, however, one feature of LTI systems/behaviors that we have given scant attention to as yet: these systems are, in their natural, timed context, entirely deterministic. Thus, when we construct a GST from an LTI system with a single, unambiguous initial condition, the problem is essentially reduced to the consideration of order equivalences between a trajectory and itself; given the above comments, this problem is suddenly a lot more tractable! In fact, this observation forms a useful starting point from which to begin describing the surrogate KSs that result from the LTI-derived GSTs: that 110 is the subject of the next section. 5.5 Modal Logic and Order-equivalence Induced Nondeterminism In Section 5.3, we considered an LTI system with carefully specified restrictions on its admissible inputs, and those restrictions allowed us to precisely characterize the nature of order equivalences between LTI system trajectories in Section 5.4; see Theorem 11 in particular. Given the nature of weak bisimulation and the related definition of GHML in terms of equivalence classes of functions over a domain of modalities (modulo order-equivalence, essentially), we now have the necessary pre- requisites to describe the structure of a surrogate KS, GFx (A,B,C), that results0 from an LTI-derived GST, GFx (A,B,C). Hence, in this section, we can provide a0 treatment of VHHM classes and their relationship LTI-system models as GSTs. Throughout this section, we will work with the natural domain of modalities for LTI systems: for a total order, we will use the real number line with the usual ordering, (I,I) := (R,?R), and for a set of labels, we will use pairs of (instanta- neous) inputs and outputs, L := Rm ?R`. It is clear then that this choice captures any set of GSTs derived from a common LTI system; the use of (R,?R) also means that modal executions share an obviously special relationship with trajectories of the underlying LTI systems. In general, then, we will consider a set of GSTs, U , each element of which is comprised of a subset of behaviors from some GFx (A,B,C); that0 is we may consider any set of different control ?programs? executed on (A,B,C) starting from some x0, so long as they all comply with (A1)-(A3) (under a common 111 F). It is in this context that the following results will hold. 5.5.1 The Structure of Nondeterminism in LTI-derived Surrogate KSs We begin by revisiting Example 2 (see also Fig. 5.1), which was meant to serve in part as motivation for our current undertaking. Another way of framing the important lesson of that example is as follows: when a GST contains a trajectory that is order equivalent to a prefix of itself, that GST will have nondeterminism in its surrogate KS; for Example 2, this nondeterminism is illustrated in Fig. 5.1. In the succeeding paragraphs of Section 5.4, we argued that constant-input/constant- output trajectories from an LTI system exhibit exactly the same kind of property: if both input and output are constant for some interval of time, then in essence, trajectories over sub-intervals are indistinguishable by order equivalence! This is straightforwardly reflected in terms of modal executions: after all, a modal execution is really nothing more than a ?trajectory? over a domain of modalities, which can itself be seen as analogous to a linear GST (albeit without any notion of root); the semantics of GHML then are about matching such modal executions with GST trajectories by order equivalence. What is perhaps not quite as straightforward is how Theorem 11 (using (A1) - (A3)) will affect the structure of an LTI-derived GST?s surrogate KS, GFx (A,B,C). This structure is described in the following0 theorem, the main result of this subsection. Theorem 12 (The Nondeterminism Structure of LTI-derived Surrogate KSs). Let 112 GFx (A,B,C) be as in Definition 48, and let G F x (A,B,C) be the associated surrogate0 0 KS over the domain of modalities (I,I) := (R,? mR) and set of labels L := R ?R`. Furthermore, let p1 = (t1, (u1, y1, x1)|t1) and p2 = (t2, (u2, y2, x2)|t2) be two distinct, non-root nodes in GFx (and hence, also states in the surrogate KS). Then, if there0 is a modal execution, |E| such that (p0, p1] and (p0, p2] are order equivalent to |E|, then: ? there exists a common subinterval [a, b] ? [0, t1] and [a, b] ? [0, t2] on which both (u1, y1) and (u2, y2) are constant and equal; and ? there exists a time ? ? [a, b] such that (u1, y1, x1)|? = (u2, y2, x2)|? , and in particular, x1(?) = x2(?) so that p1 and p2 share a common non-root ancestor. Proof. This is more or less a consequence of Theorem 11 and the fact that we are constructing GSTs from deterministic executions of an LTI system. We begin by noting that two trajectories in GFx that are order equivalent to a0 common |E|must necessarily be order equivalent to each other ? simply compose the (invertible) order equivalences as needed. Hence, Theorem 11 applies, and we know the nature of this order equivalence ? and hence, how these trajectories ?satisfy? |E| ? simply by the the type of analytic segments comprising (u1, y1) and (u2, y2). If the first analytic segment of (u1, y1) is not constant-input/constant-output, then we know the only possible order equivalence to another trajectory in the tree is the identity: this is because both trajectories start from the same, common initial condition and we are considering deterministic executions by construction. Thus, the first analytic segments of (u1, y1) and (u2, y2) are literally identical: that is 113 they go through the same state trajectory as well. Of course by Theorem 11, this argument applies up to the first non-constant-input/constant-output segment of the trajectory, of which there must be at least one, lest the entire trajectories be identical (this would be impermissible by the assumed distinctness of the trajectory endpoints). This proves both the first claim and the second claim of the theorem. Corollary 1. Let GFx (A,B,C) be as in Definition 48, only created with some subset0 of the behaviors from BFx (A,B,C). Then the conclusions of Theorem 12 still hold.0 Proof. Theorem 12 depends on uniqueness of the identity order equivalence in cer- tain situations and determinism of the underlying LTI system; these properties are retained when considering a subset of the specified set of behaviors. With regard to these results, it is first worth emphasizing the crucial role played by determinism in the underlying behavioral system model: there is determinism not just in the LTI-system model itself but also in the trajectories (or executions) of said system. In particular, we have a priori ruled out the possibility of modeling uncertainty by means of nondeterministic behaviors, wherein the same input leads to multiple behaviors or execution trajectories. That is these models cannot use nondeterministic executions to encode some auxiliary ?hidden? state that affects future branching behavior: only the actual system state and clock time can be used for that purpose. On the one hand, this may be seen as consistent with the deter- minism inherent in the LTI-system model, especially since we have as yet considered known, fixed initial conditions; on the other hand, this is perhaps a severe model- ing constraint for CPSs, where the supplied inputs may conceivably be created or 114 influenced by, say, the execution of some complicated interactive computer program or indeed even another CPS. There are two counterpoints to this latter objection. For one, the abstraction of time ? through weak bisimulation and GHML via order equivalence ? converts a deterministic system into a nondeterministic one that has an inherently interesting structure, especially in terms of modal logic; allowing other types of nondeterminism merely obscures this structure, which is an interesting sub- ject of study in itself. Second, though, we have advertised this as a contribution towards a compositional paradigm of modeling: in that sense, it seems reasonable to start with deterministic models ? especially when those are standard and useful modeling primitives ? and use composition operators to introduce nondeterminism as necessary. This is a limitation to be sure, but it is not inconsistent with a process algebraic approach. In that sense, it also ensures a certain level of formalism with which nondeterminism is introduced. And remember, GSTs as such have abstracted away the notion of real, ?clock? time, so there is actually the hope that composition operators in this domain are easier to describe and far less ?brittle?; see [15,17] for example composition operators. Now, to communicate the intuition behind the claims of Theorem 12, Fig. 5.3 illustrates the essence of the branching structure that it implies for a surrogate KS. Fig. 5.3 thus depicts some cartoon LTI-system trajectories, along with their asso- ciated surrogate KS arcs, which are shown in green. There are three trajectories depicted: the upper and lower trajectories, (u1, y1, x1) and (u2, y2, x2), are shown only for times after their ?branching? point from the central trajectory, (u0, y0, x0); according to Theorem 12, this structure for the picture makes sense, as these tra- 115 jectories must necessarily share their initial non-constant trajectory segments. All three trajectories also share a common segment of non-constant input/output tra- jectory that starts after t0 + ?tb0 , t0 + ?tb1 and t0 + ?tb2 , respectively and which lasts for a (common) duration of t1??tb1?t0; however, these segments of trajectory do not share state trajectories because the branching has forced them to begin at different times relative to each other. Recall that the nodes in our tree are labeled with times as well as states! Indeed, the actual state values along these trajectories may not even be the same, although by previous arguments, order equivalent nodes will necessarily have output invariant states. Nevertheless, the surrogate KS will have identical arcs from the root of the tree to the nodes given by (t?0, (u0, y0, x0)|t? ),0 (t1, (u1, y1, x1)|t1) and (t2, (u2, y2, x2)|t2): these arcs are labeled by |E| , |t ? [0, t?0]?7 (u2(t), y2(t))|. (5.49) This is the constant-input/constant-output nondeterminism that we have claimed! To emphasize this point, Fig. 5.3 also depicts surrogate KS arcs to intermediary nodes of interest: of particular note is the arc over constant portions of the respective trajectories, |EC | , |t ? [t0, t0 + ?tb0 ] 7? (u0(t), y0(t)) = (u0(t0), y0(t0))|. (5.50) In fact, the actual picture of surrogate KS arcs between the nodes connected by |EC | is exactly like the one depicted in Fig. 5.1: this is an essential structure that we will study going forward! Finally, note the different extensions of the system trajectories depicted after times t?0, t1 and t2, respectively: since the respective trajectories lead to different nodes in the GST at these times, permitting subsets of behaviors from 116 y1(t) u1(t) t1 ?tb1 |E| |E2| y0(t) u0(t) 0 t ?0 y, u constant t0 ?tb0 |EC | |E1| |E2| |E| y2(t) u2(t) t2 ?tb2 |E2| |E| Figure 5.3: Cartoon of nondeterministic order-equivalent trajectories. Surrogate KS arcs (in green) pictorially ?span? their associated trajectories; they have labels |E|, |E1|, |EC | and |E2|, which are defined in the text. |EC |-labeled arcs lie entirely in the shaded box. 117 BFx ? as in Corollary 1 ? means that we are allowing GSTs that have possibly0 different behavior after such a branching has occurred. Despite its rather compact statement, then, Theorem 12 somewhat narrowly specifies the branching structure of a surrogate KS GFx (A,B,C). In fact, it can0 be summarized as saying that nondeterminism in GFx (A,B,C) arises only at or0 because of nodes within stretches of constant-input/constant-output. This essential fact creates additional structure in the nondeterminism of the surrogate KS beyond the anticipated weak density and transitivity of Theorem 10. In particular, as a (further) consequence of determinism in the underlying behavioral model, the nodes within a particular segment of constant-input/constant-output occur in a linear order with respect to their associated constant-function modal execution ? a property called right-linearity. This is precisely the structure claimed for the |EC | transitions depicted in Fig. 5.3 and the |E| transitions depicted in Fig. 5.1. The implications of this for modal logic and GHML, particularly with respect to VHHM classes, are significant: not only is this a type of nondeterminism, but it is also a type of ?infinitary? nondeterminism. Thus, we make this the subject of the next subsection. 5.5.2 Quasi-discreteness and VHHM Classes for Weak Dense, Tran- sitive, Right-linear Structures Since we claim that right linearity [36] is induced by the LTI order-equivalence structure over constant-input/constant-output trajectories, we begin this section 118 with a definition of right-linearity, or as it is much more commonly called, weak connectedness [26]. Definition 49 (Right linearity/Weakly connected). A transition relation R ? P?P is said to be right-linear or weakly connected if it satisfies the following first-order property: ? For all s, t, u ? P , sRt ? sRu =? ( tRu ? t=u ? uRt ). (5.51) Furthermore, this property is captured by the schema [37]:  ((A ?A)? B) ? ((B ?B)? A) (5.52) or its equivalent, somewhat more intuitive schema [36]: ?A ? ?B ? ?(A ? ?B) ? ?(A ?B) ? ?(?A ?B). (5.53) (This equivalence holds at least in the case of logics that are also transitive and weakly dense; see the following proposition.) Proposition 9. A transitive, weak-dense normal logic satisfies schema (5.52) if and only if it satisfies schema (5.53). Proof. The forward direction follows straightforwardly from the normal logic schema K. 119 For the reverse direction, simply observe: ?A ? ?B ? ?(A ? ?B) ? ?(A ?B) ? ?(?A ?B) =? ?(A ?B)? ? ((A ? ?B) ? (A ?B) ? (?A ?B)) =?  (?(A ? ?B) ? ?(A ?B) ? ?(?A ?B))? ?(A ?B) =? ?(A ? ?B) ??(A ?B) ??(?A ?B)? ?(A ?B) =? ?(A ? ?B) ??(?A ?B)? ?(A ?B) =?  (?(A ? ?B) ? ?(?A ?B))? ?(A ?B) Now, expanding the argument of the box on the left using propositional distribution of ? over ?, we get the following. =?  ((?A ? ??A) ? (?B ? ??B) ? (?A ? ?B) ? (??A ? ??A))? ?(A ?B). The left-hand side of this expression can be strengthened by distributing the box across the disjunct to get: =? (?A ? ??A) ?(?B ? ??B) ?(?A ? ?B) ?(??A ? ??B) ? ?(A ?B). Now, the (?A ? ?B) on the left is obviously redundant, and by transitivity and weak density, the term (??A ? ??B) is likewise redundant, since: (??A ? ??B) ? ?A ??B ? ?A ??B. By strengthening the remaining disjunct on the left to a conjunction, we can continue 120 simplifying as follows. =?  (?(A ? ?A) ? ?(?B ?B))? ?(A ?B) =? ?(A ? ?A) ??(?B ?B)? ?(A ?B) =? ?(A ? ?A) ??(?B ?B)? ?A ??B =? ??(A ? ?A) ? ??(?B ?B) ??A ??B =? ??(A ? ?A) ??B ? ??(?B ?B) ??A =? (?(A ? ?A)? ?B) ? (?(?B ?B)? ?A) The last of which is clearly equivalent to (5.52) when we allow A and B to span over all formulas. In fact, as a consequence of using a deterministic behavioral model, LTI- derived GST nodes along constant-input/constant-output trajectories are in cor- respondence with real numbers (i.e. R): this means that they actually satisfy a stronger property than weak -connectedness. This property, called connected- ness [26], will of course imply right linearity/weak connectedness, but it will be of some special importance later when we consider VHHM classes. Definition 50 (Connected [26]). A transition relation is connected if it satisfies the following first-order property: ? For all t, u ? P , tRu ? t=u ? uRt . (5.54) Proposition 10. The orderings < and ? are connected relations over the real num- ber line, R, and its open sub-intervals (a, b) ? R. 121 ? ? ? ? ? ? ? . . . ? ? ? ? . . . ? ? . . . ? r1 r? 2 Figure 5.4: A right-linear, weakly dense, transitive example from [19] (note: the shading was altered on the second node from the left). Not shown are ?transitive? ?; ? transitions. Two important nodes are labeled as r1 and r2, respectively. Now, as we did in Section 5.4, we will consider an informative example from [19]. In particular, consider the KS depicted in Fig. 5.4, which is transitive, weakly dense and right-linear with respect to the transition ?. In [19], this KS was in fact (bisimilar to) the surrogate KS of a particular GST; see Example 6 in [19]. How- ever, given the discussion in the previous section, we can also think of this KS as a hypothetical surrogate KS obtained from an LTI-derived GST with a stretch of constant-input/constant-output trajectory : the ? transitions then stand-in for the modal execution of a constant-input/constant-output trajectory. In [19], the impor- tant observation about this KS is as follows: both gray nodes r1 and r2 satisfy the same formulas, yet they are clearly not bisimilar. Hence, this KS cannot belong to any VHHM class of KSs2; moreover, an ?-labeled self-transition may be added to 2There is a slight overstatement in [19]: although Fig. 5.4 definitely meets these criteria, it is not exactly difficult to obtain KSs that don?t belong to any VHHM class. What is special about the KS in Fig. 5.4, though, is that it is an example that is weakly dense, transitive and right-linear. And those particular structures have special importance for surrogate KSs and hence, GSTs. 122 r2 without changing the formulas satisfied by any of the nodes. It turns out that the proof of this latter fact is revealing, and it may be generalized. In particular, though, the ability to add a transition without changing formula satisfaction sug- gests immediately that we are dealing with a node that is not m-saturated. Recall Theorem 2: VHHM classes are obtained by removing transitions from the canonical model (aka the Henkin model) to obtain Henkin-like models, and in particular, then the Henkin model itself identifies the unique m-saturated VHHM class. The observations in the previous paragraph were present in [19] as claimed, but it is natural to ask the question: what is it about the example KS in Fig. 5.4 that makes its node r2 modally un-saturated? On the one hand, consider the infinite set of formulas: { ? = ?1 = ???(???>, ) [ ( )] ?2 = ???(???> ? ??????> , = ??? ???> ? ?1( )) [ ( )] ?3 = ??? ???> ? ??? ???> ? ??????> , = ??? ???> ? ?2 . . .( ) ?k = ??? ???> ? ?k?1 , } . . . . (5.55) Each formula ?k ? ? essentially describes the ability to do an ? transition followed by the possibility of doing k different ? transitions. Clearly, this set of formulas is finitely satisfied by node r2 in Fig. 5.4, but there is no ?-reachable node that satisfies all of these formulas simultaneously. Hence, this KS is most certainly 123 not m-saturated. On the other hand, while the set of formulas, ?, witnesses lack of modal saturation, it doesn?t necessarily give us much of a hint about what transitions and nodes would need to be ?added? to make it m-saturated. Recall that the set of formulas satisfied by r2 is a maximally consistent set, and so corresponds to a node in the canonical model; the same is true of the other nodes. However, the set of formulas satisfied by node r2 ? when considered as a state in the canonical model ? may have ? transitions to other nodes in the canonical model, and indeed it must, since it?s not m-saturated. To get a sense of the additional nodes/transitions required to ?saturate? Fig. 5.4, we drew inspiration from [36] and a first-order transition-relation prop- erty therein called quasi-discreteness. The idea of quasi-discreteness appears there in the context of studying determination ? an essentially ?orthogonal? considera- tion to ours ? but in the context of logics that are likewise transitive, weak dense and right-linear (also serial, although for our purposes, this will not prove relevant). Nevertheless, this property captures an essential feature of the structure in Fig. 5.4, and so we will show that it has a particular relationship to m-saturation, and hence, VHHM classes; in particular, those VHHM classes related LTI-derived GSTs as they are constructed in the preceding. Definition 51 (Quasi-Discreteness [36]). A transition relation R ? P ?P is quasi- discrete if ?s. ?t. [ sRt ? ?u. (sRu =? tRu) ] . (5.56) First, note that quasi-discreteness as it appears in [36] implies seriality (as 124 indicated above): that is every node has at least one R-successor. For our purposes, we will relax this constraint by simply referring to particular nodes as being quasi- discrete rather than an entire KS (thus eliminating the universal quantifier on s in Definition 51); hence, we introduce our own restricted definition as follows. Definition 52 (Quasi-Discrete Node). A KS node, s, is quasi-discrete if it satisfies the predicate for the universally quantified variable s in (5.56). Thus, a node s may be described as quasi-discrete if it has an immediate (?-)successor: that is s has an ? successor, t (possibly t = s) such that every ? successor of s is also an ? successor of t (if t = s then s should have an ? self-loop). This property is more intuitively understood in terms of total orders like < on a subset I ? R: for that relation, a node (or real number), x, is quasi-discrete if the set {y ? I : x < y} has a minimal element (in this example, only isolated points in I are quasi-discrete). Now, the example in Fig. 5.4 can be considered in more or less the same light as the ordering < on R if we think of ? transitions as ?ordering? nodes according to their position in the diagram, with each node coming ?after? all of the nodes to its left. Thus, careful consideration of the node r2 reveals that it is not quasi-discrete in the sense of Definition 52: every one of its ? successors fails to be an ? successor of some other one. In this sense, then, node r2 and its ? successors may be regarded as a more or less fundamental illustration of non-quasi-discreteness, though the KS itself does have one superfluous feature in that regard. The KS in Fig. 5.4 has the further special property that ?between? any two successors of r2, there is always 125 a node that has an ? self-loop and only ? (or ?-prefixed) outgoing and incoming transitions otherwise. In this context, we can revisit the important concept in the proof that r1 and r2 satisfy the same HML formulas: in particular, that r2 with and without an ? self-loop satisfy the same formulas. This concept has an alternate interpretation in terms of quasi-discreteness : the non-quasi-discrete node r2 can be made quasi- discrete without changing the formulas that it satisfies! This is the relationship between quasi-discreteness and m-saturation that we will develop here. Theorem 13. Let K = (S, {R` : ` ? L}) be a KS and let R? be a weakly dense, transitive and right-linear transition relation. Suppose a node w (with ? successors) is not quasi-discrete with respect to ?. Define two variants of K that differ in the ?vicinity? of the node w: ? K1 = (S1, { (1)R` : ` ? L}) is the same as K except that wR(1)? w; and ? K (2) ?2 = (S2, {R` : ` ? L}) has states S2 = S {w?} (disjoint union) and for all ? (2)` L, R` = R` except for the following additions (i) for any ` = ? or ` = ?; `? and any t ? S = S2\{w?}, ? (2)wR`t = w?R` t; (ii) for any t ? S = S2\{w?}, tR?w =? tR(2)? w?; 126 (iii) for any ` ? L and t ? S = S2\{w?}, ? (2)tR`w = tR`;?w?; (2) (iv) wR? w?; (2) (v) w?R? w?. Then in at least one of K1 or K2, the node w satisfies exactly the same formulas as it does in K, and w is quasi-discrete with respect to ? in that KS. Proof. Whether w satisfies the same formulas in K1 or K2 depends on whether or not w has non-?-prefixed transitions emanating from it: if it has no such transitions, then K1 works; otherwise, K2 must be used. The proof in the latter case follows more or less directly from techniques used in the proof of the former, so we consider first the case when w has only ? or ?-prefixed transitions emanating from it. In this first case, our task is to show that for any given formula ? ? ?HML, w |=K ? if and only if w |=K1 ?. However, we?re working in HML and [?; `]A ? [?][`]A by transitivity and weak density, so this problem is actually equivalent to simpler one. In particular, it is enough to show that w |=K [?]? if and only if w |=K1 [?]?, where all of the modalities in ? are of the form [?] or [`] for ` 6= ?; `?. We can further restrict the scope of the claim that needs to be proved by noting that w |=K1 [?]? implies w |=K [?]?. This is by bisimilarity of the corresponding ? successors to w in the models K and K1. Hence, we can further restrict ourselves to formulas [?]? for which w |=K [?]? and w|=K1 [?]?, which taken together, further imply that w|=K1? (again by bisimilarity of the ? successors to w across both models). 127 The strategy of the proof, then, will be to construct filtrations of K and K1 using a common set of formulas that is derived from the (sub-formulas of) formula [?]?, and then to show that both filtrations are bisimilar; this will be enough prove the claim, since bisimilarity preserves HML formulas, and the filtration lemma ? see [26] ? connects the truth of [?]? in the filtrations to its truth in their respective underlying KSs. To construct useful filtrations, we first note that the (necessarily) finite formula ? contains at most finitely many distinct non-[?] modalities, say, {[`1], [`2], . . . , [`N ]}; from this list of modalities, construct the set of formulas ?[?/] := {? , [`1]? , [`2]? , . . . , [`N ]?}. Then we will construct filtrations of K and K1 from the set of formulas ? := Sf([?]?) ? ?[?/] = Sf([?]?) ? {? , [`1]? , [`2]? , . . . , [`N ]?}, (5.57) where Sf([?]?) is the set of sub-formulas of [?]? (to include [?]? itself); clearly, ? is closed under sub-formulas, as is required to construct ? filtrations. Intuitively, the inclusion of the formulas ?[?/] will allow the filtration(s) to distinguish nodes that have different transition structures; we will use this fact in the future to reconcile this proof with others. Note also that w |=K [`1]? ? . . . ? [`N ]? and w |=K1 [`1]? ? . . .?[`N ]?, since in the case under consideration, w has no non-?(-prefixed) outgoing transitions in K (and hence none in K1, either). Now, we will construct ? filtrations of K and K1, although without loss of generality, we can restrict ourselves to the submodels thereof generated by w (see the submodel lemma in [26]); we will largely elide this distinction in our notation from here on. Importantly, though, we will consider in both cases the largest ?-filtrations 128 (1) (1) with respect to R? and R? , which we denote ?R? and ?R , respectively3? ; for all (1) of the other transitions, we will use the smallest ?-filtrations, ?R` and ?R` . Recall the definitions of the largest and smallest filtrations from [26]: ( ) |s| ?R? |t| iff ?B ? ?HML. [?](B ? ? )and s |=K [?]B =? t |=K B (5.58) |s| ?R` |t| iff ?s? ? |s|, t? ? |t|. s?R t?` (5.59) where we have used the common notation |s| to represent the state in the filtration associated with the (? equivalence class of) s. The ? filtrations of K and K1 so constructed will be denoted by FK and FK1, respectively. Henceforth, we will refer to the states from FK using the bare notation |s| and the states from FK1 using the notation |s|1. Now, according to the argument above, we need to establish a bisimulation re- lation between FK and FK1. It should be clear that the only problematic situation occurs in trying to match |w| and |w|1 in a bisimulation relation: this is because, by virtue of bisimilarity, any successor to w in K satisfies the same formulas as its cor- respondent in K1 and vise-versa. Thus, we can easily begin to define a bisimulation relation between FK and FK1 with the following: ( wR?s) =? |s|B|s|1 (5.60) wR?s and sR`t =? |t|B|t|1, (5.61) which together cover every node except w in K (really its model generated by w). 3This notation roughly matches the notation in [26] for the largest/smallest filtration: ? for largest and ? for smallest. This ? has nothing to do with the order equivalences from before. 129 Furthermore, we note that, by construction, ?s 6= w : ( wR s?? wR (1) ?) ( ? s ) (5.62) ? 6 (1)s, t = w : wR s and sR (1)? `t ?? wR? s and sR` t , (5.63) so that B ? as it stands now ? also covers every node except w in K1 (again, really the submodel of K1 generated by w). Now, in considering how to match |w| and |w|1, we have to consider two cases: the first when w |=K ? and the second when w|=K?. The latter is the more difficult case, and its consideration will reveal that simply adding |w|B|w|1 is sufficient to complete a bisimulation relation in the former. The problem with the case w|=K? is evident from the definition of the largest filtration in (5.58): |w|1 will have an ? self-loop in FK1, since w has an ? self-loop in K1; but |w| need not have an ? self-loop in FK since [?]? ? ? and w |=K [?]? (by assumption) yet w|=K?, as is the defining assumption for this case (compare this observation to the case when w |=K ?, as discussed above). This discrepancy in ? self-loops for w means that we have to do a bit more work in order to have a bisimulation relation that includes |w|B|w|1. However, there is an important consequence of the assumption that K is not quasi-discrete at w: since we have chosen a finite set of formulas, ?, for our filtrations, FK has only finitely many states (equivalence classes of states in K), and so at least one equivalence class, say |i|, must contain infinitely many w-successors. However, this means that |i| necessarily has an ? self-loop, and indeed, we claim further that including |i|B|w|1 makes B a bisimulation between FK and FK1. To see this, simply note that for any 130 ? successor to w in K, say u : wR?u, it is the case that u is an ? successor to some element of |i|. This is by the lack of quasi-discreteness at w and the corresponding lack of an immediate successor. Hence, there will be an ? transition between the corresponding states in the filtration, FK: that is |w|?R?|u|. Of course this pattern also takes care of all of the transitions from w because we have assumed that w has only ? or ?-prefixed outgoing transitions. In particular, then, if we wish to show that the ? transition from |w|1 to itself is simulated in FK, then we can use the transition |w|?R?|i| as a witness to this simulation. Thus, for |i| as defined above, we conclude that simply adding |i|B|w|1 to B makes it a bisimulation between FK and FK1 that includes |w|B|w|1; recall that we can assert the existence of such an |i| by the pigeonhole argument above. The preceding paragraph actually completes the proof that when w has only ? or ?-prefixed outgoing transitions, K1 meets the claimed conclusions. Importantly, though, the technique developed above works just as well when w has non-?-prefixed transitions. We can quickly dispense with formulas like [`]?, ` =6 ?, since K2 simply adds extra ? transitions from w: thus, the truth of [`]? is unchanged between K and K2. To treat a formula like [?]?, then, we simply augment ?[?/] with any of the non-? labels that appear in ?: as a result, we can continue matching |w|B|w|2, since the equivalence class of the new node, w?, will be bisimilar to some |i|, where |i| is, as above, an equivalence class that includes infinitely many nodes. Following through on this observation completes the proof in the last remaining case. As we have alluded to with examples, the intended use of Theorem 13 is to 131 show that non-quasi-discreteness can lead to non-m-saturation. This is made precise in the following corollary. Corollary 2. Let K and w be as in Theorem 13. Suppose further that there exists an infinite sequence of formulas ?? = {?k} such that for each k ? N, there exists a wk such that wR?wk and for all u, wkR?u =? u|=K?k. Then K is not modally saturated, and moreover, in the canonical model, Fma(w) has either an ? self-loop or else an ? transition to Fma(w?), which itself has an ? self-loop. Proof. Theorem 13 explicitly defines new models in which w satisfies the same for- mulas, yet has extra transitions. Thus, since the canonical model is m-saturated, those extra transitions must be present as claimed. The assertion that non-quasi-discreteness merely can lead to non-modal sat- uration is a very deliberate distinction: in fact, this is only the consequence when there is, as the statement of Corollary 2 suggests, a ?limit? point effect in the for- mulas satisfied by ? accessible nodes. The following example makes this somewhat more explicit in a way that exploits properties of the real line. In particular, it shows that quasi-discreteness is irrelevant to m-saturation whenever there are only finitely many sets of formulas that are accessible from a non-quasi-discrete node; however, this is clearly a much stronger property than merely asserting that there are only finitely many labels, or even that the non-? structures are themselves bisimilar. Example 3. Consider the totally ordered interval [0, 1] ? R, and let C ? [0, 1] be the Cantor set; see [35]. If for x, y ? [0, 1], we relabel x < y as xR?y, then R? is a transitive, weakly dense and right-linear transition relation as discussed 132 before. Now, consider amending this transition structure with a single ? transition emanating from each element in C that is the endpoint of a ?removed? open interval. Each endpoint in the resulting KS is thus not quasi-discrete (by the density of the real numbers). Nevertheless, the result is m-saturated (with respect to ? transitions) because it is bisimilar to an image finite, quasi-discrete KS [27]. Another way to read Example 3 is that non-quasi-discreteness only reflects on m-saturation when the original model is in some sense irreducible to a quasi-discrete model. The full relationship between quasi-discreteness and m-saturation is yet more complicated. We can?t necessarily ?saturate? a model by affecting only ? transitions, either through the additional of a single ? self-loop ? as in K1 of Theorem 13 ? or through the addition of a node that essentially affects only ? transitions ? as in w? in K2 of Theorem 13. As a consequence, there are models that may not be m-saturated by merely adding ? transitions; an example of this can be derived easily from the KS in Fig. 5.4. Example 4. Given the submodel generate by r2 (from the KS of Fig. 5.4), define a new KS that deletes all ?-self-loop nodes and replaces each ? transition with k transitions ?1, . . . , ?k where k is the position of the originating, counted from the right of the diagram. The preceding example has the property that adding an ? self-loop to r2 ac- tually changes the formulas satisfied by r2! Intuitively, this suggests that to get to m-saturation by affecting only the quasi-discreteness of ? transitions, some addi- 133 tional property is needed: in some sense, then, this is a reflection of the fact that m-saturation is a property that cannot be expressed merely in terms of the ?topo- logical? considerations of quasi-discreteness, even in weakly dense, transitive and right-linear structures. To modally saturate Example 4, for example, there should be a single node with all of the transitions {?k : k ? N}, which is a requirement that clearly extends beyond mere quasi-discreteness and ? transitions. This observation, like the notion of irreducibility suggested above, will be an important consideration with regard to the modal saturation of LTI-derived GSTs: it will be relevant par- ticularly as we try to use trajectory specifications to induce m-saturated GSTs of LTI systems. 5.5.3 Implications for LTI Systems In this section, we finally pull all of the threads together to say something about the relationship between LTI-derived GSTs and VHHM classes of GSTs. On the one hand, we have shown that stretches of constant-input/constant- output trajectory lead to right-linear transition structures with respect to their associated (constant) modal executions. Then, in Section 5.5.2, we connected the m-saturation of such structures to quasi-discreteness. Thus, the preceding sub- sections have established restrictions on how branching choices must be made at the beginning of ? and within ? such constant-input/constant-output segments of trajectory in order to achieve the m-saturation of their constituent nodes. It is thus natural to regard the m-saturation of nodes within a constant-input/constant- 134 output trajectory segment as ?local? to that segment (compare with the terminology of Section 5.4). On the other hand, Theorem 12 states that two distinct nodes that are reachable by order-equivalent trajectories need only have a common ancestor in some portion of constant-input/constant-output trajectory (in the absence of such a segment, there are no order equivalent trajectories that reach them, and their com- mon ancestor is the root). Thus, from the root node of the tree, we have potential nondeterminism during and after each segment of constant-input/constant-output trajectory ? see Fig. 5.3; this nondeterminism ?compounds? further with each seg- ment of constant-input/constant-output trajectory that is included, as each such inclusion allows more and more different ways to achieve order equivalences. This type of nondeterminism is thus a sort of ?global? nondeterminism, and it is an unavoidable consequence of the transitivity of the order-equivalence semantics: no matter which two trajectories are executed in sequence, there is necessarily a third that spans them. Intuitively, global nondeterminism is the more complicated of the two to deal with: indeed, trajectories that long ago diverged from a common prefix trajectory may yet be responsible for identical transitions in the surrogate KS, and thereby be relevant for m-saturation and VHHM classes: as noted above, revisit Fig. 5.3 for an illustration. And this fact is just as true of the root node as it is of any other antecedents of constant-input/constant-output trajectory segments. However, recall the amount of work that went into proving Theorem 12: though its conclusion ulti- mately still allows ?global? nondeterminism such as we have described, the situation would actually be much more complicated without that conclusion of (A1)-(A3). A 135 subtle but invaluable convenience born of those assumptions is that nodes reachable by order-equivalent trajectories may be characterized entirely in terms of output- invariance ( Definition 44). This is actually quite a non-trivial achievement, as it allows us to specify all pertinent branching structures in the surrogate KS purely in terms of (clock) time and output-invariance classes of states ! In light of this, the most straightforward way to control global nondetermin- ism and coerce membership in a VHHM class is to simply ensure that each output- invariant equivalence class of states has its own (common) branching behavior: that is the same (shifted) behaviors emanate from each and every one of its constituent states, irrespective of when any one of those states is traversed (in the tree). Or, more generally, one might propose a fixed and finite selection of such branching behaviors that are permissible in each such [x], again agnostic of (clock) time. Ulti- mately, either scheme would result in that particular transition-label structure being bisimilar to an image finite tree, and hence, a member of every VHHM class [27]. These ideas can be made precise using the following definitions, which suggest how common sets of behaviors may be combined with enforced non-determinism to ob- tain image-finite surrogate KS. Definition 53 (Output-Invariance Branching Determiner). An Output-Invariance Branching Determiner is a function D : N (O)? ? {BF2 x (A,B,C):x?Rn} F D : [x] 7? 2B (A,B,C)[x] . (5.64) In particular, the codomain of such a D is a set of behaviors starting from time 0, 136 as per our definition of BFx ; see Definition 47. Now, we define what it means for an LTI-derived GST to be obtained by ?choosing? from among a fixed selection of such branching determiners. Definition 54 (Determiner-Finite LTI GST). Let D = {D1, . . . ,DN} be a finite set of Output-Invariance Branching Determiner functions. Then we say that an LTI- derived set of behaviors ? and its associated GST ? is determiner finite (with respect to D) if given any behavior (y, u, x) and time ? in said GST, the set of all behaviors that extend (y, u, x)|? is exactly one of the sets of behaviors Di([x(?)]) shifted by ? . The above definition is somewhat more restrictive than necessary, at least as far as our objective of getting bisimilarity with image-finite structures. Really, we could allow the number of branching determiner functions to vary based on the [x] under consideration instead of using a common maximal integer N as in Definition 54; this would complicate the notation with little conceptual gain, though. Theorem 14 (Effective Image-finiteness of Non-constant Trajectories in Dete- rminer-Finite LTI GSTs). Given a GST GFx (A,B,C) that is determiner-finite with0 respect to D, any modal execution label will necessarily have transition structure in GFx (A,B,C) that is bisimilar to an image finite structure in that label.0 Proof. By the accumulated claims of Lemma 3 through Lemma 6, we know that all nodes reachable by order-equivalent trajectories are necessarily output invariant (with respect to each other). Then, since D specifies only a finite number of different trees that these nodes may serve as the root of, we conclude that we may as well 137 consider only finitely many different modal executions with the appropriate label in the surrogate KS, at least as far as bisimulation is concerned. Consider, however, the ramifications of Definition 54 for an output-invariance class that lies along a trajectory of constant-input/constant-output. Since that invariance class is preserved along such a trajectory by Lemma 3, the necessity of distributing finitely many ?sets? of behaviors along such a trajectory means that: one, said constant-input/constant-output trajectory must be time infinite; and two, those sets of behaviors must be self-similar or ?recursive? (in some sense) in order to cover the entire trajectory and still meet the definition. Thus, ?choices? such as these are unavoidably future-aware in a very fundamental sense. This property is not terribly interesting in the context of LTI systems, which are often driven and controlled by ?programs? that are only aware of the immediate state and time. Consider then a set of LTI behaviors created by a very simple ?controller?: suppose that such a controller has only two input values available to it, and one ? the initial one, say ? results in a constant output trajectory. If that controller?s second input is enabled only at certain times ? say, because of some (hypothetical) event trigger, perhaps one triggered by going through a particular state (as opposed to an output- invariance class of states) ? then it is easy to imagine creating a structure like the KS in Fig. 5.4. Here we have easily concocted a situation where local, state/time- based decision making leads to a somewhat more interesting structure, especially with regard to VHHM classes: after all, the lesson of the KS in Fig. 5.4 is one on just that subject. Indeed, it?s possible for just such ?controllers? to create an 138 LTI-derived GST that doesn?t belong any VHHM class. Though the results so far appear to be exclusionary ? as in they specify struc- tures that can?t m-saturated ? their ramifications are amplified by the determin- ism imposed on our LTI system?s behaviors and the properties of the real number line. As argued above, we have to enforce a less restrictive notion on constant- input/constant-output trajectories than satisfying a branch determining function. Definition 55 (Non-constant Branching Determiner Function). Let D? be an output- invariance branching determiner function. We say that D? is a non-constant output-invariance branching determiner function if it has the further property that none of the behaviors in D?([x]) begin with constant-input/constant-output seg- ments. Now we define a way of specifying when these non-constant determiner func- tions lead to branching from constant-input/constant-output segments of trajectory. Definition 56 (Determiner Distribution). A determiner distribution over a fi- nite set of non-constant output-invariance branching determiner functions, D? = {D?1 , . . . ,D?N}, is a function Ey,[x],u : [0, 1) ? R? {0} ? {1, . . . , N} (5.65) indexed by [x] ? N (O)?, y ? R` and u ? Rm; moreover, Ey,[x],u must satisfy the property that ? for any x, y ? E ?1y,[x],u({1, . . . , N}), there exists an open interval (a, b) ? (x, y) such that Ey,[x],u((a, b)) ? {0}; i.e. Ey,[x],u maps each element of (a, b) to 0. 139 And we redefine what it means to have a determiner-finite GST in terms of non-constant determiner functions and determiner distributions. Definition 57 (Determiner-Distribution-Finite LTI GST). Given an (indexed col- lection of) determiner distributions Ey,[x],u, we say that an LTI-derived set of behav- iors ? and its associated GST ? is determiner-distribution finite if given any behav- ior (y, u, x) where [t1, t2) ? R is any maximal interval of constant-input/constant- output trajectory segment therein, then ? there is a monotonic bijection ? : [t1, t2)? [0, 1) such that for all ? ? [t1, t2) ? if Ey,[x],u(?(?)) 6= 0, then each and every extension of (y(?), u(?), x(?)) that begins with a non-constant-input/constant-output segment is in Ey,[x],u(?(?)) and the only constant-input/constant-output trajectory emanating from (y(?), u(?), x(?)) as constant values (y(?), u(?)) ? otherwise the only trajectory emanating from (y(?), u(?), x(?)) is (y?, u?, x?) = (y(?), u(?), x(?)) = const. For nodes with no constant-input/constant-output trajectory emanating from them, Ey,[x],u(0) specifies the behaviors. These tedious and somewhat elaborate definitions are actually relatively straight- forward generalizations of their earlier counterparts, only now able to represent ex- amples like the hypothetical controller example above. Importantly, we now have a formalism within which to begin treating more interesting issues of VHHM mem- bership. 140 Theorem 15. Suppose there is a k ? {1, . . . , N} for which E ?1y,[x],u(k) has an accumu- lation point, x?. If every interval (0, b) 3 x? excludes all but finitely many elements of E ?1y,[x],u(k), then no LTI GST that is determiner-distribution finite by Ey,[x],u is modally saturated. Proof. The important observation here is that modal formulas will be able to ?count? the number of D?k branches that are remaining in the trajectory, so this structure meets the hypotheses of Corollary 2. In particular, the Henkin model has an extra transition from Fma(x?) to some other node with a self-loop. Much more importantly, though, we note that we can never modally saturate such structures within LTI GSTs as we have defined them! Indeed, the addition of a node that has a constant-modal-execution self-loop can only be represented by an (additional) open sub-interval of R within which no other branching is possible. However, this is impossible while still retaining the assumed accumulation point x?! On the other hand, we note that not being m-saturated doesn?t imply exclu- sion from a VHHM class, so indeed such structures may belong so some VHHM class of GSTs. However, Fig. 5.4 and its KS are again relevant: in the context of determiner-distribution finite tree, this aforementioned KS indicates what sort of constant-input/constant-output branching structure eludes all VHHM classes. In particular, it suggests that a prototypical example is a constant-input/constant- output trajectory with a delay ? literally a fixed time delay ? during which no branching is possible that then abuts an accumulation point like x? from the proof of Theorem 15! 141 Chapter 6: Congruence Results In this chapter, we will consider three different congruence results. By ?con- gruence result? we mean the following: given the composition of several component sub-systems, any one of the sub-systems may be substituted for another bisimilar system, and the new composition will be bisimilar to the original one. 6.1 Synchronous Interconnection of GSTs Derived from Behavioral Systems In [25], Julius et. al. defined a composition operator between behavioral sys- tems, and proved that bisimulation (Definition 11) is a congruence for that particular operator. We repeat these results from [25] below. Definition 58 (Composition of behavioral sytems [25]). Let ?1 and ?2 be two be- havioral systems with associated state maps x1 and x2, as in, say Lemma 1. Then the (synchronous) composition of (?1, x1) and (?2, x2) is denoted by (?, x) := (?1, x1)||(?2, x2), where 1. ? = (T,V? D1 ? D2,B); 2. B = {(v, d1, d2)|(v, d1) ? B1 ? (v, d2) ? B2}; and 142 3. x(?v, d1, d2?, t) := ?x1(?v, d1?, t), x2(?v, d2?, t)?. As a consequence of this composition operator, Julius et. al. prove the follow- ing congruence theorem [25]. Theorem 16 (Composition for behavioral systems is a congruence [25]). For i = 1, 2, 3, let (?i, xi) be behavioral state systems with associated state maps as in Defi- nition 58. Then ?1x1?x2?2 =? (?1, x1)||(?3, x3) x1;x3?x2;x3 (?2, x2)||(?3, x3). (6.1) Where x1; x3 is notation for the composed state map of Definition 58. It is natural to ask whether or not there is a similar composition operator for GSTs that likewise exhibits this congruence property. For GSTs constructed from behavioral systems, we define such a composition operator below, and subsequently prove that strong bisimulation (with the time-shift property) is indeed a congruence. Definition 59 (Synchronous composition of GSTs derived from behavioral sys- tems). Let GSTs G1 and G2 be GSTs derived from (?1, x1) and (?2, x2) according to Definition 33. We define the composition G1||G2 = (P1;2, p01;02,1;2,L1;2) as follows: { } ? P1;2 := ??v, d |t |t |t1, d2? , t? | ??v, d1? , t? ? P1 ? ??v, d2? , t? ? P2 ? {?p01, p02?}; ? p01;02 = ?p01, p02?; ? ??v, d , d ?|t1 2 , t? 1;2 ??v?, d? ? ?1, d? ?|t2 , t?? if and only if ?v?, d? , d?1 2?|t |t = ?v, d |t1, d2? ; ?p01, p02?  |t1;2 ??v, d1, d2? , t? ???v, d1, d2?|t, t? ? P1;2; and ? L1;2(??v, d |t |t1, d2? , t?) := ?V(?v, d1, d2? (t)). 143 Given this definition of composition, we can establish an easy congruence result if the alternate GST is strongly bisimilar to its replacement via a bisimulation relation with the time-shift property. Theorem 17. For i = 1, 2, 3, let Gi be GSTs derived from the respective behav- ioral state systems (?i, xi). Furthermore, let G1 ? G2 be strongly bisimilar with a bisimulation relation ? that has the time-shift property. Then G1||G3 and G2||G3 are strongly bisimilar (and are related by a bisimulation relation with the time-shift property). Proof. The proof is an easy consequence of Theorem 7. In particular, because G1 and G2 are strongly bisimilar with the time-shift property, Theorem 7 asserts that (?1, x1) and (?2, x2) are bisimilar. However, by construction, the (non-root) nodes of G1||G3 are exactly the states of the canonical partial order map p?1||?3 , and likewise for G2||G3 and p?2||?3 . That is G1||G3 is exactly the GST constructed from the composition (?1, x1)||(?3, x3), and likewise for G2||G3 and (?2, x2)||(?3, x3). Since bisimulation is congruence for behavioral systems (Theorem 16), applying Theorem 7 again gives the claimed result. The proof of Theorem 17 depends on having a strong bisimulation with the time-shift property, but this is not a severe restriction, since we are working exclu- sively with GSTs that are derived from behavioral systems. However, as Example 1 shows, it is not a trivial or superfluous requirement, either. Interestingly, the composition operator defined in Definition 59 looks roughly like a special case of the CSP-parallel composition operator defined in [15]. That 144 operator, however, is not exclusive to GSTs derived from behavioral systems, and so is more general at the expense of being time ?unaware?. Example 1 suggests that time-unaware notions of composition are unlikely to be comparable to bisimulation for behavioral systems, but the congruence properties of that CSP-parallel operator are nevertheless interesting and the subject of future work. 6.2 CSP-type Parallel Composition 6.2.1 Preliminaries First, we recall the definition of our CSP-parallel composition operator for GSTs from [15], which is written in terms of S-synchronizated interleavings of tra- jectories : see Definition 27. Definition 60 (S-synchronized Interleaving). Let G1 = (P1,1, p1,L1) and G2 = (P2,2, p2,L2) be GSTs, and WLOG assume that P1 ? P2 = ?. Also let T1 and T2 be trajectories (cf. Definition 27) from the roots of G1 and G2, respectively. Also let S ? L. Then total order (Q,Q) is an S-synchronized interleaving of T1 and T2 iff there exists a monotonic bijection ? ? {p ? T1 : L1(p) ? S} ? {p ? T2 : L2(p) ? S} such that the following hold. 1. L1(p) = L2(?(p)) for all p ? T1 such that L1(p) ? S. 2. Q = {p ? T1 : L1(p) 6? S} ? {p ? T2 : L2(p) 6? S} ? {(p, ?(p)) : L1(p) ? S}. 3. Define ?1 ? Q ? (T1 ? T ? ?2) by ?1(p) = p if p ? T1 ? T2 and ?1((p1, p2)) = p?1 otherwise, and similarly for ?2. Then, ?1(q) 1 ?1(q?) or ?2(q) 2 ?2(q) 145 implies q  ?Q q . We write IS(T1, T2) for the set of S-synchronized interleavings of T1 and T2. We thus have the following definition of a CSP-parallel composition operator for GSTs. Definition 61. Let G1 = (P1,1, p1,L1) and G2 = (P2,2, p2,L2) be GSTs with P1 ? P2 = ?. Then the GST G1 |S|G2 = (Q,Q, q0,LQ) is given by: 1. Q = {(p1, p2)} ? {T : T ? IS(T1, T2) for some trajectories T1 = (p1, p?1] of G1, T2 = (p2, p ? 2] of G2 with T1 and T2 not both empty.}. 2. q  ?Q q iff q = (p1, p2), or q = (r, ), q? = (r?r ,r?), and r is a prefix of r?. 3. q0 = (p1, p2). 4. Let q ? Q and let p? = sup(q). ?Then define LQ according to?? ???????L (p?1 ) if p? ? P1 LQ(q) = ????L (p?) if p??? 2 ? P2???L (p? ) if p?2 1 = (p?1, p?2) 6.2.2 Congruence and Weak Bisimulation We begin our consideration of weak bisimulation with an observation about the relationship between trajectories in the CSP-parallel composition of two GSTs and trajectories in the composed GSTs themselves. 146 Lemma 7. For i = 1, 2, let Gi = (Pi,i, pi,Li) be GSTs, and let C1 = G1|S|G2 = (Q1,Q1 , q01,LQ1) be the CSP-parallel composition of G1 and G2 on a set of syn- chronizing labels S. If q1 = (r1,r1) is a non-root node in C1 where r1 is obtained from the interleaving of right-closed trajectories T q1 ? P and T q1G 1 G ? P2, no more1 2 than one of which is empty, then the interval (q01, q1] ? Q1 is order equivalent to the set r?1 = {p ? r1 : sup?1((q01, p]) and sup ?2((q01, p]) exist}, when ordered by r1. Proof. The essential observation is that any q? = (r?,r?) Q1 q1 is itself an S- ? ? synchronized interleaving of two right-closed trajectories T qG and T q that are nec- 1 G2 essarily prefixes of the trajectories T q1G and T q1 G , respectively. This follows directly1 2 from the definition of the tree partial order Q1 in terms of prefixes (see condition 2 in Definition 61). Since such an r? necessarily has a maximal element ? and indeed sup ? (r?1 ) and sup? (r ? 2 ) both exist ? it can be injectively matched to a unique node in the interleaving q1 = (r1,r1) of which it is a prefix. Conversely, if any element of the total order (r1,r1), say p, has the property that {p? ? r1 : p? r1 p} has a supre- mum after projection through each of ?1 and ?2, then it corresponds to one and only one S-synchronized interleaving (of the appropriate right-closed trajectories). We note, however, that such an interval (q01, q1] need not be order equivalent to the entire interleaving q1 = (r1,r1). This is clarified in the subsequent example. Example 5. Let G1 = ([0, 1) ? (1, 2],?, 0,L1 : x ?7 x) and G2 = ([0, 1],?, 0,L2 : x 7? x) bet two GSTs, and consider the CSP-parallel composition C1 = G1|[0, 1)|G2 (that is the set of synchronizing labels is the right-open interval [0, 1) ? R). Further- more, let q = (r,r) be the S-synchronized interleaving of the trajectory [0, 1.5] in 147 G1 (the interval being defined according to the partial order for G1) and the trajec- tory [0, 1] in G2 that places the node 1 from G2 in the gap between [0, 1) and (1, 1.5] in G1. That is (r,r) is isomorphic to the interval [0, 1.5] ? R. We claim that the set of ancestors of q = (r,r) in C1, i.e. [0, q), is in fact order equivalent to (r\{1},r). This example seems innocuous, but it indicates an important consequence of Lemma 7 in terms of congruence properties. This will be revisited in Section 6.2.4, but for now, we proceed to prove the first of two congruence properties to be con- sidered. Theorem 18 (Weak Bisimulation is a congruence for CSP-parallel composition). For i = 1, 2, 3, let Gi = (Pi,i, pi,Li) be GSTs such that G1 and G2 are weakly bisimilar to each other. Then C1 := G1|S|G3 is weakly bisimilar to C2 := G2|S|G3. Proof. The proof consists of establishing a weak bisimulation relation between C1 = (Q1,Q1 , q01,LQ1) and C2 = (Q2,Q2 , q02,LQ2). To this end, let q1 = (r1,r1) be a (non-root) node in C1, and let q2 = (r2,r2) be a (non-root) node in C2. By definition then, q1 is an S-synchronized interleaving of some trajectories T q1 G ? P1 1 and T q1G ? P3 from the roots of G1 and G3, respectively, and q2 is an S-synchronized3 interleaving of some trajectories T q2G ? P2 and T q2G ? P3 from the roots of G2 and2 3 G3, respectively. We may assume from part 1 on Definition 61 that at least one of T q1 and T q1 is non-empty, and likewise for T q2G G G and T q2 G . Furthermore, let ?1,2 be1 3 2 3 a weak bisimulation relation between G1 and G2 that includes (p1, p2), the pair of root nodes from each. 148 Now we propose a candidate bisimulation relation, ?? Q1 ? Q2, between the nodes in C1 and C2. Unsurprisingly, we start by insisting that (q01, q02) ??. We specify the remaining elements of ? according to a set of pairs defined by the following condition: q1 (?(q2 iff ) ( ))? T q1 =6 ? ? T q2 =6 ? ? T q1(( G 6= ? ? T q2 =6 ? 1 G2 ) G3( G3 ))? q1 q2 q1 q2 ((TG =6 ? ? TG =6 ?) =? (?1(supTG ) ?1 2 1 1,2 ?1(supTG)2)) T q1 6= ? ? T q2G G 6= ? =? ? (supT q12 G ) = ?2(supT q2G ) . (6.2)3 3 3 3 That is non-root nodes q1 and q2 are related according to ? if and only if the endpoints of their constituent trajectories from G3 are identical and the endpoints of their constituent trajectories from G1 and G2 are bisimilar according to ?1,2. The first conjunct in (6.2) ensures that interleavings with empty trajectories from one operand GST do not get matched to interleavings with non-empty trajectories from the corresponding operand. We claim that ? as defined above is a weak bisimulation relation. We will prove the bisimulation property only for the case when T q1G ? P1 and T q2G ? P2 are1 2 both non-empty, and both ?1(sup r1) = supT q1 G ? P1 and ?1(sup r q21 2) = supTG ? P2 2. The other cases will have a similar proof. To that end, suppose that q1 ? q2 (with the aforementioned properties) and q? q? 1 Q1 q1, where q?1 = (r?1,r? ) is the interleaving of trajectories T 1G ? P and1 1 1 q? T 1G ? P3; we will show that there exists a q?2 Q2 q2 such that q?1 ? q?2 and (q ?3 1, q1] is order equivalent to (q2, q ? 2]. We will obtain the requisite q ? 2 by replacing elements in 149 the totally ordered set (r?1\r1,r? ) with elements from trajectories that extend T q21 G2 and T q2G ; the result will then extend the total order q2 = (r2,r2) as an interleaving3 of trajectories from G2 and G3, thus providing a q ? 2 Q2 q2 that has the desired properties. q? By definition of Q1 , we can say that T q1G is a prefix of T 1G and T q1G is a prefix1 1 3 q? of T 1G . Moreover, because ?1(supT q1 ) ? ? (supT q2G 1,2 1 G ), there exists a trajectory3 1 2 q? from the root of G2 ? call it T 2G ? that extends T q2 G and such that:2 2 q? ?? T 2 qG \T q2G is order equivalent to the trajectory T 1G \T q1G in G1, which starts from2 2 1 1 ?1(sup r1) = ?1(supT q1 G ); and1 ? ? ? q?1(supT 1G ) ? q ? (supT 2 ). 1 1,2 1 G2 q? q? Let ? : T 1G \T q1G ? T 2G \T q2G witness the order equivalence claimed above, and1 1 2 2 replace elements of (r?1\r1,r? ) as follows: replace the elements of r?1\r1 derived1 q? ? from T 1 q1 q G \TG ? T 1G with their appropriate image under ?. Formally, define a total1 1 1 order (s,s) as follows: s = {? ? ?1(r?) : r? ? r?1\r1 and r? ? P1}? {? (r?) : r? ? r?2 1\r1 and r? ? P3}? {(? ? ?1(r?), ?2(r?)) : r? ? r?1\r1 and r? ? P1 ? P3} (6.3) s1 s s2 iff ?1(s1) 1 ?1(s2) or ?2(s1) 1 ?2(s2). (6.4) Because ? is a bijection and the total order in (6.4) is a subset of an interleaving q? q? total order, we can construct an interleaving between T 2G and T 1 G by simply joining2 3 s ? r2 and suitably extending s ? r2 . Of course we will call this interleaving q?2, 150 and we claim that it has the aforementioned properties. That q?2 Q2 q2 is obvious from the construction. Likewise, it is obvious that q? ? q?1 2. The only property that remains to be checked is that (q1, q?1] is order equivalent to (q2, q ? 2]. But this follows from the construction and Lemma 7. In particular, Lemma 7 ensures that all elements of (q2, q ? 2] can be mapped injectively to elements in the interleaving q?2 = (r ? 2,r? ), and likewise, all of the elements of2 (q1, q ? 1] can be mapped injectively to elements in the interleaving q ? 1 = (r ? 1,r? ).1 Now, ? ? through the mapping suggested in (6.3) ? effectively serves as an order equivalence between the elements of the interleaving r?1\r1 and the elements of the interleaving r?2\r2, so it preserves the joint supremum property in Lemma 7. That is take a p ? (r?1,r? ) for which set I = {p? ? r1 : p? r1 p} meets the condition1 that both sup?1(I) and sup ?2(I) exist; then the analogous suprema will exist for the image of p under the order equivalence. Hence, the previous assertion based on Lemma 7 assures that (q1, q ? 1] and (q ? 2, q2] are order equivalent. 6.2.3 Congruence and Strong Bisimulation Recall the definition of strong bisimulation from [15] and given in Definition 30. Strong bisimulation is also a congruence for CSP-parallel composition, as we shall now prove. Theorem 19 (Strong Bisimulation is a congruence for CSP-parallel composition). For i = 1, 2, 3, let Gi = (Pi,i, pi,Li) be GSTs such that G1 and G2 are strongly bisimilar to each other. Then C1 := G1|S|G3 is strongly bisimilar to C2 := G2|S|G3. 151 Proof. As in the proof of Theorem 18, we establish a strong bisimulation relation between C1 = (Q1,Q1 , q01,LQ1) and C2 = (Q2,Q2 , q02,LQ2). As before, let q1 = (r1,r1) be a (non-root) node in C1, and let q2 = (r2,r2) be a (non-root) node in C2. Again, q1 will denote an S-synchronized interleaving of trajectories T q1 G ? P1 1 and T q1G ? P3 from the roots of G1 and G3, respectively, and q2 will denote an3 S-synchronized interleaving of trajectories T q2G ? P2 and T q2G ? P3 from the roots2 3 of G2 and G3, respectively. We may assume from part 1 on Definition 61 that at least one of T q1 and T q1 is non-empty, and likewise for T q2 and T q2G G G G . However, for1 3 2 3 this proof we will let ?1,2 be a strong bisimulation relation between G1 and G2 that includes (p1, p2), the pair of root nodes from each. The proof of Theorem 18 offers a useful starting point: indeed, the proposed bisimulation relation in (6.2) is an adequate choice even for strong bisimulation, since the additional properties of the (now) strong bisimulation ?1,2 can be propa- gated through the proof without any further modifications. In particular, the order equivalence ? should associate nodes in G1 with bisimilar nodes in G2 as per the definition of strong bisimulation. Of course, this will translate into pairing nodes in (q , q?1 1] to bisimilar nodes in (q2, q ? 2] because of the way that the proposed bisimula- tion relation (between C1 and C2) is defined. Thus, the same candidate bisimulation relation, derived as it now is from a strong bisimulation relation between G1 and G2, will be a strong bisimulation relation for right-closed trajectories that extend one or the other of two nodes that are bisimilar. However, we need to prove that each right-open trajectory from q1 can be matched to a right-open trajectory from q2. To wit, let q1 ? q2 (according to (6.2)), 152 and let Iq1 = (q1,?1) be a right open trajectory in C1: we have to show that there exists a right-open trajectory (q2,?2) that is order-equivalent to (q1,?1) in a way that is consistent with the bisimulation relation ?. We begin by noting that Iq1 = (q1,?1) is a set of interleavings of right- closed trajectories that are totally ordered by set containment (the prefix property in Definition 61). Thus, the constituent trajectories of these interleavings themselves form a right-open trajectory in at least one of the composed GSTs, G1 and G3. However, the strong bisimulation relation ?1,2 considers right-open trajectories as well, so we can follow the program in Theorem 18 to create a suitable set of right- closed interleavings that will form the desired trajectory (q2,?2). Formally, let R = {(ri,i) : i ? Iq1} be the set of interleavings (with indexed total orders), and let each (ri,r1) ? R be an S-synchronized interleaving of trajectories T riG and1 T ri r r G . Then it is clear that for i  j, T ri j ri jQ1 G ? TG and TG ? TG ; furthermore,3 1 1 3 3 at least one of the sets ?{T riG : i ? Iq1} ? P1 and ?{T ri1 G : i ? I3 q1} ? P3 fails to contain its own supremum in P1 or P3, respectively (if said supremum even exists). In other words, either ?{T riG : i ? Iq1} ? P1 is a right-open trajectory from1 supT q1G in G1 or ?{T riG : i ? Iq1} ? P3 is a right-open trajectory from supT q11 3 G3 in G3 (both may be such right-open trajectories). Note that we could also have used the sets of suprema ? e.g. ?{supT riG : i ? Iq1} ? P1 ? without falling afoul1 of Lemma 7, since we?re considering the endpoints of both constituent trajectories simultaneously: an endpoint from two interleaved trajectories is only ?hidden? in the way suggested by Lemma 7 when there fails to be an interleaving that has that precise node as a supremum ? see also Example 5. From this observation, we 153 continue the program in Theorem 18: we generate a trajectory in C2 by interleaving the trajectory T q1,?G = ?{supT riG : i ? Iq1} ? P3 with a trajectory that is bisimilar3 3 (according to ?1,2) to the trajectory T q1,?G = ?{supT riG : i ? Iq1} ? P1. Thus, let1 1 T q2,?G ? P2 be a trajectory in G2 for which there is a witness to strong bisimulation2 in the form of an order-preserving bijection ? : T q1,? ? T q2,?G G ; such a ? may be1 2 applied to Iq1 as in (6.3) and (6.4), thereby constructing a trajectory of interleavings in C2. That the generalization of ? from (6.3) and (6.4) preserves bisimulation of the intermediary nodes is a direct consequence of both the definition (6.2) and the fact that all of the constituent trajectories are themselves prefixes of larger, right-open trajectories. 6.2.4 Anomalies in CSP-Parallel Composition for GSTs As it turns out, Lemma 7 has rather profound implications for the congru- ence properties of CSP-parallel composition. As we have seen in Section 6.2.2 and Section 6.2.3, both weak and strong bisimulation are congruences for CSP-parallel composition of GSTs. However, in a literal sense, these congruence results only hold because not all nodes in an interleaving of trajectories are represented as nodes in the composed GST, as described in Lemma 7 and exemplified in Example 5. This effective hiding of nodes (and their labels) is obviously troublesome in the context of further composition, but the examples in this section demonstrate that it is a necessary price to pay for aforementioned compositionality results. The culmination of this section will be an example that ought to contradict the 154 congruence for both weak and strong bisimulation in the absence of the omission of nodes described in Lemma 7. The essence of this example is that asymptotic choices can be made differently even in GSTs that strongly bisimilar; we introduce this concept in the following example, Example 6 (contrast this with the example of asymptotic choice that illustrates the semantic difference between weak and strong bisimulation in [15]). Example 6 (A bisimilar order equivalence between trajectories does not imply equivalent extensibility). Consider two GSTs ? G?1 and G2 ? defined from the sets of nodes P1 = [0, 1) ? (1, 2] ? R and P2 = [0, 1) ?x?(0,1)(x ? (x, 1) ? x ? (1, 2]), where 0 is the root of each tree, and the tree partial order is suggested by Fig. 6.1. The labeling functions assign to any node x ? (0, 1) (from either tree) and any ?y, x? ? y ? (y, 1] the label given by the real number x, and to all other (non-root) ? ? ? ? : : : : : : : : : : : : 1 : : : 1 : : : : : G1 G :2 : : : 0 0 Figure 6.1: GSTs in Example 6. G1 and G2 are strongly bisimilar according to Definition 30, yet G2 contains an un-extendable trajectory that nevertheless has a bisimilar order equivalence to an extendable trajectory from G1. 155 nodes the label ? (again, see Fig. 6.1). Proposition 11. GSTs G1 and G2 given by Example 6 and Fig. 6.1 are strongly bisimilar according to Definition 30. Proof. We claim that the following is a strong bisimulation relation between G1 and G2: { }? { } ? := ?x, x? ? P1 ? P2 : x ? [0, 1) ?x?(0,1) ?y, ?x, y?? : y ? (x, 1) ? (1, 2) . (6.5) The only difficult case to check is for nodes x ? x for x ? (0, 1) and trajectories like (x, 2] in G1 and like (x, 1) in G2. First, we consider the trajectory (x, 2] in G1, and show that there is a bisimilar order equivalence to a trajectory in G2. Indeed there is, though: such a trajectory can be of the form (?x, x?, ?x, 2?], or of the form (x, y]; (?y, y?, ?y, 2?] for any y > x. In either case, matching identical real numbers forms a bisimilar order equivalence. On the other hand, this clearly covers all trajectories in G2 emanating from x except (x, 1), so it remains to check that there is a bisimilar order equivalence between that trajectory and one in G1. Again, though, the real numbers match (x, 1) to the trajectory (x, 1) in G1 in a bisimilar order equivalence: the previous consideration of other trajectories ensures this. The importance of Proposition 11 is thus: G1 and G2 as defined in Example 6 are strongly bisimilar, but clearly the trajectory (0, 1) in G1 is always extendable, whereas the trajectory (0, 1) in G2 is never extendable. This feature of G1 and 156 G2 can be used with CSP parallel composition to create interleavings that effec- tively ?place? nodes after the trajectory (0, 1) in G2. This ought to break strong bisimilarity because no ??s are possible after that particular trajectory in G2; as suggested above, congruence will only be saved because certain nodes in the inter- leaving will not appear as nodes in the CSP-parallel composition. The subsequent example alters G1 and G2 to exploit this idea explicitly in CSP parallel composition. Example 7 (?Counterexample? to strong bisimulation as a congruence for CSP parallel). Consider two GSTs ? G?1 and ?G ? 2 ? de?fined from the sets of nodes P ? 1 = [0, 1)?{0, 1}? (1, 2] ? R and P ?2 = [0, 1) (1, 2] ?x?(0,1)(x? (x, 1)? x?{0, 1}? (1, 2]), where 0 is the root of each tree, and the tree partial order is suggested by Fig. 6.2. Note the addition of separate ?branches? after [0, 1) in G1 and (0, 1) and (?x, x?, ?x, 1?) in G2. These extra branches carry the additional label ?: see Fig. 6.2. The labeling functions for these GSTs are otherwise the same as described in Example 6; again, see Fig. 6.2. Now consider a third GST, G3, defined over the set of nodes P3 = [0, 1] ? R, where 0 is again the root node, and the tree partial order is given by ? over the reals. The labeling function assigns to each node x ? (0, 1) the label given by the real number x, and to the node 1 it assigns the label ?. See Fig. 6.2. Proposition 12. GSTs G? and G?1 2 given by Example 7 and Fig. 6.2 are strongly bisimilar according to Definition 30. Proof. We propose a bisimulation relation between G?1 and G ? 2 that is much the same as the one in Proposition 11, only with the addition that nodes labeled by ? 157 ? ? ? ? ? ? : : : : : : : : : ? ? 1 1 1: : 1: 1 : :: G0 01 G2 G3 : : : 0 0 0 Figure 6.2: G? ?1 and G2 are strongly bisimilar according to Definition 30. matched in the obvious way (by pairing real numbers). The similarity between G1 and G2 and G ? 1 and G ? 2 also forms the basis for a proof of strong bisimulation: only the new trajectories that end in ?-labeled nodes need to be considered. As before, the properties of bisimulation are mostly obvious except for pairs of nodes of the form x ? x for x ? (0, 1). Indeed the only interesting new case is the trajectory (x, 2] in G?2, since all of the other trajectories that involve ??s are matched covered by the ? branches that parallel ? branches. However, in the case of (x, 2] in G?2, there is no harm in matching the ?-labeled nodes of that trajectory to those in G?1 since the nodes y ? (x, 1) ? P ?1 each have the option to do ? branches through the extensions (?y, y?, ?y, 1, 2?]. In Example 7, we?re using synchronization to forcibly create an interleaving in G?2|R|G3 that places the ?-labeled node from G3 in between the [0, 1) spine and the solitary ? branch in G?2, effectively completing said trajectory and providing an ?anchor? from which to distinguish it from the others. If the node from that 158 interleaving were represented as a node in the composition, then it would serve as a counterexample to congruence for both weak and strong bisimulation. However, as there is no interleaving of right-closed trajectories that places the ? node from G3 in exactly such a position, the CSP-parallel composition effectively ignores this ?choice? point. 6.3 A Process Algebra for Hybrid Systems: HyPA This section shows how discrete GSTs can be constructed from HyPA terms so that bisimulation on GSTs (recall that weak and strong bisimulation coincide for discrete trees) corresponds exactly with a congruence for HyPA terms in [4]. HyPA is summarized in Section 2.4. In [4],the operational semantics of HyPA are given as a hybrid transition sys- tem; the states in the transition were HyPA-term / variable-valuation pairs; this construction is summarized in Section 2.4. Bisimulation may then be defined as usual for such a transition system. The authors of [4] then consider different defi- nitions of bisimulation for terms alone. One obvious candidate defines terms p and q to be bisimilar iff for all variable valuations ?, ?p, ?? and ?q, ?? are bisimilar as states in the HyPA hybrid transition system. Unfortunately this relation is not a congruence for HyPA terms; the problem resides in the fact that parallel processes within terms can interfere with the variable valuations produced by another parallel process. To fix this problem, the authors introduce another relation, robust bisim- ulation, show it to be a congruence for HyPA, then establish that it is the same as 159 another relation, stateless bisimulation, given in the same paper. In the rest of this section we show how to construct GSTs from HyPA terms in such as way that two HyPA terms are statelessly bisimilar iff the corresponding GSTs are bisimilar. We begin by reviewing the definition of stateless bisimulation. T (Vp) is the set of HyPA terms that use only the recursive process variables Vp, ` Val is the set of valuations for the (continuous) model variables, the transition ? represents either a discrete action or a continuous flow (depending on `) and X is a set of ?terminating? states. This discussion suggests a way to obtain congruence with respect to HyPA: one must exhibit a bisimulation relation that includes all of the subprocess/ valuation pairs that are hidden by any initial choice of valuation. This is exactly the idea behind stateless bisimulation, which is indeed a congruence for HyPA [4]1. See Definition 20, which recalls the following notation from [4] (and Section 2.4): T (Vp) is the set of HyPA terms that use only the recursive process variables Vp, Val is the ` set of valuations for the (continuous) model variables, the transition ? represents either a discrete action or a continuous flow (depending on `) and X is a set of ?terminating? states. Thus, the goal should be to construct GSTs from HyPA processes in such a way that bisimulation between the GSTs corresponds exactly to stateless bisimulation (Definition 20) between the original processes. For simplicity we ignore X in what follows. The construction of GST Gp from 1It is proved in [4] that stateless bisimulation is equivalent to a more complicated notion of equivalence called robust bisimulation; thus, we may treat only stateless bisimulation without any loss of generality. 160 ?1 `1 a,? ?a ?p? ,? ? 1 p? 2 p? `21 ?3 `3 ?1 ?1 ?1 `1 a p? ?2 a,??a p? ,? ? 2 ?p? 2 a p? a p? ?2 `2 ? p ? 2 3 `3 ?3 ?3 ?1 `1 ? a,?? ? `a p ,? ? 3 p? 2 p? 23 ?3 `3 Figure 6.3: Constructing GSTs from HyPA Terms HyPA term p is exemplified in Fig. 6.3. First, let the root of the Gp be identified with p. Then for each valuation ? of the model variables, create one successor node of p that is identified with ?p, ?? and label these nodes as ?. Since each ?p, ?? is ` a hybrid transition system state, the node has transitions of form ?p, ?? ? ?p?, ? ?? for some `; for each such ?p?, ? ??, make a node for p? labeled by `. Now repeat this procedure (coinductively) from p? to obtain discrete GST Gp. We now have the following (recall that weak and strong bisimilarity coincide for discrete GSTs). Theorem 20. Let p and q be HyPA terms. Then p and q are statelessly bisimilar iff Gp and Gq are bisimilar. Proof. Let p and q be two HyPA processes, and construct two GSTs G1 = ?P, p0,-P 161 1 ... ... ... ... ... ... ... ... ... ... ... ... . . . . . . . . . . . . ... ... ... ... ... ... ... ... ... ... ... ... . . . . . . . . . . . . . . . . . . . . . . . . ,LP ? and G2 = ?Q, q0,-Q,LQ? from these processes according to the preceding. We show the reverse direction first: if G1 and G2 are related by a bisimulation relation R that includes ?p0, q0?, then there is a stateless bisimulation relation R that includes ?p,q?. From R, we suggest that { ( ? )? R = ?p?,q?? | ? pRq s.t. p =(  |p| ? 1 ? last(p) ?? ?proc2(p) = p ? ? )} q =  |q| ? 1 ? last(q) ?? ?proc2(q) = q? is such a stateless bisimulation relation. Clearly, R includes ?p,q? by construction, so we need only establish that R is a stateless bisimulation relation. To prove the first simulation condition in the definition of stateless bisimulation, arbitrarily choose p? and q? such that p?Rq?. Now choose an arbitrary valuation ? ?, and let ` t?p = ?p?, ? ?? ? ?p??, ? ??? be any transition from state ?p?, ? ??. It is easy to see that p?.? ? and p?.? ?.t?p are nodes in G1; it is also clear that p ? - p?.? ?P -P p?.? ?.t?p . Since R is a simulation relation, there exists a node q??? %Q q? such that p?.v?Rq??? and LP (p?.? ?) = L ? ?Q(q??) = ? . As p?.? ? is obviously an immediate successor of p?, q??? must be an immediate successor of q?; since LQ(q???) = ? ?, it must be the case that q??? = q ?.? ?. Now we again use the simulation property of R to assert the existence of a q?? %Q q?.? ? such that p?.? ?.t Rq?? and L (p?.? ??p P .t?p) = LQ(q??) = `. Reasoning as above, q?? must be an immediate successor to q?.? ?, and so last(q??) must be a transition with LQ(q??) = label(last(q??)) = `. Since q?? is a node in the tree, it must be true that last(q??) = ?q?, ? ?? ?` ?q??, ? ??q ? for some process q?? and valuation v??q . This establishes that ?q?, ? ?? can process the label `; since p?.? ?.t Rq???p , we conclude that p??Rq?? by definition of the set R. The other simulation condition follows by 162 symmetric arguments because R is a bisimulation relation. Hence, we conclude that R is a stateless bisimulation relation. In the other direction, suppose that R is a stateless bisimulation relation such that pRq. We claim that there is a bisimulation relation R between G1 and G2. First we define the set { ( ? ) R ? = ?p, q?| ? p?Rq? s?.t. ? (p = p ? p = ? last(p) ?? ?p ? = proc2(last(p))) ? }q = q ? q =  last(q) ?? ?q? = proc2(last(q)) . Then we claim that R = R ? ? {?p.?, q.??|?p, q? ? R ? and ? ? Val} is a bisimulation relation between G1 and G2. Since pRq, it is the case that p0Rq0. We first show simulation in one direction. Because both trees are discrete, it suf- fices to show simulation only for the immediate successor of a node. In particular, arbitrarily choose p? and q? such that p?Rq?. First, suppose that either p? =  or last(p?) ??, i.e. ?p?, q?? ? R ?. In this case, the only immediate successors to p? are of the form p?.? ?, so arbitrarily choose ? ? ? Val. Clearly, p?.? ?Rq?.? ? by definition, and LP (p?.? ?) = LQ(q?.? ?) = ? ?. This obviously establishes simulation for any immediate successor node of p?. Now consider p??Rq?? such that p?? = p?.? ?, i.e. ?p??, q??? ? R\R ?. Only nodes that end in the valuation ? ? can possibly be related to p?? by R, so we might as well write q?? = q?.? ?. The tree property and the construction of R from R ? ensure that p?R ?q?. Without much loss of generality, we may suppose that both p? and q? are non-empty: in that case, there exist stateless bisimilar processes p? 163 and q? such that proc2(last(p ?)) = p? and proc2(last(q ?)) = q?. However, stateless ` bisimilarity implies that for every transition t?p = ?p?, ? ?? ? ?p??, ? ??? ? i.e. every ` immediate successor to p?.? ? ? there is a transition t?q = ?q?, ? ?? ? ?q??, ? ??q ? such that p??Rq??. This implies that p??.t Rq???p .t?q by definition of the set R ?. Since LP (p??.t?p) = LQ(q??, t?q) = `, we have established simulation in one direction. Simu- lation in the other direction follows by symmetric arguments because R is a stateless bisimulation relation. There are yet other ways to represent HyPA processes as GSTs. For example, encoding HYPA processes as a behavioral systems suggests that if HyPA processes are regarded in terms of execution trajectories (i.e. functions of time), yet a different GST construction can be obtained. It should be noted that such a construction necessarily has a great deal more granularity, as the resulting GSTs would be non- discrete. Consequently, our previous results about strong bisimulation would likely have significant ramifications for such a GST construction. 164 Chapter 7: Conclusions and Future Research 7.1 Conclusions This dissertation introduces a new CPS modeling framework that mitigates some of the significant limitations associated with prior CPS models. In particular, we propose GSTs as a modeling framework that is general enough to encompass a wide swath of CPS systems yet inherits the rich and expressive compositionality of the process algebraic models (STs) from which it is derived. These structural advantages make GSTs a scalable tool for the modeling and design of safe, reliable CPSs: that is by using the inherent compositionality of GSTs to design and verify small, manageable subsystems, which can subsequently be combined into large, complex systems via flexible, principled compositionality operators. In Chapter 3, we formally defined GSTs by means of generalizing the notion of a tree; this construction analogizes the structure of Milner?s STs, and it is ultimately the source GSTs? flexibility. Also in this chapter, we considered two of the prevailing notions of bisimulation for non-discrete systems, and we proved for the first time that these notions are semantically distinct. This has wide implications for the study of CPSs, since specifying system equivalence up to weak bisimulation will lead to different behavior than specifying system equivalence up to strong bisimulation. 165 In Chapter 4, we considered the problem of ?unrolling? state-based behavioral systems into GSTs, and we demonstrated that such unrollings are not only possible but also preserve a notion of bisimulation. The success of this endeavor is essential to the value of GSTs as a modeling framework. To be useful, translating conven- tional CPS models into GSTs must preserve some meaningful notion of semantics: otherwise, GSTs could not be used to reason about conventional system models at all. In Chapter 5, we again followed in Milner?s (and Hennessy?s) footsteps by defining a generalized HML-like modal logic for GSTs. We further established that GHML has a relationship to (weak) bisimulation that mirrors the one between HML and bisimulation over STs; this idea extends to the definition of maximal VHHM classes of GSTs, which are maximal classes of GSTs for which a GHML modal for- mula can provide a diagnostic witness to non-bisimilarity between the constituent GSTs. Finally, we studied the circumstances under which Linear, Time-Invariant Systems are contained in a maximal VHHM class, thus specifying for the first time the extent to which GHML formulas are expressive enough to capture weak bisim- ulation between such systems. In Chapter 6, we defined a number of different composition operators over GSTs, and for each of these operators, we demonstrated that bisimulation is a con- gruence. We defined the following operators: first, a purely synchronous operator (of the sort common for behavioral systems); second, a novel asynchronous com- position operator applicable to arbitrary GSTs (and hence continuous and hybrid systems); and finally, operators translated from the HyPA process terms (which we 166 further showed are inherently discrete). 7.2 Future Research There are many directions for future research suggested by the work in this dissertation. The most natural and immediate ones are as follows. ? Additional CPS models may be ?unrolled? into GSTs in a bisimulation-preserving way; this will broaden the reach of GSTs as a flexible, unifying modeling frame- work. ? There are an abundance of composition operators in process algebra that have yet to be adapted as composition operators over GSTs; of course, the congru- ence properties of these adaptations need to be specified, and there may be unique and surprising results in this regard (especially in comparing weak and strong bisimulation). ? GHML should be studied with respect to strong bisimulation; this will lead to separate and interesting results about the expressivity of a simple modal logic relative to the unique semantics of strong bisimulation, especially in the context of continuous/hybrid systems. ? The characterization of GHML for LTI systems (with respect to weak bisim- ulation) depends on some moderately restrictive assumptions about both the system itself and the allowed inputs; another direction of future research in- volves weakening either or both of this restrictions. 167 ? There is an open problem of characterizing more general continuous-time sys- tems in terms of GHML and weak/strong bisimulation (nonlinear and time- varying systems, for example); in this dissertation, the results on LTI systems depend heavily on unique features of LTI systems that do not have immediate analogs in more general continuous-time systems. ? There is an interesting direction of research that involves specifying the prop- erties of composition operators with respect to maximal VHHM classes of GSTs; this problem was considered by Hollenberg [27] for discrete systems, but given the (potentially) unique semantics of composition operators over GSTs, there are likely to be interesting and surprising properties when this question is posed in the GST context. 168 Bibliography [1] Jerry Hirsch. Toyota prius recall: Automaker will fix nearly 700,000 hybrids. Los Angeles Times, November 2012. [2] Robert N. Charette. This car runs on code. IEEE Spectrum, February 2009. [3] T A Henzinger. The theory of hybrid automata. In Logic in Computer Science, 1996. LICS ?96. Proceedings., Eleventh Annual IEEE Symposium On, pages 278?292, 1996. [4] P J L Cuijpers and M A Reniers. Hybrid process algebra. The Journal of Logic and Algebraic Programming, 62(2):191?245, 2005. [5] Paulo Tabuada. Verification and Control of Hybrid Systems: A symbolic ap- proach. Springer, 2009. [6] S. Strubbe and A. van der Schaft. Algorithmic bisimulation for Communicating Piecewise Deterministic Markov Processes. In 44th IEEE Conference on De- cision and Control, 2005 and 2005 European Control Conference. CDC-ECC ?05, pages 6109?6114, 2005. [7] Sebastien Bornot and Joseph Sifakis. On the composition of hybrid systems. Hybrid Systems: Computation and Control, 1998. [8] Paulo Tabuada, George J. Pappas, and Pedro Lima. Compositional Abstrac- tions of Hybrid Control Systems. Discrete Event Dynamic Systems, 14(2):203? 238, 2004. [9] Luca P. Carloni, Roberto Passerone, Alessandro Pinto, and Alberto L. Angiovanni-Vincentelli. Languages and Tools for Hybrid Systems Design. Found. Trends Electron. Des. Autom., 1(1/2):1?193, 2006. [10] A. J. van der Schaft and J. M. Schumacher. Compositionality issues in discrete, continuous, and hybrid systems. International Journal of Robust and Nonlinear Control, 11(5):417?434, 2001. 169 [11] Aaron D. Ames, Alberto Sangiovanni-Vincentelli, and Shankar Sastry. Ho- mogeneous Semantics Preserving Deployments of Heterogeneous Networks of Embedded Systems. In Panos J. Antsaklis and Paulo Tabuada, editors, Net- worked Embedded Sensing and Control, number 331 in Lecture Notes in Control and Information Science, pages 127?154. Springer Berlin Heidelberg, 2006. [12] Esfandiar Haghverdi, Paulo Tabuada, and George J Pappas. Bisimulation rela- tions for dynamical, control, and hybrid systems. Theoretical Comput Science, 342:229?261, 2005. [13] Jan C. Willems. On interconnections, control, and feedback. IEEE Transactions on Automatic Control, 42(3):326?339, 1997. [14] Jan Willems. The Behavioral Approach to Open and Interconnected Systems. IEEE Control Systems Magazine, 27(6):46?99, 2007. [15] James Ferlez, Rance Cleaveland, and Steve Marcus. Generalized Synchroniza- tion Trees. In Foundations of Software Science and Computation Structures (FoSSaCS), pages 304?319. Springer Berlin Heidelberg, 2014. [16] Robin Milner. A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer-Verlag, 1980. [17] J. Ferlez, R. Cleaveland, and S. I. Marcus. Bisimulation in Behavioral Dynam- ical Systems and Generalized Synchronization Trees. In 2018 IEEE Conference on Decision and Control (CDC), pages 751?758, 2018. [18] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 1985. [19] James Ferlez, Rance Cleaveland, and Steve Marcus. Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees. Electronic Pro- ceedings in Theoretical Computer Science, 255:35?50, 2017. [20] David Park. Concurrency and Automata on Infinite Sequences. In Proceedings of the 5th GI-Conference on Theoretical Computer Science, pages 167?183. Springer-Verlag, 1981. [21] Samson Abramsky. A domain equation for bisimulation. Information and Computation, 92(2):161 ? 218, 1991. [22] P. Aczel. Non-Well-Founded Sets, volume 14 of CSLI Lecture Notes. Center for the Study of Language and Information, 1988. [23] William C. Rounds. On the relationships between Scott domains, synchro- nization trees, and metric spaces. Information and Control, 66(1?2):6 ? 28, 1985. 170 [24] Glynn Winskel. Synchronization Trees. Theoretical Computer Science, 34:33? 82, 1984. [25] A. A. Julius and A J van der Schaft. Bisimulation as congruence in the be- havioral setting. In Proceedings of the 44th IEEE Conference on Decision and Control and 2005 European Control Conference, pages 814?819, 2005. [26] Robert Goldblatt. Logics of Time and Computation. CSLI Lecture Notes, second edition, 1992. [27] Marco Hollenberg. Hennessy-Milner Classes and Process Algebra. In Alban Ponse, Maarten de Rijke, and Yde Venema, editors, Modal Logic and Process Algebra: A Bisimulation Perspective, Center for the Study of Language and Information Publication Lecture Notes, pages 187?216. Cambridge University Press, 1995. [28] Thomas Jech. Set Theory. Springer Monographs in Mathematics. Springer- Verlag, third millenium edition, 2003. [29] PJL Cuijpers. Prefix Orders as a General Model of Dynamics. \ldots on De- velopments in Computational Models \ldots, 2013. [30] Luca Aceto, Bard Bloom, and Frits Vaandrager. Turning SOS rules into equa- tions. Information and Computation, 111(1):1?52, 1994. [31] Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can?t be traced. J. ACM, 42(1):232?268, 1995. [32] Valentin Goranko and Martin Otto. Model theory of modal logic. In Johan Van Benthem and Frank Wolter Patrick Blackburn, editor, Studies in Logic and Practical Reasoning, volume 3 of Handbook of Modal Logic, pages 249?329. Elsevier, 2007. [33] J M Davoren and Paulo Tabuada. On Simulations and Bisimulations of General Flow Systems. In Hybrid Systems: Computation and Control, pages 145?158. Springer Berlin Heidelberg, 2007. [34] Steven G. Krantz and Harold R. Parks. A Primer of Real Analytic Functions. Birkha?user Advanced Texts Basler Lehrbu?cher. Birkha?user Basel, 2 edition, 2002. [35] Halsey Royden and Patrick Fitzpatrick. Real Analysis. Pearson, 4th edition, 2010. [36] A. Nonnengart. Modal frame characterization by way of auxiliary modalities. Logic Journal of IGPL, 6(6):875?899, 1998. [37] Robert. Goldblatt. Mathematics of Modality. CSLI lecture notes ; no. 43; CSLI lecture notes ; no. 43. CSLI Publications, 1993. 171