Hybrid diagrams

AbstractHybrid systems provide a formal model for physical systems controlled by discrete-state controllers. To help with the design of correct controllers, we present a methodology that enables the verification of linear-time temporal logic properties of general, non-linear hybrid systems. The methodology is based on the deductive transformation and algorithmic checking of hybrid diagrams.Hybrid diagrams are graphs whose vertices and edges are labeled with first-order assertions; they represent system abstractions, together with the progress properties that have been proved about them. The verification process begins with the automatic construction of an initial diagram, whose behavior coincides with that of the hybrid system. The proof of a specification is constructed by applying a series of diagram transformations to this initial diagram. The transformations preserve behavior containment, and the aim of the transformations is to obtain a diagram that can be algorithmically shown to satisfy the specification. Whenever the algorithmic check of a diagram fails, the check returns guidance for the further transformation of the diagram, or indications about possible counterexamples to the specification.We present four rules for transforming diagrams: each rule enables the study of a certain class of temporal logic properties. While some rules can be applied unconditionally, others require the proof of first-order verification conditions. We prove that the rules lead to the first verification methodology for general hybrid systems that is complete (relative to first-order reasoning) for proving specifications expressed in first-order linear-time temporal logic, provided no temporal operator appears in the scope of a quantifier