Numerous temporal logics have been proposed for thie specification of hybrid systems. Though these logics are good as specification languages for representing properties of hybrid systems, they are unsuitable to be used as system description languages for representing hybrid systems them-selves. Hybrid systems are usually described by Phase Transition Systems(PTS) or by Hybrid Automata(HA). But PTS and HA cannot be used as specification languages for hybrid systems. Thus, hybrid systems and their properties are usually described with different languages. In this paper, a new linear temporal logic with continuous semantics (LTLC) is proposed. It can be conveniently used both as a specification language and as a system description language for hybrid systems. Thus, both systems and properties can be written in a unified framwork. We expect this advantage of LTLC will facilitate the verification of hybrid systems.
展开▼
