1,721,136 research outputs found
Enhanced models for privacy and utility in continuous-time diffusion networks
No full textControlling the propagation of information in social networks is a problem of growing importance. On one hand, users wish to freely communicate and interact with their peers. On the other hand, the information they spread can bring to harmful consequences if it falls in the wrong hands. There is therefore a trade-off between utility, i.e. reaching as many intended nodes as possible, and privacy, i.e. avoiding the unintended ones. The problem has attracted the interest of the research community: some models have already been proposed to study how information propagates and to devise policies satisfying the intended privacy and utility requirements. In this paper, we adapt the basic framework of Backes et al. to include more realistic features, that in practice influence the way in which information is passed around. More specifically, we consider: (a) the topic of the shared information, (b) the time spent by users to forward information among them and (c) the user social behaviour. For all features, we show a way to reduce our model to the basic one, thus allowing the methods provided in the original paper to cope with our enhanced scenarios. Furthermore, we propose an enhanced formulation of the utility/privacy policies, to maximize the expected number of reached users among the intended ones, while minimizing this number among the unintended ones, and we show how to adapt the basic techniques to these enhanced policies. We conclude by giving a new approach to the maximization/minimization problem by finding a trade-off between the risk and the gain function through biobjective optimization
A framework for abstract interpretation of timed concurrent constraint programs
No full textTimed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e. systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and we extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize the first general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric w.r.t. the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming, e.g., to perform a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we make also use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We have developed a prototypical implementation of our methodology and we have implemented the abstract domain for security to perform automatically the secrecy analysis
Separation of synchronous and asynchronous communication via testing
No full textOne of the early results about the asynchronous π-calculus which significantly contributed to its popularity is the capability of encoding the output prefix of the (choiceless) pi-calculus in a natural and elegant way.
Encodings of this kind were proposed by Honda and Tokoro, by Nestmann and (independently) by Boudol.
We investigate whether the above encodings preserve De Nicola and Hennessy’s testing semantics. In this sense, it turns out that, under some general conditions, no encoding of output prefix is able to preserve the must testing. This negative result is due to (a) the non atomicity of the sequences of steps which are necessary in the asynchronous π-calculus to mimic synchronous communication, and (b) testing semantics’s sensitivity to divergence
Fair Pi
No full textIn this paper, we define fair computations in the π-calculus [18]. We follow Costa and Stirling’s approach for CCS-like languages but exploit a more natural labeling method of process actions to filter out unfair process executions. The new labeling allows us to prove all the significant properties of the original one, such as unicity, persistence and disappearance of labels. It also turns out that the labeled pi-calculus is a conservative extension of the standard one. We contrast the existing fair testing with those that
naturally arise by imposing weak and strong fairness as defined by Costa and Stirling. This comparison provides the expressiveness of the various fair testing-based semantics and emphasizes the discriminating power of the one already proposed in the literature
Compositional Analysis for Concurrent Constraint Programming
Full text linkA framework for the analysis of concurrent constraint programming (CCP) is proposed. The approach is based on simple denotational semantics that approximate the usual semantics in the sense that they give a superset of the input-output relation of a CCP program. Analyses based on these semantics can be easily and efficiently implemented using standard techniques from the analysis of logic program
A Model-Theoretic Reconstruction ofthe Operational Semantics of Logic Programs
No full textIn this paper we define a new notion or truth on Herbrand interpretations extended with variables which allows us to capture, by means of suitable models, various observable properties, such as the ground success set, the set of atomic consequences, and the computed answer substitutions. The notion of truth extends the classical one to account for non-ground formulas in the interpretations. The various operationalsemantics are all models. An ordering on interpretations is defined to overcome the problem that the intersection of a set of models is not necessarily amodel. The set of interpretations with this partial order is shown to be a complete lattice, and the greatest lower bound of any set of models is shown to be amodel. Thus there exists a least model, which is the least Herbrand model and therefore the ground success set semantics. Richer operationalsemantics are non-least models, which can, however, be effectively defined by fixpoint constructions. The model corresponding to the computed answer substitutions operationalsemantics is the most primitive one (the others can easily be obtained from it)
Dynamic Slicing for Concurrent Constraint Languages
Full text linkConcurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP (and other language variants) and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to several variants of CCP, such as the timed language ntcc, linear CCP (an extension of CCPbased on linear logic where constraints can be consumed) and some extensions of CCP dealing with epistemic and spatial information. We also develop a prototypical implementation freely available for making experiments
A Synchronization Logic: Axiomatics and FormalSemantics of Generalized Horn Clauses
No full textAn extension of Horn clause logic is defined based on the introduction of a synchronization operator. Generalized Horn clauses (GHC) are introduced through an informal description of their operational semantics, which allows discussion of some typical synchronization problems. GHC are first considered formally as a programming language by defining the syntax, the operational semantics, the model-theoretic semantics, and the fixed-point semantics. The above mentioned semantics are given in the Van Emden-Kowalski style (1976, J. Assoc. Comput. Mach. 23, 733–742) and are proved equivalent. GHC are then characterized as axiomatic theories. A set of axiom schemata concerned with the newly introduced synchronization operator is defined and it is proved that the operational semantics inference rule is both sound and complete. Finally, the relation between GHC and Horn clauses is analyzed, and it is proved that Horn clause logic is strictly included in the generalized Horn clause logic
- …
