اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA Calculus of Consistent Component-based Software Updates
96
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
It is important to enable reasoning about the meaning and possible effects of updates to ensure that the updated system operates correctly. A formal, mathematical model of dynamic update should be developed, in order to understand by both users and implementors of update technology what design choices can be considered. In this paper, we define a formal calculus $updatepi$, a variant extension of higher-order $pi$ calculus, to model dynamic updates of component-based software, which is language and technology independent. The calculus focuses on following main concepts: proper granularity of update, timing of dynamic update, state transformation betwee
قيم البحث
اقرأ أيضاً
Computer networks have become a critical infrastructure. In fact, networks should not only meet strict requirements in terms of correctness, availability, and performance, but they should also be very flexible and support fast updates, e.g., due to p
olicy changes, increasing traffic, or failures. This paper presents a structured survey of mechanism and protocols to update computer networks in a fast and consistent manner. In particular, we identify and discuss the different desirable consistency properties that should be provided throughout a network update, the algorithmic techniques which are needed to meet these consistency properties, and the implications on the speed and costs at which updates can be performed. We also explain the relationship between consistent network update problems and classic algorithmic optimization ones. While our survey is mainly motivated by the advent of Software-Defined Networks (SDNs) and their primary need for correct and efficient update techniques, the fundamental underlying problems are not new, and we provide a historical perspective of the subject as well.
We propose a graph-based process calculus for modeling and reasoning about wireless networks with local broadcasts. Graphs are used at syntactical level to describe the topological structures of networks. This calculus is equipped with a reduction se
mantics and a labelled transition semantics. The former is used to define weak barbed congruence. The latter is used to define a parameterized weak bisimulation emphasizing locations and local broadcasts. We prove that weak bisimilarity implies weak barbed congruence. The potential applications are illustrated by some examples and two case studies.
Graph transformation approaches have been successfully used to analyse and design chemical and biological systems. Here we build on top of a DPO framework, in which molecules are modelled as typed attributed graphs and chemical reactions are modelled
as graph transformations. Edges and vertexes can be labelled with first-order terms, which can be used to encode, e.g., steric information of molecules. While targeted to chemical settings, the computational framework is intended to be very generic and applicable to the exploration of arbitrary spaces derived via iterative application of rewrite rules, such as process calculi like Milners {pi}-calculus. To illustrate the generality of the framework, we introduce EpiM: a tool for computing execution spaces of {pi}-calculus processes. EpiM encodes {pi}-calculus processes as typed attributed graphs and then exploits the existing DPO framework to compute their dynamics in the form of graphs where nodes are {pi}-calculus processes and edges are reduction steps. EpiM takes advantage of the graph-based representation and facilities offered by the framework, like efficient isomorphism checking to prune the space without resorting to explicit structural equivalences. EpiM is available as an online Python-based tool.
We develop a version of the pi-calculus, picost, where channels are interpreted as resources which have costs associated with them. Code runs under the financial responsibility of owners; they must pay to use resources, but may profit by providing th
em. We provide a proof methodology for processes described in picost based on bisimulations. The underlying behavioural theory is justified via a contextual characterisation. We also demonstrate its usefulness via examples.
We give a complete presentation for the fragment, ZX&, of the ZX-calculus generated by the Z and X spiders (corresponding to copying and addition) along with the not gate and the and gate. To prove completeness, we freely add a unit and counit to the
category TOF generated by the Toffoli gate and ancillary bits, showing that this yields the full subcategory of finite ordinals and functions with objects powers of two; and then perform a two way translation between this category and ZX&. A translation to some extension of TOF, as opposed to some fragment of the ZX-calculus, is a natural choice because of the multiplicative nature of the Toffoli gate. To this end, we show that freely adding counits to the semi-Frobenius algebras of a discrete inverse category is the same as constructing the Cartesian completion. In particular, for a discrete inverse category, the category of classical channels, the Cartesian completion and adding counits all produce the same category. Therefore, applying these constructions to TOF produces the full subcategory of finite ordinals and partial maps with objects powers of two. By glueing together the free counit completion and the free unit completion, this yields qubit multirelations.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
