Synthesis for Probabilistic Environments
Sven Schewe
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 epsilon-environments, where the probabilities assigned by the environment are bound from below by some epsilon>0.
While the results in case of 0-environments are essentially the same as for nondeterministic environments, the languages occurring in case of epsilon-environments are topologically different from the results for nondeterministic and 0-environments (in case of LTL, recognizable by weak alternating automata vs. recognizable by deterministic automata). The complexity of open synthesis is, in both cases, EXPTIME and 2EXPTIME-complete for CTL and LTL specifications, respectively.
4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006).