Sciweavers

Share
APLAS
2005
ACM

An Abstract Interpretation Perspective on Linear vs. Branching Time

9 years 2 months ago
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 ...
Francesco Ranzato, Francesco Tapparo
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where APLAS
Authors Francesco Ranzato, Francesco Tapparo
Comments (0)
books