2,664 research outputs found
Exact reachability for second-order integro-differential equations
No full textIn this Note we analyze a reachability problem for an integro-differential equation by using a harmonic analysis approach. To cite this article: P Loreti, D. Sforza, C R. Acad. Sci. Paris, Ser. I 347 (2009). (C) 2009 Academie des sciences. Published by Elsevier Masson SAS. All rights reserved
On the topological structure of univoque sets
No full textErdos, Horvath and Joo discovered some years ago that for some real numbers 1 < q < 2 there exists only one sequence c(i) of zeroes and ones such that Sigma c(i) q(-i) = 1. Subsequently, the set U of these numbers was characterized algebraically in [P. Erdos, I. Joo, V. Komornik, Characterization of the unique expansions 1 = Sigma q(-ni) and related problems, Bull. Soc. Math. France 118 (1990) 377-390] and [V. Komornik, P. Loreti, Subexpansions, superexpansions and uniqueness properties in non-integer bases, Period. Math. Hungar. 44 (2) (2002) 195-216]. We establish an analogous characterization of the closure (U) over bar of U. This allows us to clarify the topological structure of these sets: (U) over bar U is a countable dense set of (U) over bar, so the latter set is perfect. Moreover, since U is known to have zero Lebesgue measure, (U) over bar is a Cantor set. (C) 2006 Elsevier Inc. All rights reserved
Modeling adaptation with a tuple-based coordination language
No full textIn recent years, it has been argued that systems and applications, in order to deal with their increasing complexity, should be able to adapt their behavior according to new requirements or environment conditions. In this paper, we present a preliminary investigation aiming at studying how coordination languages and formal methods can contribute to a better understanding, implementation and usage of the mechanisms and techniques for adaptation currently proposed in the literature. Our study relies on the formal coordination language Klaim as a common framework for modeling some adaptation techniques, namely the MAPE-K loop, aspect- and context-oriented programming
A uniform definition of stochastic process calculi
No full textWe 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
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
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
Modeling Adaptation with Klaim
No full textIn recent years, it has been argued that systems and applications, in order to deal with their increasing complexity, should be able to adapt their behavior according to new requirements or environment conditions. In this paper, we present an investigation aiming at studying how coordination languages and formal methods can contribute to a better understanding, implementation and use of the mechanisms and techniques for adaptation currently proposed in the literature. Our study relies on the formal coordination language Klaim as a common framework for modeling some well-known adaptation techniques: the IBM MAPE-K loop, the Accord component-based framework for architectural adaptation, and the aspect- and context-oriented programming paradigms. We illustrate our approach through a simple example concerning a data repository equipped with an automated cache mechanism
A Logical Framework for Reasoning About Local and Global Properties of Collective Systems
No full textCollective adaptive systems (CAS) are composed of a large number of entities that interact with each other to reach local or global goals. Entities operate without any centralized control and should adapt their behavior to the changes in the environment where they operate. Due to the intricacies of these interactions and adaptation, it is difficult to predict the behavior of CAS. For this reason, formal tools are needed to specify and verify this behavior to ensure consistency, reliability, correctness, and safety properties. In this paper, we present a novel logical framework that permits specifying properties of CAS at both local and global levels: local properties refer to the behavior of individuals, while global properties refer to the whole system. An exact model checking algorithm, whose complexity is linear with the size of the formula and with the size of the model is also presented together with another one based on statistical model checking that permits handling systems composed by a large number of agents. Finally, a simple scenario is used to evaluate the advantages of the proposed approach
Effectiveness of overlay multicasting in mobile ad-hoc network
No full textThis paper investigates the effectiveness of the application level multicasting, named overlay multicasting, with respect to the network layer one in Mobile Ad Hoc Networks (MANET). With respect to network layer multicasting, in overlay multicasting only the mobile nodes participating to the multicast group exploit the multicast routing at application level, while the other nodes of the MANET simply perform unicast IP routing. This constraint in the possibility of use multicast routing in all nodes leads to a loss of efficiency in the bandwidth usage that we aims to discuss in this paper. The parameter used for the comparison is the cost of the multicast distribution tree, which is built by means of Steiner based algorithms. We measure this parameter by means of an exhaustive simulation campaign, analysing the performance dependence versus different parameters: device coverage range, number of MANET nodes, multicast group size and mobility model
Uniform Labeled Transition Systems for Nondeterministic, Probabilistic, and Stochastic Processes
No full textRate transition systems (RTS) are a special kind of transition systems introduced for defining the stochastic behavior of processes and for associating continuous-time Markov chains with process terms. The transition relation assigns to each process, for each action, the set of possible futures paired with a measure indicating the rates at which they are reached. RTS have been shown to be a uniform model for providing an operational semantics to many stochastic process algebras. In this paper, we define Uniform Labeled TRAnsition Systems (ULTraS) as a generalization of RTS that can be exploited to uniformly describe also nondeterministic and probabilistic variants of process algebras. We then present a general notion of behavioral relation for ULTraS that can be instantiated to capture bisimulation and trace equivalences for fully nondeterministic, fully probabilistic, and fully stochastic processes
- …
