Synthesis for Probabilistic Environments

In synthesis we construct finite state systems from temporal specifications. While this problem is well understood in the classical setting of non-probabilistic synthesis, this paper suggests the novel approach of open synthesis under the assumptions of an environment that chooses its actions randomized rather than nondeterministically. Assuming a randomized environment inspires alternative semantics both for linear-time and branching-time logics. For linear-time, natural acceptance criteria are almost-sure and observable acceptance, where it suffices if the probability measure of accepting paths is 1 and greater than 0, respectively. We distinguish 0-environments, which can freely assign probabilities to each environment action, from -environments, where the probabilities assigned by the environment are bound from below by some > 0. While the results in case of 0-environments are essentially the same as for nondeterministic environments, the languages occurring in case of -environ...

• Type: Conference
• Year: 2006
• Where: ATVA
• Authors: Sven Schewe
• Keywords: ATVA 2006, Finite State Systems, Hardware, Natural Acceptance Criteria, Open Synthesis