Hybrid systems are computational systems consisting of both continuous and discrete components. Typical examples are digital controllers that interact with continuously changing physical environments. Realtime 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, realtime and hybrid systems mostly focus on thesafety and reliability properties. So the formal analysis of these systems becomes aninteresting topic.In order to specify realtime and hybrid systems, many temporal logics, such asMetric Interoal Temporal Logic, RealTime Temporal Logic, Integrator ComputationTree Logic, and Hybrid Temporal Logic have been proposed. Though these logics aregood at specifying properties of realtime 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 realtime and hybrid systems.In the literature, realtime and hybrid systems are usually described by TimedAutomata, Hybrid Automata, Timed Transition Sgstems and Phase Transition Systems. 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 realtime and hybrid systems. Thus,redltime 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 realtime and hybrid systems.With LTLC, systems can be described at many levels of abstraction, from highlevelrequirement specifications to lowlevel implementation models, and the conformancebetween different descriptions can be expressed by logical implication.Three sublanguages 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 finitestate reactive systems, finitelocation realtime systems andhybrid systems respectively Our decision procedure for LTLC/B can be used to checkwhether a finite8tate reactive system meets a requlred specification or whether a fiIiltestate reactive system conforms with another system. Our procedure for LTLC/R cando the similar things for realtime 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.
