Temporal abstract interpretation

Patrick Cousot, Radhia Cousot

Research output: Contribution to journalConference article

Abstract

We study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to 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, a la CTL.

Original languageEnglish (US)
Pages (from-to)12-25
Number of pages14
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
StatePublished - Dec 3 2000
EventPOPL'00 - The 27th ACM SIGPLAN-SIGACT Symposium on Principles og Programming Languages - Boston, MA, USA
Duration: Jan 19 2000Jan 21 2000

    Fingerprint

ASJC Scopus subject areas

  • Software

Cite this