scholarly journals Strategic port graph rewriting: an interactive modelling framework

2018 ◽  
Vol 29 (5) ◽  
pp. 615-662 ◽  
Author(s):  
MARIBEL FERNÁNDEZ ◽  
HÉLÈNE KIRCHNER ◽  
BRUNO PINAUD
Keyword(s):  
Complex Systems ◽  
Graph Transformation ◽  
Formal Semantics ◽  
General Setting ◽  
Term Rewriting ◽  
Graph Rewriting ◽  
Modelling Framework ◽  
Initial Graph ◽  
Rewrite Rules ◽  
Interactive Modelling

We present strategic port graph rewriting as a basis for the implementation of visual modelling tools. The goal is to facilitate the specification and programming tasks associated with the modelling of complex systems. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. We give a formal semantics for the language, and describe its implementation: the graph transformation and visualisation tool Porgy.

Jungle Evaluation

1991 ◽  
Vol 15 (1) ◽  
pp. 37-60
Author(s):  
Annegret Habel ◽  
Hans-Jörg Kreowski ◽  
Detlef Plump
Keyword(s):  
Term Rewriting ◽  
Bipartite Graphs ◽  
Graph Grammar ◽  
Graph Rewriting ◽  
Structural Induction ◽  
Rewrite Rules ◽  
The Rich

Jungle evaluation is proposed as a new graph rewriting approach to the evaluation of functional expressions and, in particular, of algebraically specified operations. Jungles – being intuitively forests of coalesced trees with shared substructures – are certain acyclic hypergraphs (or equivalently, bipartite graphs) the nodes and edges of which are labeled with the sorts and operation symbols of a signature. Jungles are manipulated and evaluated by the application of jungle rewrite rules, which generalize equations or, more exactly, term rewrite rules. Indeed, jungle evaluation turns out to be a compromise between term rewriting and graph rewriting displaying some favorable properties: the inefficiency of term rewriting is partly avoided while the possibility of structural induction is maintained, and a good part of the existing graph grammar theory is applicable so that there is some hope that the rich theory of term rewriting is not lost forever without a substitute.

Algebraic properties of processes for Local Action Systems

2002 ◽  
Vol 12 (4) ◽  
pp. 423-448
Author(s):  
NICO VERLINDEN ◽  
DIRK JANSSENS
Keyword(s):  
Petri Nets ◽  
Formal Semantics ◽  
Dynamic Structure ◽  
Concurrent Systems ◽  
Local Action ◽  
Graph Rewriting ◽  
Action Systems ◽  
Algebraic Properties ◽  
Dynamic Structures

Graph rewriting has been used extensively to model the behaviour of concurrent systems and to provide a formal semantics for them. In this paper, we investigate processes for Local Action Systems (LAS); LAS generalize several types of graph rewriting based on node replacement and embedding. An important difference between processes for Local Action Systems and the process notions that have been introduced for other systems, for example, Petri nets, is the presence of a component describing the embedding mechanism. The aim of the paper is to develop a methodology for dealing with this embedding mechanism: we introduce a suitable representation (a dynamic structure) for it, and then investigate the algebraic properties of this representation. This leads to a simple characterization of the configurations of a process and to a number of equational laws for dynamic structures. We illustrate the use of these laws by providing an equational proof of one of the basic results for LAS processes, namely that the construction yielding the result graph of a process behaves well with respect to the sequential composition of processes.

scholarly journals A rewriting calculus for cyclic higher-order term graphs

2007 ◽  
Vol 17 (3) ◽  
pp. 363-406 ◽  
Author(s):  
PAOLO BALDAN ◽  
CLARA BERTOLISSI ◽  
HORATIU CIRSTEA ◽  
CLAUDE KIRCHNER
Keyword(s):  
Order Term ◽  
Equational Theory ◽  
Term Rewriting ◽  
Higher Order ◽  
Graph Representation ◽  
First Order ◽  
Rewrite Rules ◽  
Evaluation Mechanism ◽  
Matching Constraints ◽  
Higher Order Term

The Rewriting Calculus (ρ-calculus, for short) was introduced at the end of the 1990s and fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the structured results obtained are first class objects of the calculus. The evaluation mechanism, which is a generalisation of beta-reduction, relies strongly on term matching in various theories.In this paper we propose an extension of the ρ-calculus, called ρg-calculus, that handles structures with cycles and sharing rather than simple terms. This is obtained by using recursion constraints in addition to the standard ρ-calculus matching constraints, which leads to a term-graph representation in an equational style. Like in the ρ-calculus, the transformations are performed by explicit application of rewrite rules as first-class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.We show that the ρg-calculus, under suitable linearity conditions, is confluent. The proof of this result is quite elaborate, due to the non-termination of the system and the fact that ρg-calculus-terms are considered modulo an equational theory. We also show that the ρg-calculus is expressive enough to simulate first-order (equational) left-linear term-graph rewriting and α-calculus with explicit recursion (modelled using a letrec-like construct).

scholarly journals PORGY: A Visual Graph Rewriting Environment for Complex Systems

2012 ◽  
Vol 31 (3pt4) ◽  
pp. 1265-1274 ◽  
Author(s):  
B. Pinaud ◽  
G. Melançon ◽  
J. Dubois
Keyword(s):  
Complex Systems ◽  
Graph Rewriting ◽  
Visual Graph

R2M: A RECONFIGURABLE REWRITE MACHINE

1994 ◽  
Vol 04 (01n02) ◽  
pp. 171-180
Author(s):  
R. RAMESH
Keyword(s):  
Programming Languages ◽  
Pattern Matching ◽  
Parallel Architecture ◽  
Term Rewriting ◽  
Fixed Number ◽  
Main Memory ◽  
Input Size ◽  
Computational Paradigm ◽  
Rewrite Rules ◽  
Parallel Pattern

Term rewriting is a popular computational paradigm for symbolic computations such as formula manipulation, theorem proving and implementations of nonprocedural programming languages. In rewriting, the most demanding operation is repeated simplification of terms by pattern matching them against rewrite rules. We describe a parallel architecture, R2M, for accelerating this operation. R2M can operate either as a stand-alone processor using its own memory or as a backend device attached to a host using the host’s main memory. R2M uses only a fixed number (independent of input size) of processing units and fixed capacity auxiliary memory units, yet it is capable of handling variable-size rewrite rules that change during simplification. This is made possible by a simple and reconfigurable interconnection present in R2M. Finally, R2M uses a hybrid scheme that combines the ease, and efficiency of parallel pattern matching using the tree representation of terms, and the naturalness of their dag representation for replacements.

Formal Modeling and Analysis of Object Oriented Systems using Triple Graph Grammars

2015 ◽  
Vol 6 (2) ◽  
pp. 48-64 ◽  
Author(s):  
Wafa Chama ◽  
Allaoua Chaoui ◽  
Seidali Rehab
Keyword(s):  
Graph Transformation ◽  
Formal Semantics ◽  
Graph Grammars ◽  
Rewriting Logic ◽  
Modeling Framework ◽  
Modeling Tools ◽  
Modeling And Analysis ◽  
Automatic Translation ◽  
Meta Modeling ◽  
Triple Graph Grammars

This paper proposes a Model Driven Engineering automatic translation approach based on the integration of rewriting logic formal specification and UML semi-formal models. This integration is a contribution in formalizing UML models since it lacks for formal semantics. It aims at providing UML with the capabilities of rewriting logic and its Maude language to control and detect incoherencies in their diagrams. Rewriting logic Maude language allows simulation and verification of system's properties using its LTL model-checker. This automatic translation approach is based on meta-modeling and graph transformation since UML diagrams are graphs. More precisely, the authors have proposed five meta-models and three triple graph grammars to perform the translation process. The authors have used Eclipse Generative Modeling tools: Eclipse Modeling Framework (EMF) for meta-modeling, Graphical Modeling Framework (GMF) for generating visual modeling tools and TGG Interpreter for proposing triple graph grammars. The approach is illustrated through an example.

scholarly journals Annotation of rule-based models with formal semantics to enable creation, analysis, reuse and visualization

2015 ◽  
Vol 32 (6) ◽  
pp. 908-917 ◽  
Author(s):  
Goksel Misirli ◽  
Matteo Cavaliere ◽  
William Waites ◽  
Matthew Pocock ◽  
Curtis Madsen ◽  
...  
Keyword(s):  
Semantic Information ◽  
Biological Systems ◽  
Formal Semantics ◽  
Proof Of Concept ◽  
Rule Based ◽  
Model Reuse ◽  
Modelling Framework ◽  
Automated Interpretation ◽  
Machine Readable ◽  
Programmatic Access

Abstract Motivation: Biological systems are complex and challenging to model and therefore model reuse is highly desirable. To promote model reuse, models should include both information about the specifics of simulations and the underlying biology in the form of metadata. The availability of computationally tractable metadata is especially important for the effective automated interpretation and processing of models. Metadata are typically represented as machine-readable annotations which enhance programmatic access to information about models. Rule-based languages have emerged as a modelling framework to represent the complexity of biological systems. Annotation approaches have been widely used for reaction-based formalisms such as SBML. However, rule-based languages still lack a rich annotation framework to add semantic information, such as machine-readable descriptions, to the components of a model. Results: We present an annotation framework and guidelines for annotating rule-based models, encoded in the commonly used Kappa and BioNetGen languages. We adapt widely adopted annotation approaches to rule-based models. We initially propose a syntax to store machine-readable annotations and describe a mapping between rule-based modelling entities, such as agents and rules, and their annotations. We then describe an ontology to both annotate these models and capture the information contained therein, and demonstrate annotating these models using examples. Finally, we present a proof of concept tool for extracting annotations from a model that can be queried and analyzed in a uniform way. The uniform representation of the annotations can be used to facilitate the creation, analysis, reuse and visualization of rule-based models. Although examples are given, using specific implementations the proposed techniques can be applied to rule-based models in general. Availability and implementation: The annotation ontology for rule-based models can be found at http://purl.org/rbm/rbmo. The krdf tool and associated executable examples are available at http://purl.org/rbm/rbmo/krdf. Contact: [email protected] or [email protected]

scholarly journals REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS

2001 ◽  
Vol 12 (01) ◽  
pp. 69-95 ◽  
Author(s):  
PETER BOROVANSKÝ ◽  
CLAUDE KIRCHNER ◽  
HÉLÈNE KIRCHNER ◽  
CHRISTOPHE RINGEISSEN
Keyword(s):  
Term Rewriting ◽  
Higher Order ◽  
Point Of View ◽  
Starting Point ◽  
Rewrite Rules ◽  
Functional Point ◽  
Text Language

In this work, we consider term rewriting from a functional point of view. A rewrite rule is a function that can be applied to a term using an explicit application function. From this starting point, we show how to build more elaborated functions, describing first rewrite derivations, then sets of derivations. These functions, that we call strategies, can themselves be defined by rewrite rules and the construction can be iterated leading to higher-order strategies. Furthermore, the application function is itself defined using rewriting in the same spirit. We present this calculus and study its properties. Its implementation in the [Formula: see text] language is used to motivate and exemplify the whole approach. The expressiveness of [Formula: see text] is illustrated by examples of polymorphic functions and strategies.

Sign in / Sign up

Export Citation Format

Share Document