Abstract
We investigate a general framework which can be instantiated in order to obtain type systems for graph rewriting, allowing us to statically infer behavioural properties of a graph. We describe conditions such as the subject reduction property and compositionality that should be satisfied by such a framework. We present a methodology for proving these conditions, specifically we prove that it is sufficient to show properties that are local to graph transformation rules. In order to show the applicability of this framework, we describe in several case studies how to integrate existing type systems (for the π-calculus and the λ-calculus) and a system for typing acyclic graphs.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Baldan, P., Corradini, A., König, B.: A static analysis technique for graph transformation systems. In Proc. of CONCUR '01, pp. 381–395. Springer-Verlag, LNCS 2154 (2001)
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In Proc. of POPL '02, pp. 1–3. ACM (2002)
Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In Proc. of PARLE '87, Volume 2, pp. 141–158. Springer, LNCS 259 (1987)
Barr, M., Wells, C.: Category Theory for Computing Science. Prentice Hall (1990)
Bauderon, M., Courcelle, B.: Graph expressions and graph rewritings. Mathematical Systems Theory, 20, 83–127 (1987)
Cardelli, L., Gordon, A.D.: Types for mobile ambients. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages, pp. 79–92. ACM (1999)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In Proc. of ICSE '03 (25th International Conference on Software Engineering), pp. 385–395. IEEE Computer Society (2003)
Corradini, A., Montanari, U., Rossi, F.: Graph processes. Fundamenta Informaticae 26(3/4), 241–265 (1996)
Cousot, P.: Abstract interpretation. ACM Computing Surveys 28(2) (1996)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of POPL '77 (Los Angeles, California), pp. 238–252. ACM (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In Proc. of POPL '79 (San Antonio, Texas), pp. 269–282. ACM Press (1979)
Ehrig, H.: Introduction to the algebraic theory of graph grammars. In Proc. 1st International Workshop on Graph Grammars, pp. 1–69. Springer-Verlag, LNCS 73 (1979)
Ehrig, H., König, B.: Deriving bisimulation congruences in the DPO approach to graph rewriting. In Proc. of FOSSACS '04, pp. 151–166. Springer, LNCS 2987 (2004)
Fradet, P., Le Métayer, D.: Shape types. In Proc. of POPL '97, pp. 27–39. ACM (1997)
Gadducci, F., Heckel, R.: An inductive view of graph transformation. In Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT '97, pp. 223–237. Springer-Verlag, LNCS 1376 (1997)
Gadducci, F., Montanari, U.: Comparing logics for rewriting: Rewriting logic, action calculi and tile logic. Theoretical Computer Science 285(2), 319–358 (2002)
Gardner, P.: Closed action calculi. Theoretical Computer Science 228(1–2), 77–103 (1999)
Habel, A.: Hyperedge Replacement: Grammars and Languages. Springer-Verlag, LNCS 643 (1992)
Hatcliff, J., Dwyer, M.: Using the Bandera tool set to model-check properties of concurrent Java software. In Proc. of CONCUR 2001, pp. 39–58. Springer, LNCS 2154 (2001)
Honda, K.: Composing processes. In Proc. of POPL'96, pp. 344–357. ACM (1996)
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. In Proc. of POPL '01, pp. 128–141. ACM (2001)
Jeffrey, A.: A fully abstract semantics for concurrent graph reduction. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 128–131 (1994)
Jensen, O.H., Milner, R.: Bigraphs and transitions. In Proc. of POPL 2003, pp. 38–49. ACM (2003)
König, B.: Generating type systems for process graphs. In Proc. of CONCUR '99, pp. 352–367. Springer-Verlag, LNCS 1664 (1999)
König, B.: A general framework for types in graph rewriting. In Proc. of FST TCS '00, pp. 373–384. Springer-Verlag, LNCS 1974 (2000)
König, B.: A general framework for types in graph rewriting. Technical Report TUM-I0014, Technische Universität München (2000)
König, B.: A graph rewriting semantics for the polyadic π-calculus. In Workshop on Graph Transformation and Visual Modeling Techniques (Geneva, Switzerland), ICALP Workshops '00, pp. 451–458. Carleton Scientific (2000)
König, B.: Analysing input/output-capabilities of mobile processes with a generic type system. In Proc. of ICALP '00, pp. 403–414. Springer-Verlag, LNCS 1853 (2000)
König, B.: Hypergraph construction and its application to the compositional modelling of concurrency. In GRATRA '00: Joint APPLIGRAPH/GETGRATS Workshop on Graph Transformation Systems, Proceedings available as Report Nr. 2000-2 (Technische Universität Berlin) (2000)
König, B.: Hypergraph construction and its application to the static analysis of concurrent systems. Mathematical Structures in Computer Science 12(2), 149–175 (2002)
König, B.: Analysing input/output-capabilities of mobile processes with a generic type system. Journal of Logic and Algebraic Programming 63(1), 35–58 (2005)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems 21(5), 914–947 (1999)
Lafont, Y.: Interaction nets. In Proc. of POPL '90, pp. 95–108. ACM Press (1990)
Leifer, J.J.: Operational congruences for reactive systems. PhD thesis, University of Cambridge Computer Laboratory, September (2001)
Mac Lane, S.: Categories for the Working Mathematician. Springer-Verlag (1971)
Milner, R.: The polyadic π-calculus: a tutorial. Tech. Rep. ECS-LFCS-91-180, University of Edinburgh, Laboratory for Foundations of Computer Science (1991)
Mitchell, J.C.: Foundations for Programming Languages. MIT Press (1996)
Montanari, U., Pistore, M.: π-calculus, structured coalgebras, and minimal hd-automata. In Proc. of MFCS '00, pp. 569–578. Springer-Verlag, LNCS 1893 (2000)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag (1999)
Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. In Proc. of LICS '93, pp. 376–385 (1993)
Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. Journal of Mathematical Structures in Computer Science 6(5), 409–454 (1996)
Rensink, A.: Model checking graph grammars. In Proc. of AVOCS '03 (Workshop on Automated Verification of Critical Systems) (2003)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)
Rozenberg, G., editor: Handbook of Graph Grammars and Computing by Graph Transformation, Vol. 1: Foundations, volume 1. World Scientific (1997)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS (ACM Transactions on Programming Languages and Systems) 24(3), 217–298 (2002)
Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In Proc. of ASE '00 (International Conference on Automated Software Engineering), pp. 3–12. IEEE (2000)
Wadsworth, C.P.: Semantics and Pragmatics of the Lambda Calculus. PhD thesis, Oxford University, September (1971)
Yoshida, N.: Graph notation for concurrent combinators. In Proc. of TPPP '94. Springer-Verlag, LNCS 907 (1994)
Author information
Authors and Affiliations
Corresponding author
Additional information
This is a completely revised and extended version of a paper of which an earlier version has appeared in FSTTCS '00.
Rights and permissions
About this article
Cite this article
König, B. A general framework for types in graph rewriting. Acta Informatica 42, 349–388 (2005). https://doi.org/10.1007/s00236-005-0180-4
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00236-005-0180-4