1,721,134 research outputs found
Space-Aware Ambients and Processes
No full textResource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the context of an ambient-like calculus with bounded capacities and weighed processes, where migration and activation require space. A type system complements the dynamics of the calculus by providing static guarantees that the intended capacity bounds are preserved throughout the computation
A Calculus of Mobile Resources
No full textWe introduce a calculus of Mobile Resources (MR) tailored for the design and analysis of systems containing mobile, possibly nested, computing devices that may have resource and access constraints, and which are not copyable nor modifiable per se. We provide a reduction as well as a labelled transition semantics and prove a correspondence be- tween barbed bisimulation congruence and a higher-order bisimulation. We provide examples of the expressiveness of the calculus, and apply the theory to prove one of its characteristic properties
Concurrent Graph and Term Graph Rewriting
No full textGraph Rewriting Systems are a powerful formalism for the specification of parallel and distributed systems, and the corresponding theory is rich of results concerning parallelism and concurrency. I will review the main results of the theory of concurrency for the algebraic approach to graph rewriting, emphasizing the relationship with the theory of Petri nets. In fact, graph rewriting systems can be regarded as a proper generalization of Petri nets, where the current state of a system is described by a graph instead of by a collection of tokens. Recently, this point of view allowed for the generalization to graph rewriting of some interesting results and constructions of the concurrent semantics of nets, including processes, unfoldings, and categorical semantics based on pair of adjoint functors
Typing and Subtyping Mobility in Boxed Ambients
No full textWe provide a novel type system for Bugliesi et al.'s Boxed Ambients that combines value subtyping with mobility types. The former is based on read/write exchange types, the latter builds on the notion of ambient group. Mobility types allow to specify where an ambient is allowed to stay, closing existing expressiveness gaps in the literature at no additional complexity costs. Subtyping is aimed at achieving maximal generality on both communication and mobility types. We then introduce co-capabilities to express explicit permissions to access ambients. In this setting, ambient types are refined to specify who is allowed to enter an ambient, making a promising framework to model open systems
Zero-safe net models for transactions in Linda
No full textZero-safe nets are a variation of Petri nets, where transactions can be suitably modeled. The idea is to distinguish between stable places (whose markings define observable states) and zero-safe places (where tokens can only be temporarily allocated, defining hidden states): Transactions must start and end in observable states. We propose an extension of the coordination language Linda, called TraLinda, where a few basic primitives for expressing transactions are introduced by means of different typing of tuples. By exploiting previous results of Busi, Gorrieri and Zavattaro on the net modeling of Linda-like languages, we define a concurrent operational semantics based on zero-safe nets for TraLinda, where the typing of tuples reflects evidently on the distinction between stable and zero-safe places
Component refinement and CSC solving for STG decomposition
No full textComponent refinement and CSC solving for STG decomposition / Mark Schaefer, Walter Vogler. - In: Foundations of software science and computational structures : 8th international conference, FOSSACS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4 - 8, 2005 ; proceedngs / Vladimiro Sassone (ed.). - Berlin [u.a.] : Springer, 2005. - S. 348-363. - (Lecture notes in computer science ; 3441
Context Aware Specification and Verification of Distributed Systems
No full textDistributed and mobile systems are typically composed of heterogeneous computational units that interact with each other following a predefined protocol. Process algebras and modal logics have been largely used as tools for specifying and verifying such kind of systems. However, to use these tools a complete system description has to be provided. This is not always possible. Indeed, even if the protocol governing the interactions among the system components is completely specified, the precise implementation of each component, as well as the number of network elements, is generally unknown. In this paper we present a set of formal tools that permits specifying systems by means of mixed specifications: a system is not considered in isolation, but under the assumption that the enclosing environment satisfies a given set of properties. A model-checking algorithm is also defined to verify whether considered specifications satisfy or not the expected properties. In the former case, it is also guaranteed that whenever the context is instantiated with components satisfying the assumptions, property satisfaction is preserved
Categories of Coalgebraic Games
No full textWe consider a general notion of coalgebraic game, whereby games are viewed as elements of a final coalgebra. This allows for a smooth definition of game operations (e.g. sum, negation, and linear implication) as final morphisms. The notion of coalgebraic game subsumes different notions of games, e.g. possibly non-wellfounded Conway games and games arising in Game Semantics à la [AJM00]. We define various categories of coalgebraic games and (total) strategies, where the above operations become functorial, and induce a structure of monoidal closed or*-autonomous category. In particular, we define a category of coalgebraic games corresponding to AJM-games and winning strategies, and a generalization to non-wellfounded games of Joyal's category of Conway games. This latter construction provides a categorical characterization of the equivalence by Berlekamp, Conway, Guy on loopy games
- …
