Exploiting over- and underapproximations for infinite-state counterpart models

Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


Software systems with dynamic topology are often infinite-state. Paradigmatic examples are those modeled as graph transformation systems (GTSs) with rewrite rules that allow an unbounded creation of items. For such systems, verification can become intractable, thus calling for the development of approximation techniques that may ease the verification at the cost of losing in preciseness and completeness. Both over- and under-approximations have been considered in the literature, respectively offering more and less behaviors than the original system. At the same time, properties of the system may be either preserved or reflected by a given approximation. In this paper we propose a general notion of approximation that captures some of the existing approaches for GTSs. Formulae are specified by a generic quantified modal logic that generalizes many specification logics adopted in the literature for GTSs. We also propose a type system to denote part of the formulae as either reflected or preserved, together with a technique that exploits under- and over-approximations to reason about typed as well as untyped formulae.
Original languageEnglish
Title of host publicationGraph Transformations : 6th International Conference, ICGT 2012, Bremen, Germany, September 24-29, 2012. Proceedings
PublisherSpringer Berlin Heidelberg
Publication date2012
ISBN (Print)978-3-642-33653-9
ISBN (Electronic)978-3-642-33654-6
Publication statusPublished - 2012
Externally publishedYes
Event6th International Conference on Graph Transformation: Modeling and Analysis of Dynamic Structures - University of Bremen, Bremen, Germany
Duration: 24 Sep 201229 Sep 2012
Conference number: 6


Conference6th International Conference on Graph Transformation
LocationUniversity of Bremen
SeriesLecture Notes in Computer Science

Fingerprint Dive into the research topics of 'Exploiting over- and underapproximations for infinite-state counterpart models'. Together they form a unique fingerprint.

Cite this