OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

On a Dynamic Logic for Graph Rewriting

Winckel, Mathias and Matthes, Ralph On a Dynamic Logic for Graph Rewriting. (2013) In: 2nd International Workshop on Algebraic, Logical, and Algorithmic Methods of System Modeling, Specification and Verification (SMSV 2013), 20 January 2013 - 21 January 2013 (Kherson, Ukraine).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://ceur-ws.org/Vol-1000/


Initially introduced by P. Balbiani, R. Echahed and A.Herzig, this dynamic logic is useful to talk about properties on termgraphs and to characterize transformations on these graphs. Also are presented the deterministic labelled graphs for which the logical framework is designed. This logic has been the starting point of a formal development, using the Coq proof assistant, to design a logical and algorithmic framework useful for verifyin and proving graph rewriting. The formalization allowed us to figure out some ambiguities in the involved concepts. This formalization is not the topic here but the clear view brought to us by the formal work, so the results will be expressed using the original mathematical objects of this logic. Some problems of this logic are demonstrated, relatively to the representation of graph rewriting. Some are minor issues but some are far more important for the adequation between the formulas about graph rewriting and the actual rewriting systems. Invalidating some resulting propositions, solutions are given to reestablish the logical characterization of graph rewriting, which was the initial purpose.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-01233230
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:30 Oct 2015 15:16

Repository Staff Only: item control page