PAuL on Friday, August 11th

Session 1 (09:00‑10:30)
Chair: Christel Baier

09:00‑09:05	Welcome
09:05‑10:00	Anatol Slissenko (University 12, Paris, France) Decidability of verification in predicate logics of probability [pdf] Probabilistic models appear in various questions of verification, for example in communication or cryptographic protocols, information flow, robustness of security policies. The talk describes some predicate logics with probability operator, their semantics and the problem of introducing explicit time in the language. The satisfiability is usually undecidable for such logics. However, for some of them model-checking proves to be decidable. An approach to the description of decidable classes of verification based on ''bounded complexity model'' property is also discussed.
10:00‑10:30	Sandra Batista (UCLA Computer Science) A Note on Spaced Bounded Interactive Proof Systems and Martingales In this note, we offer an alternative martingale proof for the result of Condon and Lipton that any Markov (feedback) chain in a family of Markov (feedback) chains reaches its absorbing state in doubly exponential time in the size of the chain with high probability. This result was used to show an the upper bound of the complexity of languages verified by interactive proof systems with 2-way probabilistic finite verifier. Moreover, we discuss more general potential applications of our proof technique to probabilistic finite automata and interactive proof systems.

Break (10:30‑11:00)

Session 2 (11:00‑12:30)
Chair: tba

11:00‑11:30	Sayan Mitra (Massachusetts Institute of Technology) Nancy Lynch (Massachusetts Institute of Technology) Approximate Simulations for Task-Structured Probabilistic I/O Automata A Probabilistic I/O Automaton (PIOA) is a countable-state automaton model that allows nondeterministic and probabilistic choices in state transitions. A task-PIOA adds a task structure on the locally controlled actions of a PIOA as a means for restricting the nonde- terminism in the model. The task-PIOA framework defines exact implementation relations based on inclusion of sets of trace distributions. In this paper we develop the theory of approximate implementations and equivalences for task-PIOAs. We propose a new kind of approximate simulation between task-PIOAs and prove that it is sound with respect to approximate implementations. Our notion of similarity of traces is based on a metric on trace distributions and therefore, we do not require the state spaces nor the space of exter- nal actions (output alphabet) of the underlying automata to be metric spaces. We discuss applications of approximate implementations to probabilistic safety verification.
11:30‑12:00	Celine Kuttler (Interdisciplinary Research Institut of Lille) Cedric Lhoussaine (Universite of Lille) Joachim Niehren (INRIA Futurs) A Stochastic Pi-Calculus for Concurrent Objects The stochastic pi calculus is a promising highly expressive formal modeling language for systems biology. The minimality of its operators, however, is sometimes unfortunate from the modeling perspective. We propose to extend the synchronous pi calculus by pattern guarded choice, so that concurrent objects become available. We present a stochastic semantics of our pi calculus extension. We then show how to encode pattern guarded choices in the pi calculus such that the stochastic semantics is preserved.
12:00‑12:30	Alessandro Tiberi (department of computer science, University of Rome "La Sapienze") Probabilistic Configuration Theories We introduce a new framework for describing computations which are both concurrent and probabilistic. This framework is a natural extension of the \emph{Configuration Theories} of \cite{cencia}, and allows to express properties about both the \emph{causal} and the \emph{probabilistic} aspect of concurrent computations. Computations are described in an axiomatic way, by using a probabilistic extensions of poset sequents. A scheme of structural rules on these sequents is introduced and shown to be sound, while completeness can be obtained by adding a rule which is not treated in the present work. We also introduce a new probabilistic extension of \emph{Configuration Structures}, which we use as models for probabilistic sequents.

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)
Chair: tba

14:00‑15:00

Krishnendu Chatterjee (University of California, Berkeley, USA) Simple Stochastic omega-Regular Games [pdf] The theory of graph games with omega-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider stochastic graph games with omega-regular winning conditions specified as Rabin and Streett objectives. The quantitative analysis problem asks for the maximal probability of winning (optimal winning) from each state for a given objective. In this talk we present basic techniques for the quantitative analysis of stochastic graph games with Rabin and Streett ovjectives. The techniques are useful in characterizing optimal strategies and establishing the computational complexity of stochastic Rabin and Streett games. Moreover, the techniques have recently also led to the development of interesting algorithms to solve such games.

15:00‑15:30

Andrzej Murawski (University of Oxford) Joel Ouaknine On Probabilistic Program Equivalence and Refinement We study notions of equivalence and refinement for probabilistic programs formalized in the second-order fragment of Probabilistic Idealized Algol. Probabilistic programs implement randomized algorithms: a given input yields a probability distribution on the set of possible outputs. Intuitively, two programs are equivalent if they give rise to identical distributions for all inputs. We show that equivalence is decidable by studying the fully abstract game semantics of probabilistic programs and relating it to probabilistic finite automata. For terms in beta-normal form our decision procedure runs in time exponential in the syntactic size of programs; it is moreover fully compositional in that it can handle open programs (probabilistic modules with unspecified components).

Break (15:30‑16:00)

Session 4 (16:00‑18:00)
Chair: Marcus Groesser

16:00‑17:00	Javier Esparza (University of Stuttgart, Germany) Computing rewards for probabilistic pushdown systems [pdf] Imperative programming languages provide procedural mechanisms for structuring large programs. In the last years our group has used pushdown automata to model and verify programs with (possibly recursive) procedures. Currently, we (and other groups using our tools) are able to check relevant properties of programs with up to ten thousands of lines within few minutes. A fascinating current challenge is the verification of probabilistic programs. Stochastic decisions can be an intrinsic part of the program, as in randomized algorithms, or can be added to it in order to model our limited knowledge of the program or of its environment. While finite Markov chains provide a resonable semantics for probabilistic while programs, probabilistic pushdown automata (or equivalent models like recursive Markov chains) must be used in the procedural case. These models generate infinite Markov chains, and so many of the basic results of Markov chain theory, which are only valid for finite chains, cannot be applied. Many problems, like the average time it takes to serve a request, or the average stack length, can be modelled by means of probabilistic pushdown automata with reward functions. The goal is to compute the gain, or reward obtained per time unit. I will present techniques for this problem and discuss their complexity. This is joint work with Tomasz Brazdil, Antonin Kucera and Richard Mayr.
17:00‑17:30	Vaclav Brozek (Masaryk University) On Decidability and Complexity of Stochastic Pushdown Games We consider a class of infinite 2 1/2 player games generated by pushdown automata (PDA). This concept is used in the scope of modelling recursive systems allowing both probabilistic and nondeterministic choice. We study several linear and branching-time winning objectives and examine the decidability of the problem whether a player has a winning strategy for a given winning objective. Because this problem is undecidable in general (i.e. for general strategies) even for very simple winning objectives we consider only a restricted class of stackless & memoryless strategies. We show that this restriction makes the above problem decidable even for some very complex winning objectives. We also derive some complexity estimates. Note that results presented here are only partial as the work is still in progress.
17:30‑18:00	Vaclav Brozek (Masaryk University) Tomas Brazdil (Masaryk University) Vojtech Forejt (Masaryk University) Antonin Kucera (Masaryk University) Reachability in Recursive Markov Decision Processes We consider a class of infinite-state Markov decision processes generated by stateless pushdown automata. This class corresponds to 1.5-player games over graphs generated by BPA systems or (equivalently) 1-exit recursive state machines. An extended reachability objective is specified by two sets S and T of safe and terminal stack configurations, where the membership to S and T depends just on the top-of-the-stack symbol. The question is whether there is a suitable strategy such that the probability of hitting a terminal configuration by a path leading only through safe configurations is equal to (or different from) a given x in {0,1}. We show that the qualitative extended reachability problem is decidable in polynomial time, and that the set of all configurations for which there is a winning strategy is effectively regular. More precisely, this set can be represented by a deterministic finite-state automaton with a fixed number of control states. This result is a generalization of a recent theorem by Etessami & Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our 1.5-player BPA games) is decidable in polynomial time. Interestingly, the properties of winning strategies for the extended reachability objectives are quite different from the ones for termination, and new observations are needed to obtain the result. As an application, we derive the EXPTIME-completeness of the model-checking problem for 1.5-player BPA games and qualitative PCTL formulae.