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 language||English (US)|
|Number of pages||14|
|Journal||Conference Record of the Annual ACM Symposium on Principles of Programming Languages|
|State||Published - Dec 3 2000|
|Event||POPL'00 - The 27th ACM SIGPLAN-SIGACT Symposium on Principles og Programming Languages - Boston, MA, USA|
Duration: Jan 19 2000 → Jan 21 2000
ASJC Scopus subject areas