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.

An abstract interpretation perspective on linear vs. branching time

RANZATO, FRANCESCO;TAPPARO, FRANCESCO
2005

Abstract

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.
2005
Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan
3540297359
File in questo prodotto:
File Dimensione Formato  
paper-published-on-lncs.pdf

accesso aperto

Tipologia: Published (publisher's version)
Licenza: Accesso libero
Dimensione 598.48 kB
Formato Adobe PDF
598.48 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/1426808
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact