For Real-time And Hybrid Systems. Ltlc: Continuous-time Temporal Logic,

Hybrid systems are computational systems consisting of both continuous and dis-crete components. Typical examples are digital controllers that interact with contin-uously changing physical environments. Real-time systems are a subclass of hybridsystems where the continuous components of the system are clocks which are used toexpress the timing constraints on the system. Because of their extensive applicationin industry and national defene, real-time and hybrid systems mostly focus on thesafety and reliability properties. So the formal analysis of these systems becomes aninteresting topic.In order to specify real-time and hybrid systems, many temporal logics, such asMetric Interoal Temporal Logic, Real-Time Temporal Logic, Integrator ComputationTree Logic, and Hybrid Temporal Logic have been proposed. Though these logics aregood at specifying properties of real-time and hybrid systems, they are not suited fordescribing the implementations of such systems. They lack the ability to describe thedynamic change in the state of real-time and hybrid systems.In the literature, real-time and hybrid systems are usually described by TimedAutomata, Hybrid Automata, Timed Transition Sgstems and Phase Transition Sys-tems. However, these system description languages cannot be used as specificationlanguages, because they lack the ability to express some important properties(suchas safety properties and liveness properties) of real-time and hybrid systems. Thus,redl-time and hybrid systems and their properties are usually described by differentlanguages.In this thesis, a new linear temporal logic with continuous semantics, called LTLC,is introduced. It is an extension of Manna and Pnueli's linear temporal logic. It canexpress both the properties and the implementations of real-time and hybrid systems.With LTLC, systems can be described at many levels of abstraction, from high-levelrequirement specifications to low-level implementation models, and the conformancebetween different descriptions can be expressed by logical implication.Three sub-languages of LTLC, called LTLC/B, LTLC/R and LTLC/H, are definedand the satisfiability problems for the first two are proved to be decidable. They areused to represent finite-state reactive systems, finite-location real-time systems andhybrid systems respectively Our decision procedure for LTLC/B can be used to checkwhether a finite-8tate reactive system meets a requlred specification or whether a fiIilte-state reactive system conforms with another system. Our procedure for LTLC/R cando the similar things for real-time systems with finite control locations.In addition, a modelcheching procedure for multirate hybrid systems is al8o given.It can decide whether a formula in LTLC/H is true with respect to a given multirateautomatoll whose jump transitions h8Ppen only at integer times.