1,721,002 research outputs found
Security Types for Mobile Safe Ambients
No full textThe {\em Ambient Calculus} and the {\em Safe Ambient Calculus} have been recently successfully proposed as models for the Web. They are based on the notions of ambient {\em movement} and ambient {\em opening}. Different type disciplines have been devised for them in order to avoid unwanted behaviours of processes. In the present paper we propose a type discipline for safe mobile ambients which is essentially motivated by ensuring {\em security} properties. We associate security levels to ambients and we require that an ambient at security level can only be traversed or opened by ambients at security level at least . Since the movement and opening right can be unrelated, we consider two partial orders between security levels. We give some examples of use of our type discipline. A first protocol models a mailserver with different mailboxes and users: each user is allowed to enter only his own mailbox. A second example show that we can encode a security policy for reading and writing recently proposed for the -calculus. Lastly we present the renaming, firewall and channel protocols which are already typed in other type disciplines for comparisons and for showing how some behavioural conditions can be expressed in our system as type constraints
A CuCh Interpretation of an Object-Oriented Language1
No full textCuCh machine extends pure lambda--calculus with algebraic data types and provides a the possibility of defining functions over the disjoint sum of algebras. We exploit such natural form of {\em overloading} to define a functional interpretation of a simple, but significant fragment of a typical object-oriented language
Depletable channels: dynamics, behaviour, and efficiency in network design
No full textWe present a simple model, called depleatable channels, of multi-hop communication in ad hoc networks. We introduce a model for channel energy consumption, and we propose a notion of channel equivalence based on the communication service they provide, regardless of specific routing protocols. In particular, we consider equivalent two channels with identical maximum and minimum inhibiting flow, and prove that this notion of equivalence, and variants of it, coincide with standard equivalences borrowed from the theory of concurrency. Unfortunately, while the maximum flow can be computed in polynomial time, calculating the value of a minimum inhibiting flow is NP-hard. Thus, we propose a characterization of those graphs, called weak, which admit charge assignments for which the minimum inhibiting flow is strictly less than the maximum flow and show that weakness can be checked efficiently by providing an algorithm that does so in polynomial time
Conflict vs causality in event structures
Full text linkEvent structures are one of the best known models for concurrency. Many variants of the basic model and many possible notions of equivalence for them have been devised in the literature. In this paper, we study how the spectrum of equivalences for Labelled Prime Event Structures built by Van Glabbeek and Goltz changes if we consider two simplified notions of event structures: the first is obtained by removing the causality relation (Coherence Spaces) and the second by removing the conflict relation (Elementary Event Structures). As expected, in both cases the spectrum turns out to be simplified, since some notions of equivalence coincide in the simplified settings; actually, we prove that removing causality simplifies the spectrum considerably more than removing conflict. Furthermore, while the labeling of events and their cardinality play no role when removing causality, both the labeling function and the cardinality of the event set dramatically influence the spectrum of equivalences in the conflict-free setting
A Polynomial-Time Algorithm for detecting the possibility of Braess Paradox in Directed Graphs
No full textA directed multigraph is said vulnerable if it can generate Braess paradox in traffic networks. In this paper, we give a graph–theoretic characterisation of vulnerable directed multigraphs. Analogous results appeared in the literature only for undirected multigraphs and for a specific family of directed multigraphs. The proof of our characterisation provides the first polynomial time algorithm that checks if a general directed multigraph is vulnerable in O(| V| · | E|2). Our algorithm also contributes to the directed subgraph homeomorphism problem without node mapping, by providing another pattern graph for which a polynomial time algorithm exists
Totality, definability and boolean circuits
No full textWe present a bottom-up type inference algorithm for security types in Mobile Ambients. The algorithm, given an untyped process , calculates the minimal set of constraints on security levels such that all the actions during a run of can be performed without violating the security level priorities. Our algorithm appears as a preliminary step in order to use type systems to ensure security properties in the web scenario
Graph theoretic detection of inefficiencies in network models
No full textWe present graph-theoretic characterisations of three notions of inefficiency arising in network models: edge-weakness in flow networks, node-weakness in depletable channels, and vulnerability in traffic networks. Our characterisations lead to three polynomial algorithms that check these forms of inefficiency. Furthermore, checking vulnerability also leads to an advancement on the subgraph homeomorphism problem
A Characterization of Weakly Church-Rosser Abstract Reduction Systems, not Church-Rosser
No full textBasic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church–Rosser, CR) and weak confluence (or weak Church–Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known counterexamples to the implication WCR ⇒ CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graph-theoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the Newman's lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graph-rewriting rules, with specific combinatorial properties
QKS
No full textQKS is an available at http://mclab.di.uniroma1.it. It is a software tool for the automatic synthesis of quantized feedback control software from the plant model and formal closed loop specifications
Some computational properties of intersection types
No full textThis paper presents a new method for comparing computation-properties of λ-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and λ-definability are investigated. A translation is introduced from intersection typing derivations to Curry typeable terms; the main feature of the proposed technique is that the translation is preserved by β-reduction. This allows to simulate a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach naturally leads to prove strong normalization in the intersection system by means of purely syntactical techniques. In addition, the presented method enables us to give a proof of a conjecture proposed by Leivant in 1990, namely that all functions uniformly definable using intersection types are already definable using Curry type
- …
