Online Demo About Downloads Publications Case Studies


APEX Publications


Title: On the Complexity of the Equivalence Problem for Probabilistic Automata
Authors:Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Bjorn Wachter and James Worrell
Conference: FOSSACS 2012, Talinn, Estonia

Checking two probabilistic automata for equivalence has been shown to be a key problem for efficiently establishing various behavioural and anonymity properties of probabilistic systems. In recent experiments a randomised equivalence test based on polynomial identity testing outperformed deterministic algorithms. In this paper we show that polynomial identity testing yields efficient algorithms for various generalisations of the equivalence problem. First, we provide a randomized NC procedure that also outputs a counterexample trace in case of inequivalence. Second, we show how to check for equivalence two probabilistic automata with (cumulative) rewards. Our algorithm runs in deterministic polynomial time, if the number of reward counters is fixed. Finally we show that the equivalence problem for probabilistic visibly pushdown automata is logspace equivalent to the Arithmetic Circuit Identity Testing problem, which is to decide whether a polynomial represented by an arithmetic circuit is identically zero.


Title: Language Equivalence for Probabilistic Automata
Authors: Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Bjorn Wachter and James Worrell
Conference:CAV 2011, Snowbird, Utah, USA

In this paper, we propose a new randomised algorithm for deciding language equivalence for probabilistic automata. This algorithm is based on polynomial identity testing and thus returns an answer with an error probability that can be made arbitrarily small. We implemented our algorithm, as well as deterministic algorithms of Tzeng and Doyen et al., optimised for running time whilst adequately handling issues of numerical stability. We conducted extensive benchmarking experiments, including the verification of randomised anonymity protocols, the outcome of which establishes that the randomised algorithm significantly outperforms the deterministic ones in a majority of our test cases.

Finally, we also provide fine-grained analytical bounds on the complexity of these algorithms, accounting for the differences in performance.

Title: On stabilization in Herman's algorithm
Authors: Stefan Kiefer, Andrzej S. Murawski, Joel Ouaknine, James Worrell, and Lijun Zhang
Conference:ICALP'11, Zürich, Switzerland

Herman's algorithm is a synchronous randomized protocol for achieving self-stabilization in a token ring consisting of N processes. The interaction of tokens makes the dynamics of the protocol very difficult to analyze. In this paper we study the expected time to stabilization in terms of the initial configuration.

It is straightforward that the algorithm achieves stabilization almost surely from any initial configuration, and it is known that the worst-case expected time to stabilization (with respect to the initial configuration) is Θ(N^2). Our first contribution is to give an upper bound of 0.64N^2 on the expected stabilization time, improving on previous upper bounds and reducing the gap with the best existing lower bound. We also introduce an asynchronous version of the protocol, showing a similar O(N2) convergence bound in this case.

Assuming that errors arise from the corruption of some number k of bits, where k is fixed independently of the size of the ring, we show that the expected time to stabilization is O(N). This reveals a hitherto unknown and highly desirable property of Herman's algorithm: it recovers quickly from bounded errors. We also show that if the initial configuration arises by resetting each bit independently and uniformly at random, then stabilization is significantly faster than in the worst case.

Title: Algorithmic Nominal Game Semantics
Authors:Andrzej Murawski and Nick Tzevelekos
Conference:ESOP 2011, Saarbrücken, Germany

We employ automata over infinite alphabets to capture the semantics of a finitary fragment of ML with ground-type references. Our approach is founded on game semantics, which allows us to translate programs into automata in such a way that contextual equivalence is characterized by a finitary notion of bisimilarity. As a corollary, we derive a decidability result for a class of first-order programs, including open ones that contain unspecified first-order procedures.


Title: Full Abstraction Without Synchronization Primitives
Authors:Andrzej Murawski
Conference:Electr. Notes Theor. Comput. Sci. 265 (2010)

Using game semantics, we prove a full abstraction result (with respect to the may-testing preorder) for Idealized Algol augmented with parallel composition (IA). Although it is common knowledge that semaphores can be implemented using shared memory, we find that semaphores do not extend IA conservatively. We explain the reasons for the mismatch.


Title: On Automated Verification of Probabilistic Programs
Authors: Axel Legay, Andrzej S. Murawski, Joel Ouaknine and James Worrell
Conference:TACAS 2008, Budapest, Hungary

We introduce a simple procedural probabilistic programming language which is suitable for coding a wide variety of randomised algorithms and protocols. This language is interpreted over finite datatypes and has a decidable equivalence problem. We have implemented an automated equivalence checker, which we call apex, for this language, based on game semantics. We illustrate our approach with three non-trivial case studies: (i) Herman’s self-stabilisation algorithm; (ii) an analysis of the average shape of binary search trees obtained by certain sequences of random insertions and deletions; and (iii) the problem of anonymity in the Dining Cryptographers protocol. In particular, we record an exponential speed-up in the latter over state-of-the-art competing approaches.


Title: On Probabilistic Program Equivalence and Refinement
Authors: Andrzej S. Murawski and Joel Ouaknine
Conference:Concur 2005, San Francisco, California, USA

We study notions of equivalence and refinement for prob abilistic 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 β-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).

In contrast, we show that the natural notion of program refinement, in which the input-output distributions of one program uniformly dominate those of the other program, is undecidable.

External Publications

Abramsky et al. 2000

S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Inf. Comput., 163:409–470, 2000.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Bhargava, Palamidessi 2005

M. Bhargava and C. Palamidessi. Probabilistic anonymity. In Proceedings of CONCUR, volume 3653 of LNCS, 2005.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Chaum 1988

D. Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability. J. Cryptology, 1(1):65–75, 1988.

[ Google ] [ Google Scholar ]

Ciesinki, Baier 2006

F. Ciesinski and C. Baier. L A tool for qualitative and quantitative linear time analysis of reactive systems. In Proceedings of QEST. IEEE Computer Society, 2006.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Cormen et al. 2001

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms. MIT Press, second edition, 2001.

[ Google ] [ Google Scholar ]

Danos, Harmer 2002

V. Danos and R. Harmer. Probabilistic game semantics. ACM Trans. Comput. Log., 3(3):359–382, 2002.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Dijkstra 1974

E. W. Dijkstra. Self-stabilizing systems in spite of distributed control. Commun. ACM, 17(11):643–644, 1974.

[ Google ] [ Google Scholar ]

Esparza, Etessami 2004

J. Esparza and K. Etessami. Verifying probabilistic procedural programs. In Proceedings of FSTTCS, volume 3328 of LNCS, 2004.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Herman 1990

T. Herman. Probabilistic self-stabilization. Inf. Process. Lett., 35(2):63–67, 1990.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Hibbard 1962

T. N. Hibbard. Some combinatorial properties of certain trees with applications to searching and sorting. J. ACM, 9(1):13–28, 1962.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Hinton et al. 2006

A. Hinton, M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In Proceedings of TACAS, volume 3920 of LNCS, 2006.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Hyland, L 2000

J. M. E. Hyland and C.-H. L. Ong. On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Inf. Comput., 163(2):285–408, 2000.

[ Google ] [ Google Scholar ]

Jonassen, Knuth 1978

A. T. Jonassen and D. E. Knuth. A trivial algorithm whose analysis isn’t. J. Comput. Syst. Sci., 16(3):301–322, 1978.

[ Google ] [ Google Scholar ]

Knott 1975

G. D. Knott. Deletion in Binary Storage Trees. PhD thesis, Stanford University, 1975. Computer Science Technical Report STAN-CS-75-491.

[ Google ] [ Google Scholar ]

Knuth 1973

D. E. Knuth. Sorting and searching. In Volume 3 of The Art of Computer Programming (first printing). Addison-Wesley, 1973.

[ Google ] [ Google Scholar ]

Kozen 1981

D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328– 350, 1981.

[ Google ] [ Google Scholar ]

Larsen, Skou 1992

K. Larsen and A. Skou. Compositional verification of probabilistic processes. In Proceedings of CONCUR, volume 630 of LNCS, 1992.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Legay et al.

A. Legay, A. S.Murawski, J. Ouaknine, and J.Worrell. Verification of probabilistic programs via equivalence checking. In preparation.

[ Google ] [ Google Scholar ]

Norman et al. 2007

G. Norman, C. Palamidessi, D. Parker, and P. Wu. Model checking the probabilistic calculus. In Proceedings of QEST. IEEE Computer Society, 2007.

[ Google ] [ Google Scholar ] [ Publisher's website ]


PRISM case study: Dining Cryptographers. crypt.php.

[ Google ] [ Google Scholar ]

Rabin 1963

M. O. Rabin. Probabilistic automata. Information and Control, 6(3):230–245, 1963.

[ Google ] [ Google Scholar ]

Rabin 1976

M. O. Rabin. Probabilistic algorithms. In Proceedings of the Symposium on Algorithms and Complexity. Academic Press, 1976.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Schneider, Sidiropoulos 1996

S. Schneider and A. Sidiropoulos. CSP and anonymity. In Proceedings of ES- ORICS, volume 1146 of LNCS, 1996.

[ Google ] [ Google Scholar ] [ Publisher's website ]

Tzeng 1992

W.-G. Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J. Comput., 21(2):216–227, 1992.

[ Google ] [ Google Scholar ]

Back to Top

Imprint/Impressum Data Protection/Datenschutzhinweis