1,721,281 research outputs found
Jungle Rewriting: an Abstract Description of a Lazy Narrowing Machine
No full textWe propose to use Jungle Rewriting, a graph rewriting formalism, as a formal specification tool for the LANAM, an abstract machine implementing lazy narrowing. Three jungle rewriting systems which model a narrowing program at different levels of abstraction are presented. The first system is proved to be essentially equivalent (from an operational point of view) to the given program. The second one contains only rules which correspond to elementary actions of a narrowing interpreter, while the third one also models the control issues of the abstract machine. We formally prove the equivalence of the first and second systems, while the relationship between the second and the third one is sketched. The last system provides an abstract description of the compiled code of the LANAM, which is outline
Abstract Graph Derivations in the Double Pushout Approach
No full textIn the algebraic theory of graph grammars, it is common practice to present some notions or results “up to isomorphism”. This allows one to reason about graphs and graph derivations without worrying about representation-dependent details.
Motivated by a research activity aimed at providing graph grammars with a truly-concurrent semantics, we front in this paper the problem of formalizing what does it mean precisely to reason about graph derivations “up to isomorphism”. This needs the definition of a suitable equivalence on derivations, which should be consistent with the relevant definitions and results, in the sense that they should extend to equivalence classes. After showing that a naive equivalence is not satisfactory, we propose two requirements for equivalences on derivations which allow the sequential composition of derivations and guarantee the uniqueness of canonical derivations, respectively. Three new equivalences are introduced, the third of which is shown to be satisfy both requirements. We also define a new category having the abstract derivations as arrows, which is, in our view, a fundamental step towards the definition of a truly-concurrent semantics for graph grammars
Zero-Safe Nets: Composing Nets via Transition Synchronization
No full textZero-safe nets have been introduced to extend classical Petri nets with a primitive notion of transition synchronization. To this aim, besides ordinary places, called stable, zero-safe nets are equipped with zero places, which cannot contain any token in a stable marking . An evolution between two stable markings is called transaction and can be a complex computation that involves zero places, with the restriction that no stable token generated in a transaction can be reused in the same transaction. The abstract counterpart of a generic zerosafe net B consists of an ordinary pt net whose places are the stable places of B, and whose transitions are the transactions of B. The two nets offer the refined and the abstract model of the same system, where the former can be much smaller than the latter, because of the transition synchronization mechanism. Depending on the chosen approach --- collective vs individual token philosophy --- two notions of transaction may be defined, each leading ..
Dynamic Graph Transformation Systems
No full textWe introduce an extension of Graph Grammars (GGs), called Dynamic Graph Grammars (DynGGs), where the right-hand side of a production can spawn fresh parts of the type graph and fresh productions operating on it. The features of DynGGs make them suitable for the straightforward modeling of reflexive mobile systems like dynamic nets and the join calculus. Our main result shows that each DynGG can be modeled as a (finite) GG, so that the dynamically generated structure can be typed statically, still preserving exactly all derivations
Modeling a Service and Session Calculus with Hierarchical Graph Transformation
Full text linkGraph transformation techniques have been applied successfully to the modelling of process calculi, for example for equipping them with a truly concurrent semantics. Recently, there has been an increasing interest towards hierarchical structures both at the level of graph-based models, in order to represent explicitly the interplay between linking and containment (like in Milner’s bigraphs), and at the level of process calculi, in order to deal with several logical notions of scoping (ambients, sessions and transactions, among others). In this paper we show how to encode a sophisticated calculus of services and nested sessions by exploiting a suitable flavour of hierarchical graphs. For the encoding of the processes of this calculus we benefit from a recently proposed algebra of graphs with nesting
Event Structure Semantics for Dynamic Graph Grammars
Full text linkDynamic graph grammars (DGGs) are a reflexive extension of Graph Grammars that have been introduced to represent mobile reflexive systems and calculi at a convenient level of abstraction. Persistent graph grammars (PGGs) are a class of graph grammars that admits a fully satisfactory concurrent semantics thanks to the fact that all so-called asymmetric conflicts (between items that are read by some productions and consumed by other) are avoided. In this paper we introduce a slight variant of DGGs, called persistent dynamic graph grammars (PDGGs), that can be encoded in PGGs preserving concurrency. Finally, PDGGs are exploited to define a concurrent semantics for the join calculus enriched with persistent messaging (if preferred, the latter can be naively seen as dynamic nets with read arcs)
COMPATIBILITY PROBLEMS IN THE DEVELOPMENT OF ALGEBRAIC MODULE SPECIFICATIONS
No full textAlgebriac theory provides a framework for the specification and design of modules and modular software systems. Research in this area has focused on the development of "horizontal" operations for building up module and interface specifications. Our previous work also introduced the notion of vertical development steps, where abstract specifications are converted into a more concrete form. In this paper, we study a variety of compatibility problems between structuring operations and development steps and introduce notions of the realization of an interface specification by a module specification. These compatibility problems are studied in a categorical framework where specifications and developments steps are viewed as objects and morphisms in a "development category". We show that compatibility can be expressed as the fact that the structuring operations can be extended to partial functors and give sufficient conditions for this property
Sesqui-Pushout Rewriting
No full textSesqui-pushout (SqPO) rewriting - "sesqui" means "one and a half" in Latin - is a new algebraic approach to abstract rewriting in any category. SqPO rewriting is a deterministic and conservative extension of double-pushout (DPO) rewriting, which allows to model "deletion in unknown context", a typical feature of single-pushout (SPO) rewriting, as well as cloning. After illustrating the expressiveness of the proposed approach through a case study modelling an access control system, we discuss sufficient conditions for the existence of final pullback complements and we analyze the relationship between SqPO and the classical DPO and SPO approaches
- …
