2,731 research outputs found
Editorial for the Special Issue on Open Problems in Concurrency Theory
No full text“Special Issue on Open Problems in Concurrency Theory”
Edited by Marco Bernardo, Daniel Gebler and Michele Loret
Implementing Session Centered Calculi
No full textRecently, specific attention has been devoted to the development of service oriented process calculi. Besides the foundational aspects, it is also interesting to have prototype implementations for them in order to assess usability and to minimize the gap between theory and practice. Typically, these implementations are done in Java taking advantage of its mechanisms supporting network applications. However, most of the recurrent features of service oriented applications are re-implemented from scratch. In this paper we show how to implement a service oriented calculus, CaSPiS (Calculus of Services with Pipelines and Sessions) using the Java framework IMC, where recurrent mechanisms for network applications are already provided. By using the session oriented and pattern matching communication mechanisms provided by IMC, it is relatively simple to implement in Java all CaSPiS abstractions and thus to easily write the implementation in Java of a CaSPiS process
Preface
No full textPreface of Proceedings of ICTCS 2015, the 16th Italian Conference on Theoretical Computer Science
Replicated computations results (RCR) Report for "statistical abstraction for multi-scale spatio-t Systems"
Full text link“Statistical abstraction for multi-scale spatio-temporal systems” proposes a methodology that supports analysis of large-scaled spatio-temporal systems. These are represented via a set of agents whose behaviour depends on a perceived field. The proposed approach is based on a novel simulation strategy based on a statistical abstraction of the agents. The abstraction makes use of Gaussian Processes, a powerful class of non-parametric regression techniques from Bayesian Machine Learning, to estimate the agent’s behaviour given the environmental input. The authors use two biological case studies to show how the proposed technique can be used to speed up simulations and provide further insights into model behaviour. This replicated computation results report focuses on the scripts used in the paper to perform such analysis. The required software was straightforward to install and use. All the experimental results from the paper have been reproduced
A uniform definition of stochastic process calculi
Full text linkWe introduce a unifying framework to provide the semantics of process algebras, including their quantitative variants useful for modeling quantitative aspects of behaviors. The unifying framework is then used to describe some of the most representative stochastic process algebras. This
provides a general and clear support for an understanding of their similarities and differences. The framework is based on State to Function Labeled Transition Systems, FuTSs for short, that are state-transition structures where each transition is a triple of the form (s; α;P). The first andthe second components are the source state, s, and the label, α, of the transition, while the third component is the continuation function, P, associating a value of a suitable type to each state s0. For example, in the case of stochastic process algebras the value of the continuation function on s0 represents the rate of the negative exponential distribution characterizing the duration/delay of the action performed to reach state s0 from s. We first provide the semantics of a simple formalism used to describe Continuous-Time Markov Chains, then we model a number of process algebras that permit parallel composition of models according to the two main interaction paradigms (multiparty and one-to-one synchronization). Finally, we deal with formalisms where actions and rates are kept separate and address the issues related to the coexistence of stochastic, probabilistic, and non-deterministic behaviors. For each formalism, we establish the formal correspondence between the FuTSs semantics and its original semantics
Semantics of the probabilistic Lambda CalculusBy Dirk Draheim
No full textReview of the book "Semantics of the probabilistic Lambda Calculus" By Dirk Draheim: Springer-Verlag, Berlin Heidelberg, DE, 26 January 201
Replicated computations results (RCR) report for “mesoscopic modelling of pedestrian movement using carma and its tools”
No full text“Mesoscopic modeling of pedestrian movement using Carma and its tools” uses Carma (Collective Adaptive Resource-sharing Markovian Agents), a specification language recently introduced for modeling CAS, to model spatially distributed systems in which the desired model lies between an individual-based (microscopic) and a population-based (macroscopic) spatial model. The impact on the system dynamics of changes to the topology of paths is studied via simulation. The provided experiments show that it is difficult to predict the effect of changes to the network structure and that even small variations can produce significant effects. This replicated computations results report focuses on the prototypical tool implementation used in the article to perform such analysis. The software was straightforward to install and use, and all the experimental results from the article could be reproduced
Implementing a distributed mobile calculus using the IMC framework
No full textIn the last decade, many calculi for modelling distributed mobile code have been proposed. To assess their merits and encourage use, implementations of the calculi have often been proposed. These implementations usually consist of a limited part dealing with mechanisms that are specific of the proposed calculus and of a significantly larger part handling recurrent mechanisms that are common to many calculi. Nevertheless, also the "classic" parts are often re-implemented from scratch. In this paper we show how to implement a well established representative of the family of mobile calculi, the distributed [pi]-calculus, by using a Java middleware (called IMC - Implementing Mobile Calculi) where recurrent mechanisms of distributed and mobile systems are already implemented. By means of the case study, we illustrate a methodology to accelerate the development of prototype implementations while concentrating only on the features that are specific of the calculus under consideration and relying on the common framework for all the recurrent mechanisms like network connections, code mobility, name handling, etc
Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
Full text linkOne of the most studied extensions of testing theory to nondeterministic and probabilistic processes yields unrealistic probabilities estimations that give rise to two anomalies. First, probabilistic testing equivalence does not imply probabilistic trace equivalence. Second, probabilistic testing equivalence differentiates processes that perform the same sequence of actions with the same probability but make internal choices in different moments and thus, when applied to processes without probabilities, does not coincide with classical testing equivalence. In this paper, new versions of probabilistic trace and testing equivalences are presented for nondeterministic and probabilistic processes that resolve the two anomalies. Instead of focussing only on suprema and infima of the set of success probabilities of resolutions of interaction systems, our testing equivalence matches all the resolutions on the basis of the success probabilities of their identically labeled computations. A simple spectrum is provided to relate the new relations with existing ones. It is also shown that, with our approach, the standard probabilistic testing equivalences for generative and reactive probabilistic processes can be retrieved
A Spatial Logic for Simplicial Models
Full text linkCollective Adaptive Systems often consist of many heterogeneous components
typically organised in groups. These entities interact with each other by
adapting their behaviour to pursue individual or collective goals. In these
systems, the distribution of these entities determines a space that can be
either physical or logical. The former is defined in terms of a physical
relation among components. The latter depends on logical relations, such as
being part of the same group. In this context, specification and verification
of spatial properties play a fundamental role in supporting the design of
systems and predicting their behaviour. For this reason, different tools and
techniques have been proposed to specify and verify the properties of space,
mainly described as graphs. Therefore, the approaches generally use model
spatial relations to describe a form of proximity among pairs of entities.
Unfortunately, these graph-based models do not permit considering relations
among more than two entities that may arise when one is interested in
describing aspects of space by involving interactions among groups of entities.
In this work, we propose a spatial logic interpreted on simplicial complexes.
These are topological objects, able to represent surfaces and volumes
efficiently that generalise graphs with higher-order edges. We discuss how the
satisfaction of logical formulas can be verified by a correct and complete
model checking algorithm, which is linear to the dimension of the simplicial
complex and logical formula. The expressiveness of the proposed logic is
studied in terms of the spatial variants of classical bisimulation and
branching bisimulation relations defined over simplicial complexes
- …
