1,721,182 research outputs found
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
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
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
Modelling global computations with Klaim
No full textAbstract. A new area of research, known as Global Computing, is by now well established. It aims at defining new models of computation based on code and data mobility over wide-area networks with highly dynamic topologies, and at providing infrastructures to support coordination and control of components originating from different, possibly untrusted, fault-prone, malicious or selfish sources. In this paper, we present our contribution to the field of Global Computing that is centred on Kernel Language for Agents Interaction and Mobility (Klaim ). Klaim is an experimental language specifically designed to programme distributed systems consisting of several mobile components that interact through multiple distributed tuple spaces. We present some of the key notions of the language and discuss how its formal semantics can be exploited to reason about qualitative and quantitative aspects of the specified systems
A modal logic for mobile agents
No full textKlaim is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. The language relies on the use of explicit localities. This paper presents a temporal logic for specifying properties of Klaim programs. The logic is inspired by Hennessy-Milner Logic (HML) and the μ-calculus, but has novel features that permit dealing with state properties and impact of actions and movements over the different sites. The logic is equipped with a complete proof system that enables one to prove properties of mobile systems
Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
Full text linkThe logic PML is a probabilistic version of Hennessy–Milner logic introduced by Larsen and Skou to characterize bisimilarity over probabilistic processes without internal nondeterminism. In this paper, two alternative interpretations of PML over nondeterministic and probabilistic processes as models are considered, and two new bisimulation-based equivalences that are in full agreement with those interpretations are provided. The new equivalences include as coarsest congruences the two bisimilarities for nondeterministic and probabilistic processes proposed by Segala and Lynch. The latter equivalences are instead known to agree with two versions of Hennessy–Milner logic extended with an additional probabilistic operator interpreted over state distributions in place of individual states. The new interpretations of PML and the corresponding new bisimilarities are thus the first ones to offer a uniform framework for reasoning on processes that are purely nondeterministic or reactive probabilistic or that mix nondeterminism and probability in an alternating/nonalternating way
On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination
No full textTypical self-organising collective systems consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. Design of such systems is challenging and requires suitable, scalable analysis tools to check properties of proposed system designs before they are put into operation. We present a novel scalable, on-the-fly approximated model-checking procedure to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model-checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is proven and a prototype implementation of the model-checker is presented. The potential of the verification approach is illustrated by its application on self-organising collective systems and an overview of remaining open issues and future extensions is provided
Implementing Mobile and Distributed Applications in X-Klaim
No full textIn this paper we present X-Klaim, an experimental programming
language specifically designed to program distributed systems
composed of several components interacting through multiple
distributed tuple spaces and mobile code. The language consists of a
set of coordination primitives inspired by Linda, a set of operators
for building processes borrowed from process algebras and a few
classical constructs for sequential programming. We present some
programming examples in X-Klaim, dealing with mobile code
programming paradigms, such as client-server, code mobility and
mobile agents
Modeling Fuzzy Behaviours in Concurrent Systems
No full textBehaviour of concurrent systems has been classically specified by means of Labeled Transition Systems. Uncertainty can be modeled in LTS by means of non-determinism that can be used for modeling systems whose behaviour is not completely specified or for specifying unpredictable behaviours like, for instance, errors. Such approach is not completely satisfactory. Indeed, it is not able to give a measure of uncertainty. In this paper we propose a new variant of LTS, named Fuzzy Labeled Transition Systems (FLTS), where fuzziness is used for modeling uncertainty in concurrent systems. In FLTS, transition relation is defined in term of a Fuzzy Set that gives the membership degree of a given transition/computation. To reason about FLTS, a variant of Hennessy-Milner Logic is also proposed. The proposed logic will be used for specifying behavioural properties of systems for which a measure of the satisfaction is defined
Multiple-Labelled Transition Systems for nominal calculi and their logics
No full textAction-labelled transition systems (LTSs) have proved to be a fundamental model for describing and proving properties of concurrent systems. In this paper we introduce Multiple-Labelled Transition Systems (MLTSs) as generalisations of LTSs that enable us to deal with system features that are becoming increasingly important when considering languages and models for network-aware programming. MLTSs enable us to describe not only the actions that systems can perform but also their usage of resources and their handling (creation, revelation . . .) of names; these are essential for modelling changing evaluation environments. We also introduce MoMo, which is a logic inspired by Hennessy–Milner Logic and the μ-calculus, that enables us to consider state properties in a distributed environment and the impact of actions and movements over the different sites. MoMo operators are interpreted over MLTSs and both MLTSs and MoMo are used to provide a semantic framework to describe two basic calculi for mobile computing, namely μKlaim and the asynchronous π-calculus
- …
