Arrow Research search

Author name cluster

Andrzej Murawski

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers
1 author row

Possible papers

6

NeurIPS Conference 2023 Conference Paper

Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach

  • Fabian Zaiser
  • Andrzej Murawski
  • Chih-Hao Luke Ong

We present an exact Bayesian inference method for discrete statistical models, which can find exact solutions to a large class of discrete inference problems, even with infinite support and continuous priors. To express such models, we introduce a probabilistic programming language that supports discrete and continuous sampling, discrete observations, affine functions, (stochastic) branching, and conditioning on discrete events. Our key tool is probability generating functions: they provide a compact closed-form representation of distributions that are definable by programs, thus enabling the exact computation of posterior probabilities, expectation, variance, and higher moments. Our inference method is provably correct and fully automated in a tool called Genfer, which uses automatic differentiation (specifically, Taylor polynomials), but does not require computer algebra. Our experiments show that Genfer is often faster than the existing exact inference tools PSI, Dice, and Prodigy. On a range of real-world inference problems that none of these exact tools can solve, Genfer's performance is competitive with approximate Monte Carlo methods, while avoiding approximation errors.

Highlights Conference 2020 Conference Abstract

Leafy automata for higher-order concurrency

  • Andrzej Murawski

Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA. The automata use an infinite alphabet with a tree structure. To demonstrate suitability of this automata model, we show that: – the game semantics of any FICA term can be represented by traces of a leafy automaton, and – the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation.

Highlights Conference 2017 Conference Abstract

Higher-order linearisability

  • Andrzej Murawski
  • Nikos Tzevelekos

Linearisability is a central notion for verifying concurrent libraries: a library is proven correct if its operational history can be rearranged into a sequential one that satisfies a given specification. Until now, linearisability has been examined for libraries in which method arguments and method results were of ground type, including libraries parameterised with such methods. In this paper we extend linearisability to the general higher-order setting: methods can be passed as arguments and returned as values. A library may also depend on abstract methods of any order. Extended abstract available in PDF.

Highlights Conference 2014 Conference Abstract

Böhm Trees as Higher-Order Recursive Schemes

  • Andrzej Murawski

Higher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, in that respect, are known to be equivalent to a restricted fragment of the λ Y -calculus, consisting of ground-type terms whose free variables have types of the form o →. .. → o (with o as a special case). In this paper, we show that any λ Y -term (with no restrictions on term type or the types of free variables) can actually be represented by a HORS. That is, for any λ Y -term M, there exists a HORS generating a tree that faithfully represents M 's Böhm tree. In particular, the HORS captures higher-order binding information contained in the Böhm tree. An analogous result holds for finitary PCF. As a consequence, we can reduce a variety of problems related to the λ Y -calculus or finitary PCF to problems concerning higher-order recursive schemes. For instance, Böhm tree equivalence can be reduced to the equivalence problem for HORS. Our results also enable MSO model-checking of Böhm trees.

Highlights Conference 2013 Conference Abstract

Bisimilarity of pushdown automata is nonelementary

  • Michael Benedikt
  • Stefan Göller
  • Stefan Kiefer
  • Andrzej Murawski

Given two pushdown systems, the bisimilarity problem asks whether they are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the previously best known lower bound for this problem. Our lower bound result holds for normed pushdown systems as well.