Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userUniform Labeled Transition Systems for Nondeterministic, Probabilistic, and Stochastic Process Calculi
85
0
0.0
(
0
)
Added by
EPTCS
Publication date
2011
fields
Informatics Engineering
and research's language is
English
Authors
Marco Bernardo
Ask ChatGPT about the research
No Arabic abstract
Labeled transition systems are typically used to represent the behavior of nondeterministic processes, with labeled transitions defining a one-step state to-state reachability relation. This model has been recently made more general by modifying the transition relation in such a way that it associates with any source state and transition label a reachability distribution, i.e., a function mapping each possible target state to a value of some domain that expresses the degree of one-step reachability of that target state. In this extended abstract, we show how the resulting model, called ULTraS from Uniform Labeled Transition System, can be naturally used to give semantics to a fully nondeterministic, a fully probabilistic, and a fully stochastic variant of a CSP-like process language.
rate research
Read More
Interface theories are powerful frameworks supporting incremental and compositional design of systems through refinements and constructs for conjunction, and parallel composition. In this report we present a first Interface Theor -- |Modal Mixed Interfaces -- for systems exhibiting both non-determinism and randomness in their behaviour. The associated component model -- Mixed Markov Decision Processes -- is also novel and subsumes both ordinary Markov Decision Processes and Probabilistic Automata.
A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.
A framework for the elicitation and debugging of formal specifications for Cyber-Physical Systems is presented. The elicitation of specifications is handled through a graphical interface. Two debugging algorithms are presented. The first checks for erroneous or incomplete temporal logic specifications without considering the system. The second can be utilized for the analysis of reactive requirements with respect to system test traces. The specification debugging framework is applied on a number of formal specifications collected through a user study. The user study establishes that requirement errors are common and that the debugging framework can resolve many insidious specification errors.
The probabilistic reachability problems of nondeterministic systems are studied. Based on the existing studies, the definition of probabilistic reachable sets is generalized by taking into account time-varying target set and obstacle. A numerical method is proposed to compute probabilistic reachable sets. First, a scalar function in the state space is constructed by backward recursion and grid interpolation, and then the probability reachable set is represented as a nonzero level set of this scalar function. In addition, based on the constructed scalar function, the optimal control policy can be designed. At the end of this paper, some examples are taken to illustrate the validity and accuracy of the proposed method.
Two of the most studied extensions of trace and testing equivalences to nondeterministic and probabilistic processes induce distinctions that have been questioned and lack properties that are desirable. Probabilistic trace-distribution equivalence differentiates systems that can perform the same set of traces with the same probabilities, and is not a congruence for parallel composition. Probabilistic testing equivalence, which relies only on extremal success probabilities, is backward compatible with testing equivalences for restricted classes of processes, such as fully nondeterministic processes or generative/reactive probabilistic processes, only if specific sets of tests are admitted. In this paper, n
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
