An abstract interpretation perspective on linear vs. branching time

It is known that the branching time language ACTL and the linear time language for all LTL of universally quantified formulae of LTL have incomparable expressive powers, i.e., Sem(ACTL) and Sem(for all LTL) are incomparable sets. Within a standard abstract interpretation framework, ACTL can be viewed as an abstract interpretation LTLfor all of LTL where the universal path quantifier V abstracts each linear temporal operator of LTL to a corresponding branching state temporal operator of ACTL. In abstract interpretation terms, it turns out that the universal path quantifier abstraction of LTL is incomplete. In this paper we reason on a generic abstraction a over a domain A of a generic linear time language L. This approach induces both a language alpha L of a-abstracted formulae of L and an abstract language L-alpha whose operators are the best correct abstractions in A of the linear operators of L. When the abstraction a is complete for the operators in L it turns out that alpha L and L alpha have the same expressive power, so that trace-based model checking of aL can be reduced with no lack of precision to Abased model checking of L alpha. This abstract interpretation-based approach allows to compare temporal languages at different levels of abstraction and to view the standard linear vs. branching time comparison as a particular instance.