Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators
122
0
0.0
(
0
)
Added by
EPTCS
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Authors
Daniel Gebler
Ask ChatGPT about the research
No Arabic abstract
Bisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS specification of probabilistic processes, we provide a method to compute for each operator of the language its respective metric compositionality property. The compositionality property of an operator is defined as its modulus of continuity which gives the relative increase of the distance between processes when they are combined by that operator. The compositionality property of an operator is computed by recursively counting how many times the combined processes are copied along their evolution. The compositionality properties allow to derive an upper bound on the distance between processes by purely inspecting the operators used to specify those processes.
rate research
Read More
A point process on a space is a random bag of elements of that space. In this paper we explore programming with point processes in a monadic style. To this end we identify point processes on a space X with probability measures of bags of elements in X. We describe this view of point processes using the composition of the Giry and bag monads on the category of measurable spaces and functions and prove that this composition also forms a monad using a distributive law for monads. Finally, we define a morphism from a point process to its intensity measure, and show that this is a monad morphism. A special case of this monad morphism gives us Walds Lemma, an identity used to calculate the expected value of the sum of a random number of random variables. Using our monad we define a range of point processes and point process operations and compositionally compute their corresponding intensity measures using the monad morphism.
We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds. We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds. Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is $Pi^0_2$-complete. We also provide a compositional representation of our semantics in terms of an intersection type system. In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites. Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability. Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods. We have constructed prototype implementations of our method of computing lower bounds of termination probability, and AST verification.
Single-pass instruction sequences under execution are considered to produce behaviours to be controlled by some execution environment. Threads as considered in thread algebra model such behaviours: upon each action performed by a thread, a reply from its execution environment determines how the thread proceeds. Threads in turn can be looked upon as producing processes as considered in process algebra. We show that, by apposite choice of basic instructions, all processes that can only be in a finite number of states can be produced by single-pass instruction sequences.
We make a formal analogy between random sampling and fresh name generation. We show that quasi-Borel spaces, a model for probabilistic programming, can soundly interpret Starks $ u$-calculus, a calculus for name generation. Moreover, we prove that this semantics is fully abstract up to first-order types. This is surprising for an off-the-shelf model, and requires a novel analysis of probability distributions on function spaces. Our tools are diverse and include descriptive set theory and normal forms for the $ u$-calculus.
We introduce a method for proving almost sure termination in the context of lambda calculus with continuous random sampling and explicit recursion, based on ranking supermartingales. This result is extended in three ways. Antitone ranking functions have weaker restrictions on how fast they must decrease, and are applicable to a wider range of programs. Sparse ranking functions take values only at a subset of the programs reachable states, so they are simpler to define and more flexible. Ranking functions with respect to alternative reduction strategies give yet more flexibility, and significantly increase the applicability of the ranking supermartingale approach to proving almost sure termination, thanks to a novel (restricted) confluence result which is of independent interest. The notion of antitone ranking function was inspired by similar work by McIver, Morgan, Kaminski and Katoen in the setting of a first-order imperative language, but adapted to a higher-order functional language. The sparse ranking function and confluent semantics extensions are unique to the higher-order setting. Our methods can be used to prove almost sure termination of programs that are beyond the reach of methods in the literature, including higher-order and non-affine recursion.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
