Andrea Corradini

I&C Journal 2021 Journal Article

Concurrent semantics for fusions: Weak prime domains and connected event structures

• Paolo Baldan
• Andrea Corradini
• Fabio Gadducci

Stable event structures, and their duality with prime algebraic domains, represent a landmark of concurrency theory, since they provide a neat characterisation of causality in computations. As such, they have been used for defining the concurrent semantics of many formalisms, from Petri nets to (linear) graph rewriting systems. Stability however is restrictive for formalisms with “fusion”, where a computational step may merge parts of the state. This happens e. g. for graph rewriting systems with non-linear rules, which are used to cover some relevant applications (such as the graphical encoding of calculi with name passing). Guided by the need of giving semantics to such formalisms, we leave aside stability and characterise a class of domains, referred to as weak prime domains, naturally generalising prime algebraic domains. We then identify a corresponding class of event structures, that we call connected event structures, via a duality result formalised as an equivalence of categories.

TCS Journal 2020 Journal Article

Algebraic graph rewriting with controlled embedding

• Andrea Corradini
• Dominique Duval
• Rachid Echahed
• Frédéric Prost
• Leila Ribeiro

Graph transformation is a specification technique suitable for a wide range of applications, specially the ones that require a sophisticated notion of state. In graph transformation, states are represented by graphs and actions are specified by rules. Most algebraic approaches to graph transformation proposed in the literature ensure that if an item is preserved by a rule, so are its connections with the graph where it is embedded. But there are applications in which it is desirable to specify different embeddings. For example when cloning an item, there may be a need to handle the original and the copy in different ways. We propose a new algebraic approach to graph transformation, AGREE: Algebraic Graph Rewriting with controllEd Embedding, where rules allow one to specify how the embedding should be carried out. We define this approach in the framework of classified categories which are categories endowed with partial map classifiers. This new approach leads to graph transformations in which effects may be non-local, e. g. a rewrite step may alter a node of the host graph which is outside the image of the left-hand side of the considered rule. We propose a syntactic condition on AGREE rules which guarantees the locality of transformations. We also compare AGREE with other algebraic approaches to graph transformation.

TCS Journal 2012 Journal Article

Efficient unfolding of contextual Petri nets

• Paolo Baldan
• Alessandro Bruni
• Andrea Corradini
• Barbara König
• César Rodríguez
• Stefan Schwoon

A contextual net is a Petri net extended with read arcs, which allows transitions to check for tokens without consuming them. Contextual nets allow for better modelling of concurrent read access than Petri nets, and their unfoldings can be exponentially more compact than those of a corresponding Petri net. A constructive but abstract procedure for generating those unfoldings was proposed in previous work. However, it remained unclear whether the approach was useful in practice and which data structures and algorithms would be appropriate to implement it. Here, we address this question. We provide two concrete methods for computing contextual unfoldings, with a view to efficiency. We report on experiments carried out on a number of benchmarks. These show that not only are contextual unfoldings more compact than Petri net unfoldings, but they can be computed with the same or better efficiency, in particular with respect to alternative approaches based on encodings of contextual nets into Petri nets.

I&C Journal 2008 Journal Article

A framework for the verification of infinite-state graph transformation systems

• Paolo Baldan
• Andrea Corradini
• Barbara König

We propose a technique for the analysis of infinite-state graph transformation systems, based on the construction of finite structures approximating their behaviour. Following a classical approach, one can construct a chain of finite under-approximations (k-truncations) of the Winskel style unfolding of a graph grammar. More interestingly, also a chain of finite over-approximations (k-coverings) of the unfolding can be constructed. The fact that k-truncations and k-coverings approximate the unfolding with arbitrary accuracy is formalised by showing that both chains converge (in a categorical sense) to the full unfolding. We discuss how the finite over- and under-approximations can be used to check properties of systems modelled by graph transformation systems, illustrating this with some small examples. We also describe the Augur tool, which provides a partial implementation of the proposed constructions, and has been used for the verification of larger case studies.

I&C Journal 2007 Journal Article

Unfolding semantics of graph transformation

• Paolo Baldan
• Andrea Corradini
• Ugo Montanari
• Leila Ribeiro

Several attempts have been made of extending to graph grammars the unfolding semantics originally developed by Winskel for (safe) Petri nets, but only partial results were obtained. In this paper, we fully extend Winskel’s approach to single-pushout grammars providing them with a categorical concurrent semantics expressed as a coreflection between the category of (semi-weighted) graph grammars and the category of prime algebraic domains, which factorises through the category of occurrence grammars and the category of asymmetric event structures. For general, possibly nonsemi-weighted single-pushout grammars, we define an analogous functorial concurrent semantics, which, however, is not characterised as an adjunction. Similar results can be obtained for double-pushout graph grammars, under the assumptions that nodes are never deleted.

TCS Journal 2002 Journal Article

A functorial semantics for multi-algebras and partial algebras, with applications to syntax

• Andrea Corradini
• Fabio Gadducci

Multi-algebras allow for the modelling of nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results. We propose a functorial presentation of various categories of multi-algebras and partial algebras, analogous to the classical presentation of algebras over a signature Σ as cartesian functors from the algebraic theory over Σ to Set. We introduce two different notions of theory over a signature, both having a structure weaker than cartesian, and we consider functors from them to Rel or Pfn, the categories of sets and relations or partial functions, respectively. Next we discuss how the functorial presentation provides guidelines when choosing syntactical notions for a class of algebras, and as an application we argue that the natural generalization of usual terms are “conditioned terms” for partial algebras, and “term graphs” for multi-algebras.

TCS Journal 2002 Journal Article

Compositional SOS and beyond: a coalgebraic view of open systems

• Andrea Corradini
• Reiko Heckel
• Ugo Montanari

In this paper we address the issue of providing a structured coalgebra presentation of transition systems with algebraic structure on states determined by an equational specification Γ. More precisely, we aim at representing such systems as coalgebras for an endofunctor on the category of Γ-algebras. The systems we consider are specified by using arbitrary SOS rules, which in general do not guarantee that bisimilarity is a congruence. We first show that the structured coalgebra representation works only for systems where transitions out of complex states can~be derived from transitions out of corresponding component states. This decomposition property of transitions indeed ensures that bisimilarity is a congruence. For a system not satisfying this requirement, next we propose a closure construction which adds context transitions, i. e. , transitions that spontaneously embed a state into a bigger context or vice versa. The notion of bisimulation for the enriched system coincides with the notion of dynamic bisimilarity for the original one, i. e. , with the coarsest bisimulation which is a congruence. This is sufficient to ensure that the structured coalgebra representation works for the systems obtained as result of the closure construction.

TCS Journal 2001 Journal Article

A Coalgebraic presentation of structured transition systems

• Andrea Corradini
• Martin Große-Rhode
• Reiko Heckel

This paper relates labelled transition systems and coalgebras with the motivation of comparing and combining their complementary contributions to the theory of concurrent systems. The well-known mismatch between these two notions concerning the morphisms is resolved by extending the coalgebraic framework by lax cohomomorphisms. Enriching both labelled transition systems and coalgebras with algebraic structure for an algebraic specification, the correspondence is lost again. This motivates the introduction of lax coalgebras, where the coalgebra structure is given by a lax homomorphism. The resulting category of lax coalgebras and lax cohomomorphisms for a suitable endofunctor is shown to be isomorphic to the category of structured transition systems, where both states and transitions form algebras. The framework is also presented on a more abstract categorical level using monads and comonads, extending the bialgebraic approach introduced by Turi and Plotkin.

I&C Journal 2001 Journal Article

Contextual Petri Nets, Asymmetric Event Structures, and Processes

• Paolo Baldan
• Andrea Corradini
• Ugo Montanari

We present an event structure semantics for contextual nets, an extension of P/T Petri nets where transitions can check for the presence of tokens without consuming them (read-only operations). A basic role is played by asymmetric event structures, a generalization of Winskel's prime event structures where symmetric conflict is replaced by a relation modelling asymmetric conflict or weak causality, used to represent a new kind of dependency between events arising in contextual nets. Extending Winskel's seminal work on safe nets, the truly concurrent event-based semantics of contextual nets is given at categorical level via a chain of coreflections leading from the category SW-CN of semi-weighted contextual nets to the category Dom of finitary prime algebraic domains. First an unfolding construction generates from a contextual net a corresponding occurrence contextual net, from where an asymmetric event structure is extracted. Then the configurations of the asymmetric event structure, endowed with a suitable order, are shown to form a finitary prime algebraic domain. We also investigate the relation between the proposed unfolding semantics and several deterministic process semantics for contextual nets in the literature. In particular, the domain obtained via the unfolding is characterized as the collection of the deterministic processes of the net endowed with a kind of prefix ordering.

TCS Journal 1998 Journal Article

Contents and abstracts of the electronic notes in Theoretical Computer Science vol. 2

• Andrea Corradini
• Ugo Montanari

TCS Journal 1994 Journal Article

An abstract machine for concurrent modular systems: CHARM

• Andrea Corradini
• Ugo Montanari
• Francesca Rossi

CHARM (for concurrency and hiding in an abstract rewriting machine) is an abstract machine which allows one to model naturally the behavior of distributed systems consisting of a collection of processes-sharing variables. CHARM is equipped with a clean operational semantics based on term rewriting over a suitable algebra, and it exhibits a sophisticated treatment of concurrency and modularity, which is obtained through the partition of each state into a global and a local part. To show the expressiveness and generality of this abstract machine, three relevant computational formalisms are mapped onto the CHARM framework: graph grammars, concurrent constraint programming, and place/transition Petri nets.

TCS Journal 1993 Journal Article

Hyperedge replacement jungle rewriting for term-rewriting systems and logic programming

• Andrea Corradini
• Francesca Rossi

We introduce hyperedge replacement jungle rewriting, a graph-rewriting formalism suitable for modeling the manipulation of terms and similar structures, and investigate its expressive power by showing that it can model both term-rewriting systems and logic programming in a faithful way. For term-rewriting systems we prove the soundness of their jungle representation, and a result of completeness w. r. t. applicability which is stronger than similar results in the related literature, since it works also for non-left-linear rules. For logic programming both soundness and completeness hold.

TCS Journal 1992 Journal Article

An algebraic semantics for structured transition systems and its application to logic programs

• Andrea Corradini
• Ugo Montanari

We present a general methodology aimed at providing an algebraic semantics for a large class of formalisms. The methodology, which generalizes the algebraic treatment of Petri nets proposed by Meseguer and Montanari (1990) individuates three levels of description of a formalism (i. e. , programs, structured transitions systems, and models), and defines two free constructions which generate in an automatic way the induced transition system and the free model of a program. These constructions are parametric with respect to the structure of states and transitions: instantiating them in various ways, different formalisms can be treated. The construction of the free model extends the algebraic structure of transitions to the computations of a program, thus producing a category having as arrows abstract computations, i. e. , equivalence classes of concrete computations. Interestingly, the equivalence relation induced on computations captures some basic properties of true concurrency. Moreover, by general categorical properties the construction of the free model is compositional w. r. t. various forms of program union. As a running example, we apply the methodology to phrase structure grammars, while the main case study is logic programming. For both formalisms the free model is shown to include all the computations at a natural level of abstraction: the free model of a grammar includes all its derivation trees as arrows, while the arrows of the free model of a logic program are parallel refutations.