Temporal abstract interpretation

Publisher Website
Google Scholar
Abstract
We study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to the @@@@-calculus, a generalization of the μ-calculus with new reversal and abstraction modalities as well as a new time-symmetric trace-based semantics. The more classical set-based semantics is shown to be an abstract interpretation of the trace-based semantics which leads to the understanding of model-checking and its application to data-flow analysis as incomplete temporal abstract interpretations. Soundness and incompleteness of the abstractions are discussed. The sources of incompleteness, even for finite systems, are pointed out, which leads to the identification of relatively complete sublogics, à la CTL.

This publication has 15 references indexed in Scilit: