This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The... Show moreThis paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The construction is essentially a generalisation of the topos of trees from the codomain fibration over sets to arbitrary fibrations. As a result, we obtain a framework that allows the addition of a recursion principle for coinduction to rather arbitrary logics and programming languages. The main interest of using recursion is that it allows one to write proofs and programs in a goal-oriented fashion. This enables easily understandable coinductive proofs and programs, and fosters automatic proof search. Part of the framework are also various results that enable a wide range of applications: transportation of (co)limits, exponentials, fibred adjunctions and first-order connectives from the initial fibration to the one constructed through the framework. This means that the framework extends any first-order logic with the later modality. Moreover, we obtain soundness and completeness results, and can use up-to techniques as proof rules. Since the construction works for a wide variety of fibrations, we will be able to use the recursion offered by the later modality in various context. For instance, we will show how recursive proofs can be obtained for arbitrary (syntactic) first-order logics, for coinductive set-predicates, and for the probabilistic modal mu-calculus. Finally, we use the same construction to obtain a novel language for probabilistic productive coinductive programming. These examples demonstrate the flexibility of the framework and its accompanying results. Show less
The goal of this paper is to learn the dynamics of truck co-driving behaviour. Understanding this behaviour is important because co-driving has a potential positive impact on the environment. In... Show moreThe goal of this paper is to learn the dynamics of truck co-driving behaviour. Understanding this behaviour is important because co-driving has a potential positive impact on the environment. In the so-called co-driving network, trucks are nodes while links indicate that two trucks frequently drive together. To understand the network’s dynamics, we use a link prediction approach employing a machine learning classifier. The features of the classifier can be categorized into spatio-temporal features, neighbourhood features, path features, and node features. The very different types of features allow us to understand the social processes underlying the co-driving behaviour. Our work is based on a spatio-temporal data not studied before. Data is collected from 18 million truck movements in the Netherlands. We find that co-driving behaviour is best described by using neighbourhood features, and to lesser extent by path and spatio-temporal features. Node features are deemed unimportant. Findings suggest that the dynamics of a truck co-driving network has clear social network effects. Show less
The LOFAR radio telescope is a low-frequency aperture synthesis radio telescope with headquarters in the Netherlands and stations across Europe. As a general purpose telescope, LOFAR produces... Show moreThe LOFAR radio telescope is a low-frequency aperture synthesis radio telescope with headquarters in the Netherlands and stations across Europe. As a general purpose telescope, LOFAR produces petabytes of data each year serving a wide range of science cases. The data volumes produced are difficult or impossible to process on a single machine or even a small cluster at a scientific institute. We provide a layout for serving LOFAR processing to the astronomical community by providing access to LOFAR pipelines accelerated on a high throughput platform. We build this on our previous success with parallelizing the LOFAR Surveys pipeline and with creating automated LOFAR workflows on a distributed architecture. The LOFAR As A Service platform will serve the LOFAR Key Science Projects (KSPs), specifically the LOFAR Surveys KSP, which aims to provide science ready products to the scientific community. Additionally, this system will provide a robust method to re-process LOFAR data with a single click. Show less
A number of data mining problems on probabilistic networks can be modelled as Stochastic Constraint Optimisation and Satisfaction Problems, i.e., problems that involve objectives or constraints... Show moreA number of data mining problems on probabilistic networks can be modelled as Stochastic Constraint Optimisation and Satisfaction Problems, i.e., problems that involve objectives or constraints with a stochastic component. Earlier methods for solving these problems used Ordered Binary Decision Diagrams (OBDDs) to represent constraints on probability distributions, which were decomposed into sets of smaller constraints and solved by Constraint Programming (CP) or Mixed Integer Programming (MIP) solvers. For the specific case of monotonic distributions, we propose an alternative method: a new propagator for a global OBDD-based constraint. We show that this propagator is efficient and maintains domain consistency. We experimentally evaluate this global constraint in comparison to existing decomposition-based approaches. As test cases we use problems from the data mining literature. Show less
We present a modular framework, the Workload Characterisation Framework (WCF), that is developed to obtain, store and compare key characteristics of radio astronomy processing software in a... Show moreWe present a modular framework, the Workload Characterisation Framework (WCF), that is developed to obtain, store and compare key characteristics of radio astronomy processing software in a reproducible way. As a demonstration, we discuss the experiences using the framework to characterise a LOFAR calibration and imaging pipeline. Show less
After the recent groundbreaking results of AlphaGo and AlphaZero, we have seen strong interests in deep reinforcement learning and artificial general intelligence (AGI) in game playing. However,... Show moreAfter the recent groundbreaking results of AlphaGo and AlphaZero, we have seen strong interests in deep reinforcement learning and artificial general intelligence (AGI) in game playing. However, deep learning is resource-intensive and the theory is not yet well developed. For small games, simple classical table-based Q-learning might still be the algorithm of choice. General Game Playing (GGP) provides a good testbed for reinforcement learning to research AGI. Q-learning is one of the canonical reinforcement learning methods, and has been used by (Banerjee & Stone, IJCAI 2007) in GGP. In this paper we implement Q-learning in GGP for three small-board games (Tic-Tac-Toe, Connect Four, Hex), to allow comparison to Banerjee et al. We find that Q-learning converges to a high win rate in GGP. For the ϵ" role="presentation" style="display: inline-table; line-height: normal; letter-spacing: normal; word-spacing: normal; overflow-wrap: normal; white-space: nowrap; float: none; direction: ltr; max-width: none; max-height: none; min-width: 0px; min-height: 0px; border-width: 0px; border-style: initial; position: relative;">ϵ-greedy strategy, we propose a first enhancement, the dynamic ϵ" role="presentation" style="display: inline-table; line-height: normal; letter-spacing: normal; word-spacing: normal; overflow-wrap: normal; white-space: nowrap; float: none; direction: ltr; max-width: none; max-height: none; min-width: 0px; min-height: 0px; border-width: 0px; border-style: initial; position: relative;">ϵ algorithm. In addition, inspired by (Gelly & Silver, ICML 2007) we combine online search (Monte Carlo Search) to enhance offline learning, and propose QM-learning for GGP. Both enhancements improve the performance of classical Q-learning. In this work, GGP allows us to show, if augmented by appropriate enhancements, that classical table-based Q-learning can perform well in small games. Show less
