Abstract
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.
Partly supported by the EU FP7-ICT IP ASCEns and by the MIUR PRIN SisteR.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baldan, P., Corradini, A., König, B.: A Static Analysis Technique for Graph Transformation Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 381–395. Springer, Heidelberg (2001)
Baldan, P., Corradini, A., König, B., Lluch Lafuente, A.: A Temporal Graph Logic for Verification of Graph Transformation Systems. In: Fiadeiro, J.L., Schobbens, P.-Y. (eds.) WADT 2006. LNCS, vol. 4409, pp. 1–20. Springer, Heidelberg (2007)
Baldan, P., König, B.: Approximating the Behaviour of Graph Transformation Systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 14–29. Springer, Heidelberg (2002)
Baldan, P., König, B., König, B.: A Logic for Analyzing Abstractions of Graph Transformation Systems. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 255–272. Springer, Heidelberg (2003)
Bauer, J., Boneva, I., Kurbán, M.E., Rensink, A.: A Modal-Logic Based Graph Abstraction. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 321–335. Springer, Heidelberg (2008)
Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic, A Language Theoretic Approach. Cambridge University Press, Cambridge (2012)
Dawar, A., Gardner, P., Ghelli, G.: Expressiveness and complexity of graph logic. Information and Computation 205(3), 263–310 (2007)
Gadducci, F., Lluch Lafuente, A., Vandin, A.: Counterpart semantics for a second-order mu-calculus. Fundamenta Informaticae 118(1-2) (2012)
Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and Analysis Using GROOVE. Software Tools for Technology Transfer 14(1), 15–40 (2012)
König, B., Kozioura, V.: Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 197–211. Springer, Heidelberg (2006)
Lluch Lafuente, A., Vandin, A.: Towards a Maude Tool for Model Checking Temporal Graph Properties. In: Gadducci, F., Mariani, L. (eds.) GT-VMT. ECEASST, vol. 42, EAAST (2011)
Rensink, A.: Towards model checking graph grammars. In: Leuschel, M., Gruner, S., Lo Presti, S. (eds.) AVOCS. DSSE-TR, vol. 2003-2. University of Southampton (2003)
Rensink, A.: Isomorphism checking in GROOVE. In: Zündorf, A., Varró, D. (eds.) GraBaTs. ECEASST, vol. 1. EAAST (2006)
Rensink, A., Distefano, D.: Abstract graph transformation. In: Mukhopadhyay, S., Roychoudhury, A., Yang, Z. (eds.) SVV. ENTCS, vol. 157(1), pp. 39–59. Elsevier, Amsterdam (2006)
Rensink, A., Zambon, E.: Neighbourhood abstraction in GROOVE. In: de Lara, J., Varró, D. (eds.) GraBaTs. ECEASST, vol. 32. EAAST (2010)
Zambon, E., Rensink, A.: Using Graph Transformations and Graph Abstractions for Software Verification. In: Corradini, A. (ed.) ICGT - Doctoral Symposium. ECEASST, vol. 38. EASST (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gadducci, F., Lluch Lafuente, A., Vandin, A. (2012). Exploiting Over- and Under-Approximations for Infinite-State Counterpart Models. In: Ehrig, H., Engels, G., Kreowski, HJ., Rozenberg, G. (eds) Graph Transformations. ICGT 2012. Lecture Notes in Computer Science, vol 7562. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33654-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-33654-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33653-9
Online ISBN: 978-3-642-33654-6
eBook Packages: Computer ScienceComputer Science (R0)