Predicate diagrams for the verification of reactive systems

Colloque avec actes et comité de lecture. internationale.International audienceWe define a class of diagrams that represent abstractions of---possibly infinite-state---reactive systems described by specifications written in temporal logic. Our diagrams are intended as the basis for the verification of both safety and liveness properties of such systems. Non-temporal proof obligations establish the correspondence between the original specification and the diagram, whereas model checking can be used to verify properties over finite-state abstractions. We describe the use of abstract interpretation techniques to generate proof diagrams from a given specification and user-defined predicates that represent sets of states