15 Result(s)
within
Conference Paper
Roberto Bruni
Software Engineering/Programming and Operating Systems
-
Chapter and Conference Paper
Exploiting Adjoints in Property Directed Reachability Analysis
We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley’s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-...
-
Chapter and Conference Paper
Exploiting Modularity of SOS Semantics to Define Quantitative Extensions of Reaction Systems
Reaction Systems (RSs) are a successful natural computing framework inspired by chemical reaction networks. A RS consists of a set of entities and a set of reactions. Entities can enable or inhibit each reacti...
-
Chapter and Conference Paper
First-Order Dynamic Logic for Compensable Processes
Compensable programs offer a convenient paradigm to deal with long-running transactions, because they offer a structured and modular approach to the composition of distributed transactional activities, like se...
-
Chapter and Conference Paper
Service Oriented Architectural Design
We propose Architectural Design Rewriting (ADR), an approach to formalise the development and reconfiguration of software architectures based on term-rewriting. An architectural style consists of a set of archite...
-
Chapter and Conference Paper
Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines
The notion of a session is fundamental in service-oriented applications, as it serves to separate interactions between clients and different instances of the same service, and to group together logical units o...
-
Chapter and Conference Paper
Sessions and Pipelines for Structured Service Programming
Service-oriented computing is calling for novel computational models and languages with primitives for client-server interaction, orchestration and unexpected events handling. We present CaSPiS, a process calculu...
-
Chapter and Conference Paper
PRISMA: A Mobile Calculus with Parametric Synchronization
We present PRISMA, a parametric calculus that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). We define both operational semantics an...
-
Chapter and Conference Paper
Symbolic Equivalences for Open Systems
Behavioural equivalences on open systems are usually defined by comparing system behaviour in all environments. Due to this “universal” quantification over the possible hosting environments, such equivalences ...
-
Chapter and Conference Paper
Pre-nets, Read Arcs and Unfolding: A Functorial Presentation
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 classical model. Her...
-
Chapter and Conference Paper
Generalized Rewrite Theories
Since its introduction, more than a decade ago, rewriting logic has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framewor...
-
Chapter and Conference Paper
Bisimulation by Unification*
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 suitable components ...
-
Chapter and Conference Paper
Algebraic Models for Contextual Nets
We extend the algebraic approach of Meseguer and Montanari from ordinary place/transition Petri nets to contextual nets, covering both the collective and the individual token philosophy uniformly along the two in...
-
Chapter and Conference Paper
Normal Forms for Partitions and Relations
Recently there has been a growing interest towards algebraic structures that are able to express formalisms different from the standard, tree-like presentation of terms. Many of these approaches reveal a speci...
-
Chapter and Conference Paper
Executable Tile Specifications for Process Calculi
Tile logic extends rewriting logic by taking into account side-effects and rewriting synchronization. These aspects are very important when we model process calculi, because they allow us to expr...
-
Chapter and Conference Paper
Zero-safe nets: The individual token approach
In this paper we provide both an operational and an abstract concurrent semantics for zero-safe nets under the individual token philosophy. The main feature of zero-safe nets is a primitive notion of transition s...
