We show how to obtain stochastic bounds for the strong stochastic ordering and the concave ordering of the maximal flow in a network where the capacities are non negative discrete random variables. While the deterministic problem is polynomial, the stochastic version with discrete random variables is NP-hard. The monotonicity of the Min-Cut problem for these stochastic orderings allows us to simplify the input distributions and obtain bounds on the results. Thus we obtain a tradeoff between the complexity of the computations and the precision of the bounds. We illustrate the approach with some examples.
Algebras can be used to interpret the behaviour of effectful programs. In particular, we use Eilenberg-Moore algebras given over a complete lattices of truth values, which specify answers to queries about programs. The algebras can be used to formulate a quantitative logic of behavioural properties, specifying a congruent notion of program equivalence coinciding with a notion of applicative bisimilarity. Many combinations of effects can be interpreted using these algebras. In this paper, we specify a method of generically combining effects and the algebras used to interpret them. At the core of this method is the tensor of complete lattices, which combines the carrier sets of the algebras. We show that this tensor preserves complete distributivity of complete lattices. Moreover, the universal properties of this tensor can then be used to properly combine the Eilenberg-Moore algebras. We will apply this method to combine the effects of probability, global store, cost, nondeterminism, and error effects. We will then compare this method of combining effects with the more traditional method of combining equational theories using interaction laws.
The analysis of information flow is a popular technique for ensuring the confidentiality of data. It is in this context that confidentiality policies arise for giving guarantees that private data cannot be inferred by the inspection of public data. One of those policies is non-interference, a semantic condition that ensures the absence of illicit information flow during program execution by not allowing to distinguish the results of two computations when they only vary in their confidential inputs. A remarkable feature of non-interference is that it can be enforced statically by the definition of information flow type systems. In those type systems, if a program type-checks, then it means that it meets the security policy. In this paper we focus on the preservation of non-interference through program translation. Concretely, we formalize the proof of security preservation of Hunt and Sands' translation that transforms high-level While programs typable in a flow-sensitive type system into equivalent high-level programs typable in a flow-insensitive type system. Our formalization is performed in the dependently-typed language Agda. We use the expressive power of Agda's type system to encode the security type systems at the type level. A particular aspect of our formalization is that it follows a fully internalist approach where we decorate the type of the abstract syntax with security type information in order to obtain the representation of well-typed (i.e secure) programs. A benefit of this approach is that it allows us to directly express the property of security preservation in the type of the translation relation. In this manner, apart from inherently expressing the transformation of programs, the translation relation also stands for an inductive proof of security preservation.
The bond-calculus is a language for modelling interactions between continuous populations of biomolecular agents. The calculus combines process-algebra descriptions of individual agent behaviour with affinity patterns, which can specify a wide variety of patterns of interactions between the sites of different agents. These affinity patterns extend binary molecular affinities to multiway reactions, general kinetic laws, and cooperative interactions. In this paper we explore bond-calculus modelling of gene regulation at both the molecular and network levels. At the molecular level, we show how affinity patterns can succinctly describe the λ-switch, a prototypical example of cooperative regulation. Moving to the network level, we develop a general model of gene regulatory networks using affinity patterns and an expanded Hill kinetic law. We illustrate the approach with a specific example: the complex plant circadian clock. We analyse these models via the bond-calculus's differential equation and stochastic semantics, and validate our results against existing models from the literature.
In this paper we present a modeling approach suitable for practical evaluation of the delays that may affect security monitoring systems in (multitenant) cloud based architecture, and in general to support professionals in planning and evaluating relevant parameters in dealing with new designs or migration projects. The approach is based on modularity and multiformalism techniques to manage complexity and guide designers in an incremental process, to help transferring technical knowledge into modeling practice and to help easing the use of simulation. We present a case study based on a real experience, triggered by a new legal requirement that Italian Public Administration should comply about their datacenters.
