Paolo Baldan

Deducing Interactions in Partially UnspecifiedBiological Systems (2008)

and Barbara K"onig 4

P. Baldan, Behaviour-preserving Reconfigurations, Paolo Baldan, Andrea Corradini, Hartmut Ehrig, Reiko Heckel, ...

Abstract. We propose a framework for the specification of behaviourpreserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of...

Paolo Baldan, Andrea Bracciali, Linda Brodo, Roberto Bruni

Abstract. We show how a symbolic approach to the semantics of process alge-bras can be fruitfully applied to the modeling and analysis of partially unspecified biological systems, i.e., systems whose...

Paolo Baldan, Andrea Corradini, Hartmut Ehrig, Reiko Heckel, Barbara König

Abstract. We propose a framework for the specification of behaviourpreserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of...

Baldan, Paolo, Corradini, Andrea, Ehrig, Hartmut, Heckel, Reiko, König, Barbara

We propose a framework for the specification of behaviour-preserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of ordinary...

and Backwards? (2008)

Paolo Baldan, Andrea Corradini, Ugo Montanari, Leila Ribeiro, Paolo Baldan, Andrea Corradini, ...

List of Tables (2008)

Paolo Baldan, Giorgio Ghelli, Ra Raffaet À, Giorgio Ghelli

1 A pictorial representation of rule II.5: the two subtyping derivations (∀α≤ c1. d1);(∀α≤c2. d2) and ∀α≤(c1[α≤A ′ ←c2]).(d1[α≤A ′ ←c2]; d2)...... 21 2 The equational...

Deducing Interactions in Partially Unspecified Biological Systems (2008)

Paolo Baldan, Andrea Bracciali, Linda Brodo, Roberto Bruni

Abstract. We show how a symbolic approach to the semantics of process algebras can be fruitfully applied to the modeling and analysis of partially unspecified biological systems, i.e., systems whose...

Reversing graph transformations 2 (2008)

Paweł Sobociński, Paolo Baldan, Hartmut Ehrig, Julia Padberg, Grzegorz Rozenberg, Tiziana Margaria, ...

a general framework for backtracking in concurrent formalisms, thus allowing modelling of situations where deadlock can arise without the necessity of explicitly encoding the often involved...

Graph Transactions as Processes ⋆ (2008)

Paolo Baldan, Andrea Corradini, Luciana Foss, Fabio Gadducci

Abstract. Transactional graph transformation systems (t-gtss) have been recently proposed as a mild extension of the standard dpo approach to graph transformation, equipping it with a suitable notion...

Modelling Calculi with Name Mobility using Graphs with Equivalences (2008)

Paolo Baldan, Fabio Gadducci, Ugo Montanari

In the theory of graph rewriting, the use of coalescing rules, i.e., of rules which besides deleting and generating graph items, can coalesce some parts of the graph, turns out to be quite useful for...

McMillan’s Complete Prefix for Contextual Nets ⋆ (2008)

Paolo Baldan, Andrea Corradini, Barbara König, Stefan Schwoon

Abstract. In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finitestate) Petri nets, which can be used for verification...

Event Structure Semantics for Dynamic Graph Grammars (2008)

Roberto Bruni, Hernán Melgratti, Ugo Montanari, Paolo Baldan, Hartmut Ehrig, Julia Padberg, ...

Abstract: Dynamic 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....

Pre-nets, read arcs and unfolding: a functorial presentation Extended abstract (2008)

Paolo Baldan, Roberto Bruni, Ugo Montanari

P/T Petri nets are one of the most widely known models of concurrency. Since their introduction [Pet62], the conceptual simplicity of the model and its intuitive graphical presentation have attracted...

Deducing Interactions in Partially UnspecifiedBiological Systems (2008)

Paolo Baldan, Andrea Bracciali, Linda Brodo, Roberto Bruni

Abstract. We show how a symbolic approach to the semantics of process alge-bras can be fruitfully applied to the modeling and analysis of partially unspecified biological systems, i.e., systems whose...

Deducing Interactions in Partially Unspecified Biological Systems (2008)

Paolo Baldan, Andrea Bracciali, Linda Brodo, Roberto Bruni

Abstract. We show how a symbolic approach to the semantics of process algebras can be fruitfully applied to the modeling and analysis of partially unspecified biological systems, i.e., systems whose...

Symbolic Equivalences for Open Systems\Delta (2008)

Paolo Baldan, Andrea Bracciali, Roberto Bruni, Dipartimento Informatica, Foscari Venezia

1 Introduction The widespread diffusion of web applications and mobile devices has shiftedthe attention to open systems, i.e., systems where mobile software components can be dynamically connected to...

Pre-nets, read arcs and unfolding: a functorial presentation (2008)

Paolo Baldan, Roberto Bruni, Ugo Montanari

Abstract. Pre-nets have been recently proposed as a means of providing a functorial algebraic semantics to Petri nets (possibly with read arcs), overcoming some previously unsolved subtleties of the...

Open Systems (2008)

Abstract UniGra’03 Preliminary Version Towards Unfolding-Based Verification for Graph Transformation Systems (2008)

(1) Dipartimento di Informatica, Universit`a Ca ' Foscari di Venezia (2)

Paolo Baldan, Andrea Corradini, Barbara König, Baldan Corradini König

The unfolding semantics of graph transformation systems can represent a basis for their formal verification. For general, possibly infinite-state, graph transformation systems one can construct...

UNIVERSIT A DI PISA (2007)

Fabio Alessi, Fabio Alessi, Paolo Baldan, Paolo Baldan, Furio Honsell, Furio Honsell

In this paper we introduce SFP

A Characterization of Distance between 1-Bounded Compact Ultrametric Spaces through a Universal Space (2007)

Fabio Alessi, Paolo Baldan

The category of 1-bounded compact ultrametric spaces and non-distance increasing functions (KUM's) have been extensively used in the semantics of concurrent programming languages. In this paper...

and (2007)

Replace this le with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting.

1 (2007)

UniGra'03 Preliminary Version Towards Unfolding-Based Verication for Graph Transformation Systems (2007)

Abstract. We propose a framework where behavioural properties of nite-state systems modelled as graph transformation systems can be expressed and veried. The technique is based on the unfolding...

Deducing interactions in partially unspecified biological systems (2007)

The unfolding semantics of graph transformation systems can represent a basis for their formal verication. For general, possibly innite-state, graph transformation systems one can construct nite...

Baldan, Paolo, Bracciali, Andrea, Brodo, Linda, Bruni, Roberto

We show how a symbolic approach to the semantics of process algebras can be fruitfully applied to the modeling and analysis of partially unspecified biological systems, i.e., systems whose components...

Processes for adhesive rewriting systems (2006)

Paolo Baldan, Andrea Corradini, Tobias Heindel, Barbara König

Abstract. Rewriting systems over adhesive categories have been recently introduced as a general framework which encompasses several rewriting-based computational formalisms, including various...

Concurrent rewriting for graphs with equivalences (2006)

Paolo Baldan, Fabio Gadducci, Ugo Montanari

Abstract. Several applications of graph rewriting systems (notably, some encodings of calculi with name passing) require rules which, besides deleting and generating graph items, are able to coalesce...

Distributed unfolding of Petri nets (2006)

Paolo Baldan, Stefan Haar, Barbara König

Abstract. Petri net unfoldings have been recognised as an efficient means to fight state space explosion when dealing with concurrent and distributed systems. Some recent Petri net-based approaches...

A temporal graph logic for verification of graph transformation systems (2006)

Paolo Baldan, Andrea Corradini, Barbara König, Alberto Lluch Lafuente

Abstract. We extend our approach for verifying properties of graph transformation systems using suitable abstractions. In the original approach properties are specified as formulae of a propositional...

Verifying a Behavioural Logic for Graph Transformation Systems (2006)

Paolo Baldan, Andrea Corradini, Barbara König, Bernhard König

A rewriting calculus for cyclic higher-order term graphs (2005)

Baldan, Paolo, Bertolissi, Clara, Cirstea, Horatiu, Kirchner, Claude

Introduced at the end of the nineties, the Rewriting Calculus (rho-calculus, for short) fully integrates term-rewriting and lambda-calculus. The rewrite rules, acting as elaborated abstractions,...

A rewriting calculus for cyclic higher-order term graphs (2005)

Baldan, Paolo, Bertolissi, Clara, Cirstea, Horatiu, Kirchner, Claude

Introduced at the end of the nineties, the Rewriting Calculus (rho-calculus, for short) fully integrates term-rewriting and lambda-calculus. The rewrite rules, acting as elaborated abstractions,...

A rewriting calculus for cyclic higher-order term graphs (2005)

Baldan, Paolo, Bertolissi, Clara, Cirstea, Horatiu, Kirchner, Claude

Introduced at the end of the nineties, the Rewriting Calculus (rho-calculus, for short) fully integrates term-rewriting and lambda-calculus. The rewrite rules, acting as elaborated abstractions,...

Specifying and verifying UML activity diagrams via graph transformation (2005)

Paolo Baldan, Andrea Corradini, Fabio Gadducci

1 Dipartimento di Informatica, Universit`a Ca ' Foscari di Venezia, Italy 2 Dipartimento di Informatica, Universit`a di Pisa, Italy

Graph grammar verification through abstraction (summary 2 (2005)

Paolo Baldan, Barbara König, Arend Rensink

Abstract. Until now there have been few contributions concerning the verification of graph grammars, specifically of infinite-state graph grammars. This paper compares two existing approaches, based...

Verifying red-black trees (2005)

Paolo Baldan, Andrea Corradini, Javier Esparza, Tobias Heindel, Barbara König, Vitali Kozioura

Abstract. We show how to verify the correctness of insertion of elements into red-black trees—a form of balanced search trees—using analysis techniques developed for graph rewriting. We first...

Symbolic equivalences for open systems (2005)

Summary 2: Graph Grammar Verification through Abstraction (2005)

Abstract. Behavioural equivalences on open systems are usually defined by comparing system behaviour in all environments. Due to this “universal ” quantification over the possible hosting...

Baldan, Paolo, König, Barbara, Rensink, Arend

Until now there have been few contributions concerning the verification of graph grammars, specifically of infinite-state graph grammars. This paper compares two existing approaches, based on...

A rewriting calculus for cyclic higher-order term graphs (2004)

Paolo Baldan, Clara Bertolissi, Claude Kirchner

graphs

Verifying finite-state graph grammars: an unfolding-based approach (2004)

Verifying finite-state graph grammars: an unfolding-based approach (2004)

an Unfolding-Based Approach?

Paolo Baldan, Andrea Corradini, Barbara König

Abstract. We propose a framework where behavioural properties of finite-state systems modelled as graph transformation systems can be expressed and verified. The technique is based on the unfolding...

Generating test cases for code generators by unfolding graph transformation systems (2004)

Paolo Baldan, Barbara König, Ingo Stürmer

Abstract. Code generators are widely used in the development of embedded software to automatically generate executable code from graphical specifications. However, at present, code generators are not...

A logic for analyzing abstractions of graph transformation systems (2003)

Paolo Baldan

3 1 Dipartimento di Informatica, Universit`a Ca ' Foscari di Venezia, Italy 2 Institut f"ur Informatik, Technische Universit"at M"unchen, Germany

A logic for analyzing abstractions of graph transformation systems (2003)

Paolo Baldan

3 1 Dipartimento di Informatica, Universit`a Ca ' Foscari di Venezia, Italy 2 Institut f"ur Informatik, Technische Universit"at M"unchen, Germany

Coreflective concurrent semantics for single-pushout graph grammars (2003)

Paolo Baldan, Andrea Corradini, Ugo Montanari, Leila Ribeiro

Abstract. The problem of extending to graph grammars the unfolding semantics originally developed by Winskel for (safe) Petri nets has been faced several times along the years, both for the...

A Logic for Analyzing Abstractions of Graph Transformation Systems (2003)

Paolo Baldan, Barbara König, Bernhard König

A technique for approximating the behaviour of graph transformation systems (GTSs) by means of Petri net-like structures has been recently de ned in the literature. In this paper we introduce a...

A logic for analyzing abstractions of graph transformation systems (2003)

Paolo Baldan, Barbara König, Bernhard König

Abstract. A technique for approximating the behaviour of graph transformation systems (GTSs) by means of Petri net-like structures has been recently defined in the literature. In this paper we...

Bisimulation by unification (2002)

Static analysis of distributed systems with mobility specified by graph grammars—a case study (2002)

Abstract. We propose a methodology for the analysis of open systems based on process calculi and bisimilarity. Open systems are seen as coordinators (i.e. terms with place-holders), that evolve when...

Specified Graph, Paolo Baldan, Andrea Corradini

ABSTRACT:We consider a distributed system with mobility modelled as a graph transformation system. Then we show that non-secure level processes cannot influence secure level processes, a property...

DOI: 10.1017/S0960129504004311 Printed in the United Kingdom Compositional semantics for open Petri nets based on deterministic processes † (2002)

Bisimulation by unification (2002)

In order to model the behaviour of open concurrent systems by means of Petri nets, we introduce open Petri nets, a generalisation of the ordinary model where some places, designated as open,...

Approximating the Behaviour of Graph Transformation Systems (2002)

Abstract. We propose a methodology for the analysis of open systems based on process calculi and bisimilarity. Open systems are seen as coordinators (i.e. terms with place-holders), that evolve when...

Paolo Baldan, Barbara König

We propose a technique for the analysis of graph transformation systems which relies on the construction of nite structures approximating the behaviour of such systems with arbitrary accuracy.

Bisimulation by unification (2002)

Approximating the behaviour of graph transformation systems (2002)

Abstract We propose a methodology for the analysis of open systems based on process calculi and bisimilarity. Open systems are seen as coordinators (i.e. terms with place-holders), that evolve when...

Paolo Baldan, Barbara König

Abstract. We propose a technique for the analysis of graph transformation systems based on the construction of finite structures approximating the behaviour of such systems with arbitrary accuracy....

A category of compositional domain-models for separable (2001)

Stone Spaces, Fabio Alessi, Paolo Baldan, Furio Honsell

In this paper we introduce SFP M, a category of SFP domains which provides very satisfactory domain-models, i.e. “partializations”, of separable Stone spaces (2-Stone spaces). More specifically,...

Contextual petri nets, asymmetric event structures and processes (2001)

A static analysis technique for graph transformation systems (2001)

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...

A static analysis technique for graph transformation systems (2001)

Abstract. In this paper we introduce a static analysis technique for graph transformation systems. We present an algorithm which, given a graph transformation system and a start graph, produces a...

Paolo Baldan, Andrea Corradini, Barbara König

Abstract. In this paper we introduce a static analysis technique for graph transformation systems. We present an algorithm which, given a graph transformation system and a start graph, produces a...

Unfolding of Double-Pushout Graph Grammars is a Coreflection (2000)

History Preserving Bisimulation for Contextual Nets (2000)

. In a recent paper, mimicking Winskel's construction for Petri nets, a concurrent semantics for (double-pushout) DPO graph grammars has been provided by showing that each graph grammar can be...

Basic theory of F-bounded quantification (1999)

. We investigate the notion of history preserving bisimulation [15, 18, 3] for contextual P/T nets, a generalization of ordinary P/T Petri nets where a transition may check for the presence of tokens...

Paolo Baldan, Giorgio Ghelli, Alessandra Raffaetà, Ra Raffaet

System F-bounded is a second order typed lambda calculus, where the basic features of object-oriented languages can be naturally modelled. F-bounded extends the better known system F , in a way that...

Contextual Petri Nets, Asymmetric Event Structures, and Processes (1999)

Paolo Baldan, Andrea Corradini, U. Montanari, 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 theory of F-bounded quantification (1999)

Paolo Baldan, Ra Raffaet, Alessandra Raffaetà, Giorgio Ghelli, Giorgio Ghelli

System F-bounded is a second order typed lambda calculus, where the basic features of object-oriented languages can be naturally modelled.

Unfolding and Event Structure Semantics for Graph Grammars (1999)

An Event Structure Semantics for P/T Contextual Nets: Asymmetric Event Structures (1998)

. We propose an unfolding semantics for graph transformation systems in the double-pushout (DPO) approach. Mimicking Winskel's construction for Petri nets, a graph grammar is unfolded into an...

Concatenable Graph Processes: Relating Processes and Derivation Traces (1998)

. We propose an event based semantics for contextual nets, i.e. an extension of Place/Transition Petri nets where transitions can also have context conditions, modelling resources that can be read...