For verifying systems involving a wide number or even an infinite number of states, standard model checking needs approximating techniques to be tractable. Abstract interpretation offers an appropriate framework to approximate models of reactive systems in order to obtain simpler models, where properties of interest can be effectively checked. In this work we study the impact of domain refinements in abstract interpretation based model checking. We consider the universal fragment of the branching time temporal logic CTL∗ and we characterize the structure of temporal formulae that are verified in new abstract models obtained by refining an abstract domain by means of reduced product and disjunctive completion, or by simplifying the domain by their inverse operations of complementation and least disjunctive bases.

Refining and Compressing Abstract Model Checking

QUINTARELLI, ELISA
2001

Abstract

For verifying systems involving a wide number or even an infinite number of states, standard model checking needs approximating techniques to be tractable. Abstract interpretation offers an appropriate framework to approximate models of reactive systems in order to obtain simpler models, where properties of interest can be effectively checked. In this work we study the impact of domain refinements in abstract interpretation based model checking. We consider the universal fragment of the branching time temporal logic CTL∗ and we characterize the structure of temporal formulae that are verified in new abstract models obtained by refining an abstract domain by means of reduced product and disjunctive completion, or by simplifying the domain by their inverse operations of complementation and least disjunctive bases.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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: http://hdl.handle.net/11311/688627
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact