An Abstract Interpretation Perspective on Linear vs. Branching Time

act Interpretation Perspective on Linear vs. Branching Time Francesco Ranzato and Francesco Tapparo Dipartimento di Matematica Pura ed Applicata, Universit`a di Padova, Italy It is known that the branching time language ACTL and the linear time language ∀LTL of universally quantified formulae of LTL have incomparable expressive powers, i.e., Sem(ACTL) and Sem(∀LTL) are incomparable thin a standard abstract interpretation framework, ACTL can be viewed stract interpretation LTL∀ of LTL where the universal path quantifier racts each linear temporal operator of LTL to a corresponding branching mporal operator of ACTL. In abstract interpretation terms, it turns out universal path quantifier abstraction of LTL is incomplete. In this paper n on a generic abstraction α over a domain A of a generic linear time L. This approach induces both a language αL of α-abstracted formulae an abstract language Lα whose operators are the best correct abstracA of the linear operators of L. When ...

• Type: Conference
• Year: 2005
• Where: APLAS
• Authors: Francesco Ranzato, Francesco Tapparo
• Keywords: APLAS 2005, Branching Time, Linear, Linear Time