Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent computations where code usage plays a central role. The theory of program equivalence for modal and coeffectful languages, however, is considerably underdeveloped if compared to the denotational and operational semantics of such languages. This raises the question of how much of the theory of ordinary program equivalence can be given in a modal scenario. In this work, we show that coinductive equivalences can be extended to a modal setting, and we do so by generalising Abramsky's applicative bisimilarity to coeffectful behaviours. To achieve this goal, we develop a general theory of ternary program relations based on the novel notion of a comonadic lax extension, on top of which we define a modal extension of Abramsky's applicative bisimilarity (which we dub modal applicative bisimilarity). We prove such a relation to be a congruence, this way obtaining a compositional technique for reasoning about modal and coeffectful behaviours. But this is not the end of the story: we also establish a correspondence between modal program relations and program distances. This correspondence shows that modal applicative bisimilarity and (a properly extended) applicative bisimilarity distance coincide, this way revealing that modal program equivalences and program distances are just two sides of the same coin.

Report on the 2025 Ackermann Award, on behalf of the EACSL Ackermann Award Jury.

We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.

Abstract In this work, we generalize the concept of bisimulation metric in order to metrize the behaviour of continuous-time processes. Similarly to what is done for discrete-time systems, we follow two approaches and show that they coincide: as a fixpoint of a functional and through a real-valued logic. The whole discrete-time approach relies entirely on the step-based dynamics: the process jumps from state to state. We define a behavioural pseudometric for processes that evolve continuously through time, such as Brownian motion or involve jumps or both.

Extracting relevant information from a stream of high-dimensional observations is a central challenge for deep reinforcement learning agents. Actor-critic algorithms add further complexity to this challenge, as it is often unclear whether the same information will be relevant to both the actor and the critic. To this end, we here explore the principles that underlie effective representations for the actor and for the critic in on-policy algorithms. We focus our study on understanding whether the actor and critic will benefit from separate, rather than shared, representations. Our primary finding is that when separated, the representations for the actor and critic systematically specialise in extracting different types of information from the environment---the actor's representation tends to focus on action-relevant information, while the critic's representation specialises in encoding value and dynamics information. We conduct a rigourous empirical study to understand how different representation learning approaches affect the actor and critic's specialisations and their downstream performance, in terms of sample efficiency and generation capabilities. Finally, we discover that a separated critic plays an important role in exploration and data collection during training. Our code, trained models and data are accessible at https://github.com/francelico/deac-rep.

Learning from Preferential Feedback (LfPF) plays an essential role in training Large Language Models, as well as certain types of interactive learning agents. However, a substantial gap exists between the theory and application of LfPF algorithms. Current results guaranteeing the existence of optimal policies in LfPF problems assume that both the preferences and transition dynamics are determined by a Markov Decision Process. We introduce the Direct Preference Process, a new framework for analyzing LfPF problems in partially-observable, non-Markovian environments. Within this framework, we establish conditions that guarantee the existence of optimal policies by considering the ordinal structure of the preferences. We show that a decision-making problem can have optimal policies – that are characterized by recursive optimality equations – even when no reward function can express the learning goal. These findings underline the need to explore preference-based learning strategies which do not assume that preferences are generated by reward.

Reinforcement learning (RL) on high-dimensional and complex problems relies on abstraction for improved efficiency and generalization. In this paper, we study abstraction in the continuous-control setting, and extend the definition of Markov decision process (MDP) homomorphisms to the setting of continuous state and action spaces. We derive a policy gradient theorem on the abstract MDP for both stochastic and deterministic policies. Our policy gradient results allow for leveraging approximate symmetries of the environment for policy optimization. Based on these theorems, we propose a family of actor-critic algorithms that are able to learn the policy and the MDP homomorphism map simultaneously, using the lax bisimulation metric. Finally, we introduce a series of environments with continuous symmetries to further demonstrate the ability of our algorithm for action abstraction in the presence of such symmetries. We demonstrate the effectiveness of our method on our environments, as well as on challenging visual control tasks from the DeepMind Control Suite. Our method's ability to utilize MDP homomorphisms for representation learning leads to improved performance, and the visualizations of the latent space clearly demonstrate the structure of the learned abstraction.

Inspired by the seminal work of Hyland, Plotkin, and Power on the combination of algebraic computational effects via sum and tensor, we develop an analogous theory for the combination of quantitative algebraic effects. Quantitative algebraic effects are monadic computational effects on categories of metric spaces, which, moreover, have an algebraic presentation in the form of quantitative equational theories, a logical framework introduced by Mardare, Panangaden, and Plotkin that generalises equational logic to account for a concept of approximate equality. As our main result, we show that the sum and tensor of two quantitative equational theories correspond to the categorical sum (i.e., coproduct) and tensor, respectively, of their effects qua monads. We further give a theory of quantitative effect transformers based on these two operations, essentially providing quantitative analogues to the following monad transformers due to Moggi: exception, resumption, reader, and writer transformers. Finally, as an application, we provide the first quantitative algebraic axiomatizations to the following coalgebraic structures: Markov processes, labelled Markov processes, Mealy machines, and Markov decision processes, each endowed with their respective bisimilarity metrics. Apart from the intrinsic interest in these axiomatizations, it is pleasing they have been obtained as the composition, via sum and tensor, of simpler quantitative equational theories.

Abstract In this paper, we study the approximate minimization problem of weighted finite automata (WFAs): to compute the best possible approximation of a WFA given a bound on the number of states. By reformulating the problem in terms of Hankel matrices, we leverage classical results on the approximation of Hankel operators, namely the celebrated Adamyan-Arov-Krein (AAK) theory. We solve the optimal spectral-norm approximate minimization problem for irredundant WFAs with real weights, defined over a one-letter alphabet. We present a theoretical analysis based on AAK theory and bounds on the quality of the approximation in the spectral norm and $\ell ^2$ norm. Moreover, we provide a closed-form solution, and an algorithm, to compute the optimal approximation of a given size in polynomial time.

We give a categorical treatment, in the spirit of Baez and Fritz, of relative entropy for probability distributions defined on standard Borel spaces. We define a category suitable for reasoning about statistical inference on standard Borel spaces. We define relative entropy as a functor into Lawvere's category and we show convexity, lower semicontinuity and uniqueness.

Abstract Bisimulation is a concept that captures behavioural equivalence of states in a variety of types of transition systems. It has been widely studied in a discrete-time setting. The core of this work is to generalise the discrete-time picture to continuous time by providing a notion of behavioural equivalence for continuous-time Markov processes. In Chen et al. [(2019). Electronic Notes in Theoretical Computer Science347 45–63.], we proposed two equivalent definitions of bisimulation for continuous-time stochastic processes where the evolution is a flow through time: the first one as an equivalence relation and the second one as a cospan of morphisms. In Chen et al. [(2020). Electronic Notes in Theoretical Computer Science.], we developed the theory further: we introduced different concepts that correspond to different behavioural equivalences and compared them to bisimulation. In particular, we studied the relation between bisimulation and symmetry groups of the dynamics. We also provided a game interpretation for two of the behavioural equivalences. The present work unifies the cited conference presentations and gives detailed proofs.

Diffusion models are recent state-of-the-art methods for image generation and likelihood estimation. In this work, we generalize continuous-time diffusion models to arbitrary Riemannian manifolds and derive a variational framework for likelihood estimation. Computationally, we propose new methods for computing the Riemannian divergence which is needed for likelihood estimation. Moreover, in generalizing the Euclidean case, we prove that maximizing this variational lower-bound is equivalent to Riemannian score matching. Empirically, we demonstrate the expressive power of Riemannian diffusion models on a wide spectrum of smooth manifolds, such as spheres, tori, hyperboloids, and orthogonal groups. Our proposed method achieves new state-of-the-art likelihoods on all benchmarks.

Abstraction has been widely studied as a way to improve the efficiency and generalization of reinforcement learning algorithms. In this paper, we study abstraction in the continuous-control setting. We extend the definition of MDP homomorphisms to encompass continuous actions in continuous state spaces. We derive a policy gradient theorem on the abstract MDP, which allows us to leverage approximate symmetries of the environment for policy optimization. Based on this theorem, we propose an actor-critic algorithm that is able to learn the policy and the MDP homomorphism map simultaneously, using the lax bisimulation metric. We demonstrate the effectiveness of our method on benchmark tasks in the DeepMind Control Suite. Our method's ability to utilize MDP homomorphisms for representation learning leads to improved performance when learning from pixel observations.

We develop a theory for the commutative combination of quantitative effects, their tensor, given as a combination of quantitative equational theories that imposes mutual commutation of the operations from each theory. As such, it extends the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We show that under certain assumptions on the quantitative theories the free monad that arises from the tensor of two theories is the categorical tensor of the free monads on the theories. As an application, we provide the first algebraic axiomatizations of labelled Markov processes and Markov decision processes. Apart from the intrinsic interest in the axiomatizations, it is pleasing they are obtained compositionally by means of the sum and tensor of simpler quantitative equational theories.

We address the approximate minimization problem for weighted finite automata (WFAs) with weights in $\mathbb{R}$, over a one-letter alphabet: to compute the best possible approximation of a WFA given a bound on the number of states. This work is grounded in Adamyan-Arov-Krein Approximation theory, a remarkable collection of results on the approximation of Hankel operators. In addition to its intrinsic mathematical relevance, this theory has proven to be very effective for model reduction. We adapt these results to the framework of weighted automata over a one-letter alphabet. We provide theoretical guarantees and bounds on the quality of the approximation in the spectral and $\ell^2$ norm. We develop an algorithm that, based on the properties of Hankel operators, returns the optimal approximation in the spectral norm.

We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used an explicit source of randomness to reason about higher-order probabilistic programs.

We present a new behavioural distance over the state space of a Markov decision process, and demonstrate the use of this distance as an effective means of shaping the learnt representations of deep reinforcement learning agents. While existing notions of state similarity are typically difficult to learn at scale due to high computational cost and lack of sample-based algorithms, our newly-proposed distance addresses both of these issues. In addition to providing detailed theoretical analyses, we provide empirical evidence that learning this distance alongside the value function yields structured and informative representations, including strong results on the Arcade Learning Environment benchmark.

We present a distributional approach to theoretical analyses of reinforcement learning algorithms for constant step-sizes. We demonstrate its effectiveness by presenting simple and unified proofs of convergence for a variety of commonly-used methods. We show that value-based methods such as TD(?) and Q-Learning have update rules which are contractive in the space of distributions of functions, thus establishing their exponentially fast convergence to a stationary distribution. We demonstrate that the stationary distribution obtained by any algorithm whose target is an expected Bellman update has a mean which is equal to the true value function. Furthermore, we establish that the distributions concentrate around their mean as the step-size shrinks. We further analyse the optimistic policy iteration algorithm, for which the contraction property does not hold, and formulate a probabilistic policy improvement property which entails the convergence of the algorithm.

The choice of approximate posterior distributions plays a central role in stochastic variational inference (SVI). One effective solution is the use of normalizing flows \cut{defined on Euclidean spaces} to construct flexible posterior distributions. However, one key limitation of existing normalizing flows is that they are restricted to the Euclidean space and are ill-equipped to model data with an underlying hierarchical structure. To address this fundamental limitation, we present the first extension of normalizing flows to hyperbolic spaces. We first elevate normalizing flows to hyperbolic spaces using coupling transforms defined on the tangent bundle, termed Tangent Coupling ($\mathcal{TC}$). We further introduce Wrapped Hyperboloid Coupling ($\mathcal{W}\mathbb{H}C$), a fully invertible and learnable transformation that explicitly utilizes the geometric structure of hyperbolic spaces, allowing for expressive posteriors while being efficient to sample from. We demonstrate the efficacy of our novel normalizing flow over hyperbolic VAEs and Euclidean normalizing flows. Our approach achieves improved performance on density estimation, as well as reconstruction of real-world graph data, which exhibit a hierarchical structure. Finally, we show that our approach can be used to power a generative model over hierarchical data using hyperbolic latent variables.

Bisimulation is a concept that captures behavioural equivalence of states in a transition system. In [Linan Chen, Florence Clerc, and Prakash Panangaden, Bisimulation for feller-dynkin processes, in: Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science 347 (2019) 45–63.], we proposed two equivalent definitions of bisimulation on continuous-time stochastic processes where the evolution is a flow through time. In the present paper, we develop the theory further: we introduce different concepts that correspond to different behavioural equivalences and compare them to bisimulation. In particular, we study the relation between bisimulation and symmetry groups of the dynamics. We also provide a game interpretation for two of the behavioural equivalences. We then compare those notions to their discrete-time analogues.

Abstract The present paper uses spectral theory of linear operators to construct approximatelyminimal realizations of weighted languages. Our new contributions are: (i) a new algorithm for the singular value decomposition (SVD) decomposition of finite-rank infinite Hankel matrices based on their representation in terms of weighted automata, (ii) a new canonical form for weighted automata arising from the SVD of its corresponding Hankelmatrix, and (iii) an algorithmto construct approximateminimizations of given weighted automata by truncating the canonical form.We give bounds on the quality of our approximation.

The ordinary untyped λ-calculus has a λ-theoretic model proposed in two related forms by Scott and Plotkin in the 1970s. Recently Scott showed how to introduce probability by extending these models with random variables. However, to reason about correctness and to add further features, it is useful to reinterpret the construction in a higher-order Boolean-valued model involving a measure algebra. We develop the semantics of an extended stochastic λ-calculus suitable for modeling a simple higher-order probabilistic programming language. We exhibit a number of key equations satisfied by the terms of our language. The terms are interpreted using a continuation-style semantics with an additional argument, an infinite sequence of coin tosses, which serves as a source of randomness. We also introduce a fixpoint operator as a new syntactic construct, as β-reduction turns out not to be sound for unrestricted terms. Finally, we develop a new notion of equality between terms interpreted in a measure algebra, allowing one to reason about terms that may not be equal almost everywhere. This provides a new framework and reasoning principles for probabilistic programs and their higher-order properties.

Markov processes are a fundamental model of probabilistic transition systems and are the underlying semantics of probabilistic programs. We give an algebraic axiomatisation of Markov processes using the framework of quantitative equational logic introduced in [13]. We present the theory in a structured way using work of Hyland et al. [9] on combining monads. We take the interpolative barycentric algebras of [13] which captures the Kantorovich metric and combine it with a theory of contractive operators to give the required axiomatisation of Markov processes both for discrete and continuous state spaces. This work apart from its intrinsic interest shows how one can extend the general notion of combining effects to the quantitative setting.

We develop a new bisimulation (pseudo)metric for weighted finite automata (WFA) that generalizes Boreale's linear bisimulation relation. Our metrics are induced by seminorms on the state space of WFA. Our development is based on spectral properties of sets of linear operators. In particular, the joint spectral radius of the transition matrices of WFA plays a central role. We also study continuity properties of the bisimulation pseudometric, establish an undecidability result for computing the metric, and give a preliminary account of applications to spectral learning of weighted automata.

Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. Logical characterizations of probabilistic bisimulation and simulation were given by Desharnais et al. These results hold for systems defined on analytic state spaces and assume that there are countably many labels in the case of bisimulation and finitely many labels in the case of simulation. In this paper, we first revisit these results by giving simpler and more streamlined proofs. In particular, our proof for simulation has the same structure as the one for bisimulation, relying on a new result of a topological nature. This departs from the known proof for this result, which uses domain theory techniques and falls out of a theory of approximation of Labelled Markov processes. Both our proofs assume the presence of countably many labels. We investigate the necessity of this assumption, and show that the logical characterization of bisimulation may fail when there are uncountably many labels. However, with a stronger assumption on the transition functions (continuity instead of just measurability), we can regain the logical characterization result, for arbitrarily many labels. These new results arose from a new game-theoretic way of understanding probabilistic simulation and bisimulation.

Stone duality relates logic, in the form of Boolean algebra, to spaces. Stone-type dualities abound in computer science and have been of great use in understanding the relationship between computational models and the languages used to reason about them. Recent work on probabilistic processes has established a Stone-type duality for a restricted class of Markov processes. The dual category was a new notion—Aumann algebras—which are Boolean algebras equipped with countable family of modalities indexed by rational probabilities. In this article we consider an alternative definition of Aumann algebra that leads to dual adjunction for Markov processes that is a duality for many measurable spaces occurring in practice. This extends a duality for measurable spaces due to Sikorski. In particular, we do not require that the probabilistic modalities preserve a distinguished base of clopen sets, nor that morphisms of Markov processes do so. The extra generality allows us to give a perspicuous definition of event bisimulation on Aumann algebras.

Quantitative algebras (QAs) are algebras over metric spaces defined by quantitative equational theories as introduced by us in 2016. They provide the mathematical foundation for metric semantics of probabilistic, stochastic and other quantitative systems. This paper considers the issue of axiomatizability of QAs. We investigate the entire spectrum of types of quantitative equations that can be used to axiomatize theories: (i) simple quantitative equations; (ii) Horn clauses with no more than c equations between variables as hypotheses, where c is a cardinal and (iii) the most general case of Horn clauses. In each case we characterize the class of QAs and prove variety/quasivariety theorems that extend and generalize classical results from model theory for algebras and first-order structures.

We develop a quantitative analogue of equational reasoning which we call quantitative algebra. We define an equality relation indexed by rationals: a = ε b which we think of as saying that "a is approximately equal to b up to an error of ε ". We have 4 interesting examples where we have a quantitative equational theory whose free algebras correspond to well known structures. In each case we have finitary and continuous versions. The four cases are: Hausdorff metrics from quantitive semilattices; p-Wasserstein metrics (hence also the Kantorovich metric) from barycentric algebras and also from pointed barycentric algebras and the total variation metric from a variant of barycentric algebras.

We provide a novel, flexible, iterative refinement algorithm to automatically construct an approximate statespace representation for Markov Decision Processes (MDPs). Our approach leverages bisimulation metrics, which have been used in prior work to generate features to represent the state space of MDPs. We address a drawback of this approach, which is the expensive computation of the bisimulation metrics. We propose an algorithm to generate an iteratively improving sequence of state space partitions. Partial metric computations guide the representation search and provide much lower space and computational complexity, while maintaining strong convergence properties. We provide theoretical results guaranteeing convergence as well as experimental illustrations of the accuracy and savings (in time and memory usage) of the new algorithm, compared to traditional bisimulation metric computation.

We provide a novel, flexible, iterative refinement algorithm to automatically construct an approximate statespace representation for Markov Decision Processes (MDPs). Our approach leverages bisimulation metrics, which have been used in prior work to generate features to represent the state space of MDPs.We address a drawback of this approach, which is the expensive computation of the bisimulation metrics. We propose an algorithm to generate an iteratively improving sequence of state space partitions. Partial metric computations guide the representation search and provide much lower space and computational complexity, while maintaining strong convergence properties. We provide theoretical results guaranteeing convergence as well as experimental illustrations of the accuracy and savings (in time and memory usage) of the new algorithm, compared to traditional bisimulation metric computation.

We study the problem of constructing approximations to a weighted automaton. Weighted finite automata (WFA) are closely related to the theory of rational series. A rational series is a function from strings to real numbers that can be computed by a WFA. Among others, this includes probability distributions generated by hidden Markov models and probabilistic automata. The relationship between rational series and WFA is analogous to the relationship between regular languages and ordinary automata. Associated with such rational series are infinite matrices called Hankel matrices which play a fundamental role in the theory of minimal WFA. Our contributions are: (1) an effective procedure for computing the singular value decomposition (SVD) of such infinite Hankel matrices based on their finite representation in terms of WFA, (2) a new canonical form for WFA based on this SVD decomposition, and, (3) an algorithm to construct approximate minimizations of a given WFA. The goal of our approximate minimization algorithm is to start from a minimal WFA and produce a smaller WFA that is close to the given one in a certain sense. The desired size of the approximating automaton is given as input. We give bounds describing how well the approximation emulates the behavior of the original WFA. The study of this problem is motivated by the analysis of machine learning algorithms that synthesize weighted automata from spectral decompositions of finite Hankel matrices. It is known that when the number of states of the target automaton is correctly guessed, these algorithms enjoy consistency and finite-sample guarantees in the probably approximately correct (PAC) learning model. It has also been suggested that asking the learning algorithm to produce a model smaller than the true one will still yield useful models with reduced complexity. Our results in this paper vindicate these ideas and confirm intuitions provided by empirical studies. Beyond learning problems, our techniques can also be used to reduce the complexity of any algorithm working with WFA, at the expense of incurring a small, controlled amount of error.

We provide a theoretical framework for analyzing basis function construction for linear value function approximation in Markov Decision Processes (MDPs). We show that important existing methods, such as Krylov bases and Bellman-error-based methods are a special case of the general framework we develop. We provide a general algorithmic framework for computing basis function refinements which “respect” the dynamics of the environment, and we derive approximation error bounds that apply for any algorithm respecting this general framework. We also show how, using ideas related to bisimulation metrics, one can translate basis refinement into a process of finding “prototypes” that are diverse enough to represent the given MDP.

Functional Reactive Programming (FRP) models reactive systems with events and signals, which have previously been observed to correspond to the "eventually" and "always" modalities of linear temporal logic (LTL). In this paper, we define a constructive variant of LTL with least fixed point and greatest fixed point operators in the spirit of the modal mu-calculus, and give it a proofs-as-programs interpretation as a foundational calculus for reactive programs. Previous work emphasized the propositions-as-types part of the correspondence between LTL and FRP; here we emphasize the proofs-as-programs part by employing structural proof theory. We show that the type system is expressive enough to enforce liveness properties such as the fairness of schedulers and the eventual delivery of results. We illustrate programming in this calculus using (co)iteration operators. We prove type preservation of our operational semantics, which guarantees that our programs are causal. We give also a proof of strong normalization which provides justification that our programs are productive and that they satisfy liveness properties derived from their types.

Normally, one thinks of probabilistic transition systems as taking an initial probability distribution over the state space into a new probability distribution representing the system after a transition. We, however, take a dual view of Markov processes as transformers of bounded measurable functions. This is very much in the same spirit as a “predicate-transformer” view, which is dual to the state-transformer view of transition systems. We redevelop the theory of labelled Markov processes from this viewpoint; in particular, we explore approximation theory. We obtain three main results. (i) It is possible to define bisimulation on general measure spaces and show that it is an equivalence relation. The logical characterization of bisimulation can be done straightforwardly and generally. (ii) A new and flexible approach to approximation based on averaging can be given. This vastly generalizes and streamlines the idea of using conditional expectations to compute approximations. (iii) We show that there is a minimal process bisimulation-equivalent to a given process, and this minimal process is obtained as the limit of the finite approximants.

We give a new presentation of Brzozowski's algorithm to minimize finite automata using elementary facts from universal algebra and coalgebra and building on earlier work by Arbib and Manes on a categorical presentation of Kalman duality between reachability and observability. This leads to a simple proof of its correctness and opens the door to further generalizations. Notably, we derive algorithms to obtain minimal language equivalent automata from Moore nondeterministic and weighted automata.

We define Aumann algebras, an algebraic analog of probabilistic modal logic. An Aumann algebra consists of a Boolean algebra with operators modeling probabilistic transitions. We prove a Stone-type duality theorem between countable Aumann algebras and countably-generated continuous-space Markov processes. Our results subsume existing results on completeness of probabilistic modal logics for Markov processes.

I give a brief introduction to Stone duality and then survey a number of duality theories that arise in logic and computer science. I mention some more unfamiliar dualities at the end which may be of importance to emerging fields within computer science.

The scope of computation has expanded dramatically beyond the rubric of discrete, deterministic sequential computation under which it has been studied for many decades. That focus, of course, led to a great deal of deep and beautiful theory, but our focus in this special issue of Mathematical Structures in Computer Science is on new directions that have emerged from the study of computational phenomena in other settings, and thus on a celebration of the diversity of ideas, methods, new applications and novel sources of inspiration that have marked the modern era. The papers in this issue come from sources extending far beyond the core of computer science, yet using many of the central ideas that have evolved within computer science and mathematics. The nexus of all this activity has been, on the one hand, the boundary between logic and computation, and, on the other hand, the natural sciences, particularly physics and biology. The papers in this collection are expanded versions of selected papers from the DCM 2010 workshop, which was held in Edinburgh in July 2010. The theme of the workshop was Causality, Computation and Physics.

We develop a game semantics for process algebra with two interacting agents. The purpose of our semantics is to make manifest the role of knowledge and information flow in the interactions between agents and to control the information available to interacting agents. We define games and strategies on process algebras, so that two agents interacting according to their strategies determine the execution of the process, replacing the traditional scheduler. We show that different restrictions on strategies represent different amounts of information being available to a scheduler. We also show that a certain class of strategies corresponds to the syntactic schedulers of Chatzikokolakis and Palamidessi, which were developed to overcome problems with traditional schedulers modelling interaction. The restrictions on these strategies have an explicit epistemic flavour.

I will present three main themes in current research in semantics: (a) models of programming languages, (b) concurrency and (c) approximation. The first theme covers denotational semantics and operational semantics and the search for tight connections between them. This led to the full abstraction problem and ultimately to game semantics. The second theme began with the attempt to understand processes and the realization that there were brand new issues to deal with. In particular it was hard to even find compositional models at first. Finally, domain theory originally invented to provide set-theoretic models of the lambda calculus, turned into a general theory of approximation and has had an impact on the theory of probabilistic processes.

In recent years, various metrics have been developed for measuring the behavioral similarity of states in probabilistic transition systems [J. Desharnais et al., Proceedings of CONCUR'99, Springer-Verlag, London, 1999, pp. 258–273; F. van Breugel and J. Worrell, Proceedings of ICALP'01, Springer-Verlag, London, 2001, pp. 421–432]. In the context of finite Markov decision processes (MDPs), we have built on these metrics to provide a robust quantitative analogue of stochastic bisimulation [N. Ferns, P. Panangaden, and D. Precup, Proceedings of UAI-04, AUAI Press, Arlington, VA, 2004, pp. 162–169] and an efficient algorithm for its calculation [N. Ferns, P. Panangaden, and D. Precup, Proceedings of UAI-06, AUAI Press, Arlington, VA, 2006, pp. 174–181]. In this paper, we seek to properly extend these bisimulation metrics to MDPs with continuous state spaces. In particular, we provide the first distance-estimation scheme for metrics based on bisimulation for continuous probabilistic transition systems. Our work, based on statistical sampling and infinite dimensional linear programming, is a crucial first step in formally guiding real-world planning, where tasks are usually continuous and highly stochastic in nature, e.g., robot navigation, and often a substitution with a parametric model or crude finite approximation must be made. We show that the optimal value function associated with a discounted infinite-horizon planning task is continuous with respect to metric distances. Thus, our metrics allow one to reason about the quality of solution obtained by replacing one model with another. Alternatively, they may potentially be used directly for state aggregation.

We define a metric for measuring behavior similarity between states in a Markov decision process (MDP), in which action similarity is taken into account. We show that the kernel of our metric corresponds exactly to the classes of states defined by MDP homomorphisms (Ravindran & Barto, 2003). We prove that the difference in the optimal value function of different states can be upper-bounded by the value of this metric, and that the bound is tighter than that provided by bisimulation metrics (Ferns et al. 2004, 2005). Our results hold both for discrete and for continuous actions. We provide an algorithm for constructing approximate homomorphisms, by using this metric to identify states that can be grouped together, as well as actions that can be matched. Previous research on this topic is based mainly on heuristics.

Randomized protocols for hiding private information can be regarded as noisy channels in the information-theoretic sense, and the inference of the concealed information can be regarded as a hypothesis-testing problem. We consider the Bayesian approac

Randomized protocols for hiding private information can fruitfully be regarded as noisy channels in the information-theoretic sense, and the inference of the concealed information can be regarded as a hypothesis-testing problem. We consider the Bayesian approach to the problem, and investigate the probability of error associated to the inference when the MAP (maximum aposteriori probability) decision rule is adopted. Our main result is a constructive characterization of a convex base of the probability of error, which allows us to compute its maximum value (over all possible input distributions), and to identify upper bounds for it in terms of simple functions. As a side result, we are able to improve substantially the Hellman-Raviv and the Santhi-Vardy bounds expressed in terms of conditional entropy. We then discuss an application of our methodology to the Crowds protocol, and in particular we show how to compute the bounds on the probability that an adversary breaks anonymity.

Measurement-based quantum computation has emerged from the physics community as a new approach to quantum computation where the notion of measurement is the main driving force of computation. This is in contrast with the more traditional circuit model that is based on unitary operations. Among measurement-based quantum computation methods, the recently introduced one-way quantum computer [Raussendorf and Briegel 2001] stands out as fundamental. We develop a rigorous mathematical model underlying the one-way quantum computer and present a concrete syntax and operational semantics for programs, which we call patterns , and an algebra of these patterns derived from a denotational semantics. More importantly, we present a calculus for reasoning locally and compositionally about these patterns. We present a rewrite theory and prove a general standardization theorem which allows all patterns to be put in a semantically equivalent standard form. Standardization has far-reaching consequences: a new physical architecture based on performing all the entanglement in the beginning, parallelization by exposing the dependency structure of measurements and expressiveness theorems. Furthermore we formalize several other measurement-based models, for example, Teleportation, Phase and Pauli models and present compositional embeddings of them into and from the one-way model. This allows us to transfer all the theory we develop for the one-way model to these models. This shows that the framework we have developed has a general impact on measurement-based computation and is not just particular to the one-way quantum computer.

We develop a pseudo-metric analogue of bisimulation for generalized semi-Markov processes. The kernel of this pseudo-metric corresponds to bisimulation; thus we have extended bisimulation for continuous-time probabilistic processes to a much broader class of distributions than exponential distributions. This pseudo-metric gives a useful handle on approximate reasoning in the presence of numerical information -- such as probabilities and time -- in the model. We give a fixed point characterization of the pseudo-metric. This makes available coinductive reasoning principles for reasoning about distances. We demonstrate that our approach is insensitive to potentially ad hoc articulations of distance by showing that it is intrinsic to an underlying uniformity. We provide a logical characterization of this uniformity using a real-valued modal logic. We show that several quantitative properties of interest are continuous with respect to the pseudo-metric. Thus, if two processes are metrically close, then observable quantitative properties of interest are indeed close.

We develop a notion of predicate transformer and, in particular, the weakest precondition, appropriate for quantum computation. We show that there is a Stone-type duality between the usual state-transformer semantics and the weakest precondition semantics. Rather than trying to reduce quantum computation to probabilistic programming, we develop a notion that is directly taken from concepts used in quantum computation. The proof that weakest preconditions exist for completely positive maps follows immediately from the Kraus representation theorem. As an example, we give the semantics of Selinger's language in terms of our weakest preconditions. We also cover some specific situations and exhibit an interesting link with stabilisers.

We recast dataflow in a modern categorical light using profunctors as a generalisation of relations. The well-known causal anomalies associated with relational semantics of indeterminate dataflow are avoided, but still we preserve much of the intuitions of a relational model. The development fits with the view of categories of models for concurrency and the general treatment of bisimulation they provide. In particular, it fits with the recent categorical formulation of feedback using traced monoidal categories. The payoffs are: (1) explicit relations to existing models and semantics, especially the usual axioms of monotone IO automata are read off from the definition of profunctors; (2) a new definition of bisimulation for dataflow, the proof of the congruence of which benefits from the preservation properties associated with open maps; and (3) a treatment of higher-order dataflow as a biproduct, essentially by following the geometry of interaction programme.

We observe that equivalence is not a robust concept in the presence of numerical information - such as probabilities-in the model. We develop a metric analogue of weak bisimulation in the spirit of our earlier work on metric analogues for strong bisimulation. We give a fixed point characterization of the metric. This makes available conductive reasoning principles and allows us to prove metric analogues of the usual algebraic laws for process combinators. We also show that quantitative properties of interest are continuous with respect to the metric, which says that if two processes are close in the metric then observable quantitative properties of interest are indeed close. As an important example of this we show that nearby processes have nearby channel capacities - a quantitative measure of their propensity to leak information.

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.

No abstract available.

) Vineet Gupta Radha Jagadeesan Prakash Panangaden y [email protected] [email protected] [email protected] Caelum Research Corporation Dept. of Math. and Computer Sciences School of Computer Science NASA Ames Research Center Loyola University--Lake Shore Campus McGill University Moffett Field CA 94035, USA Chicago IL 60626, USA Montreal, Quebec, Canada Abstract This paper describes a stochastic concurrent constraint language for the description and programming of concurrent probabilistic systems. The language can be viewed both as a calculus for describing and reasoning about stochastic processes and as an executable language for simulating stochastic processes. In this language programs encode probability distributions over (potentially infinite) sets of objects. We illustrate the subtleties that arise from the interaction of constraints, random choice and recursion. We describe operational semantics of these programs (programs are run by sampling random choices), deno...

This paper gives a logical characterization of probabilistic bisimulation for Markov processes. Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition. Bisimulation can be characterized by several inequivalent logics; we report five in this paper and there are surely many more. We do not need any finite branching assumption yet there is no need of infinitely conjunction. We give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.

In this paper we introduce a new class of labelled transition systems-Labelled Markov Processes-and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete, it could be the reals, for example. We assume that it is a Polish space (the underlying topological space for a complete separable metric space). The mathematical theory of such systems is completely new from the point of view of the extant literature on probabilistic process algebra; of course, it uses classical ideas from measure theory and Markov process theory. The notion of bisimulation builds on the ideas of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result that we prove is that a notion of bisimulation for Markov processes on Polish spaces, which extends the Larsen-Skou definition for discrete systems, is indeed an equivalence relation. This turns our to be a rather hard mathematical result which, as far as we know, embodies a new result in pure probability theory. This work heavily uses continuous mathematics which is becoming an important part of work on hybrid systems.

In this paper we establish new expressiveness results for indeterminate datatlow primitives. We consider split primitives with three differing fairness assumptions and show that they are strictly inequivalent in expressive power. We also show that the ability to announce internal choices enhances the expressive power of two of the primitives. These results are proved using a very crude notion of observation and thus apply in any reasonable theory of process equivalence.

Accumulation of tokens on the arcs of a dataflow program operating on potentially infinite streams in a DSP computation leads to unbounded storage requirement. Compile-time techniques to determine the storage requirement are essential for efficient scheduling. A class of program graphs called regular stream flow graphs is studied. Restricting the construction to a set of construction rules facilitates compile-time predictability of storage requirement. Compared to existing methods, the model has a stronger verifiability, which is due to the structure of the well-constructed graphs.>

We analyze the relative expressive power of variants of the indeterminate fair merge operator in the context of static dataflow. We establish that there are three different, provably inequivalent, forms of unbounded indeterminacy. In particular, we show that the well-known fair merge primitive cannot be expressed with just unbounded indeterminacy. Our proofs are based on a simple trace semantics and on identifying properties of the behaviors of networks that are invariant under network composition. The properties we consider in this paper are all generalizations of monotonicity.

A formal framework called Security Logic ( SL ) is developed for specifying and reasoning about security policies and for verifying that system designs adhere to such policies. Included in this modal logic framework are definitions of knowledge, permission, and obligation . Permission is used to specify secrecy policies and obligation to specify integrity policies. The combination of policies is addressed and examples based on policies from the current literature are given.

Concurrent constraint programming [Sar89 ,SR90] is a simple and powerful model of concurrent computation based on the notions of store-as-constraint and process as information combinators in the language, can be used for proving liveness properties of programs, and is fully abstract with respect to the obvious notion of observation.

There is much interest in combining the functional and logic programming paradigms � in particular, there have been several proposals for adding logic variables to functional languages, since that permits incremental construction of data structures through constraint intersection. While it is straight-forward to give an abstract semantics for functional languages and for logic languages, it has proven surprisingly di cult to give a proper semantic account of functional languages with logic variables. In this paper, we present a rst-order functional language with logic variables and give its meaning using a structural operational semantics. We also give it a denotational semantics, using a novel technique involving closure operators on a Scott domain. Finally, we show that these two semantics correspond in the strongest possible way|weshow that the denotational semantics is fully abstract with respect to the operational semantics. The techniques developed in this paper are quite general, and can be used to give semantics to any constraint-based logic programming languages. Our results can also be interpreted as a generalization of Kahn semantics for data ow networks in which processes not only exchange messages, but have access to a shared global address space in which variables are bound through constraint intersection. Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Functional Programming � D.3.1 [Programming Languages]: Formal De nitions and Theory- semantics � D.3.2 [Programming Languages]: Data ow Languages � F.3.2 [Theory of Computation]: Semantics of Programming Languages- denotational semantics � F.4.1 [Theory of Computation]: Mathematical Logic- logic programming

A formal framework called security logic (SL) is developed for specifying and reasoning about security policies, and for verifying that system designs adhere to such policies. Included in this framework is a definition of knowledge based on modal logic so that properties can be time-related, a definition of permission, and a definition of obligation. Permission is used to specify secrecy policies, and obligation is used to specify integrity policies. A security policy is given as a set of policy constraints on the SL model. The combination of policies is addressed. Examples based on policies from the current literature are given.>

There is much interest in the declarative languages community in integrating logic variables into functional languages. The authors give a full semantic account of such a language. They present a Plotkin-style operational semantics for the language and an abstract semantics that expresses meanings as closure operators on a Scott domain. They also show that the denotational semantics is fully abstract with respect to the operational semantics.>

Expressiveness results for indeterminate data flow primitives are established. Choice primitives with three differing fairness assumptions are considered, and it is shown that they are strictly inequivalent in expressive power. It is also shown that the ability to announce choices enhances the expressive power of two of the primitives. These results are proved using a very crude semantics and will thus apply in any reasonable theory of process equivalence.>

In this paper we discuss a new knowledgetheoretic definition of agreement appropriate to asynchronous systems.This definition has two important features; first, it uses causality rather than time in its definition and, second, this form of agreement is attainable.In analogy with common knowledge, it is called concurrent common knowledge.Concurrent common knowledge has several applications and we give analyses of two examples that use it.In general, it seems to be the case that applications that involve all processes reaching agreement about some property of a consistent global state are protocols that use concurrent common knowledge.

We provide a scheme for determining which global variables are involved when an expression is evaluated in a language with higher order constructs and imperative features. The heart of our scheme is a mechanism for computing the support of an expression, i.e. the set of global variables involved in its evaluation. This computation requires knowledge of all the aliases of an expression. The inference schemes are presented as abstract semantic interpretations. We prove the soundness of our estimates by establishing a correspondence between the abstract semantics and the standard semantics of the programming language.