Search

Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, which guarantees that if an implementation satisfying certain conditions passes all tests, then it is equivalent to the specification. We introduce a framework for proving completeness of test suites at the general level of automata in monoidal closed categories. Moreover, we provide a generalization of a classical conformance testing technique, the W-method. We demonstrate the applicability of our results by recovering the W-method for deterministic finite automata, Moore machines, and Mealy machines, and by deriving new instances of complete test suites for weighted automata and deterministic nominal automata.

The Kantorovich distance is a widely used metric between probability distributions. The Kantorovich-Rubinstein duality states that it can be defined in two equivalent ways: as a supremum, based on non-expansive functions into [0, 1], and as an infimum, based on probabilistic couplings.Orthogonally, there are categorical generalisations of both presentations proposed in the literature, in the form of codensity liftings and what we refer to as coupling-based liftings. Both lift endofunctors on the category Set of sets and functions to that of pseudometric spaces, and both are parameterised by modalities from coalgebraic modal logic. A generalisation of the Kantorovich-Rubinstein duality has been more nebulous-it is known not to work in some cases. In this paper we propose a compositional approach for obtaining such generalised dualities for a class of functors, which is closed under coproducts and products. Our approach is based on an explicit construction of modalities and also applies to and extends known cases such as that of the powerset functor.

Geuvers and Jacobs (LMCS 2021) formulated the notion of apartness relation on state-based systems modelled as coalgebras. In this context apartness is formally dual to bisimilarity, and gives an explicit proof system for showing that certain states are not bisimilar. In the current paper, we relate apartness to another classical element of the theory of behavioural equivalences: that of turn-based two-player games. Studying both strong and branching bisimilarity, we show that winning configurations for the Spoiler player correspond to apartness proofs, for transition systems that are image-finite (in the case of strong bisimilarity) and finite (in the case of branching bisimilarity).

While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances.

Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temporal inference: to compute the likelihood that the execution traces satisfy a given temporal property. This paper presents a general framework for temporal inference, which applies to a rich variety of quantitative models including those that arise in the operational semantics of probabilistic and weighted programs. The key idea underlying our framework is that in a variety of existing approaches, the main construction that enables temporal inference is that of a product between the system of interest and the temporal property. We provide a unifying mathematical definition of product constructions, enabled by the realisation that 1) both systems and temporal properties can be modelled as coalgebras and 2) product constructions are distributive laws in this context. Our categorical framework leads us to our main contribution: a sufficient condition for correctness, which is precisely what enables to use the product construction for temporal inference. We show that our framework can be instantiated to naturally recover a number of disparate approaches from the literature including, e.g., partial expected rewards in Markov reward models, resource-sensitive reachability analysis, and weighted optimization problems. Further, we demonstrate a product of weighted programs and weighted temporal properties as a new instance to show the scalability of our approach., Comment: Preprint

Active automata learning (AAL) is a method to infer state machines by interacting with black-box systems. Adaptive AAL aims to reduce the sample complexity of AAL by incorporating domain specific knowledge in the form of (similar) reference models. Such reference models appear naturally when learning multiple versions or variants of a software system. In this paper, we present state matching, which allows flexible use of the structure of these reference models by the learner. State matching is the main ingredient of adaptive L#, a novel framework for adaptive learning, built on top of L#. Our empirical evaluation shows that adaptive L# improves the state of the art by up to two orders of magnitude., Comment: Extended paper for FM 2024

We define a framework for incorporating alternation-free fixpoint logics into the dual-adjunction setup for coalgebraic modal logics. We achieve this by using order-enriched categories. We give a least-solution semantics as well as an initial algebra semantics, and prove they are equivalent. We also show how to place the alternation-free coalgebraic $\mu$-calculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality.

Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems. We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples.

In this paper, two mesh-free CFD solvers for pore-scale fluid flow through porous media are considered, namely the Lattice Boltzmann Method with the two relaxation time collision term and the direct Navier-Stokes solver under the artificial compressibility limit. The porous media is built with a regular arrangement of spherical grains with variable radii, which allows control of the porosity. Both solvers use the same h-refined meshless spatial discretization to adequately capture the underlying geometry and the same Radial Basis Function (RBF) method to approximate the involved fields and partial differential operators. First, the results are compared with the data from the literature in terms of drag coefficient and permeability at different porosities achieving excellent agreement with the reported results. Next, the simulations are extended beyond the porosity range reported in the literature using proposed h-refined CFD solvers. The results are supported by convergence and timing analyses and discussions on meshless parameters such as stencil size and refinement settings.

Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system. In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality. ..., Comment: Extended version (includes the Appendix) of the paper accepted at LiCS-24

In this paper, we address a way to reduce the total computational cost of meshless approximation by reducing the required stencil size through spatially varying computational node regularity. Rather than covering the entire domain with scattered nodes, only regions with geometric details are covered with scattered nodes, while the rest of the domain is discretized with regular nodes. A simpler approximation can be used in regions covered by regular nodes, effectively reducing the required stencil size and computational cost compared to the approximation on scattered nodes where a set of polyharmonic splines is added to ensure convergent behaviour. This paper is an extended version of conference paper entitled "Spatially-varying meshless approximation method for enhanced computational efficiency" [arXiv:2303.01760] presented at "International Conference on Computational Science (ICCS) 2023". The paper is extended with discussion on development and implementation of a hybrid regular-scattered node positioning algorithm (HyNP). The performance of the proposed HyNP algorithm is analysed in terms of separation distance and maximal empty sphere radius. Furthermore, it is demonstrated that HyNP nodes can be used for solving problems from fluid flow and linear elasticity, both in 2D and 3D, using meshless methods. The extension also provides additional analyses of computational efficiency and accuracy of the numerical solution obtained on the spatially-variable regularity of discretization nodes. In particular, different levels of refinement aggressiveness and scattered layer widths are considered to exploit the computational efficiency gains offered by such solution procedure., Comment: 36 pages, 23 figures; Submitted to the Journal of Computational Science as an extension of arXiv:2303.01760. arXiv admin note: text overlap with arXiv:2303.01760

When solving partial differential equations on scattered nodes using the Radial Basis Function-generated Finite Difference (RBF-FD) method, one of the parameters that must be chosen is the stencil size. Focusing on Polyharmonic Spline RBFs with monomial augmentation, we observe that it affects the approximation accuracy in a particularly interesting way - the solution error oscillates under increasing stencil size. We find that we can connect this behaviour with the spatial dependence of the signed approximation error. Based on this observation we are able to introduce a numerical quantity that could indicate whether a given stencil size is locally optimal. This work is an extension of our ICCS 2023 conference paper., Comment: 41 pages, 18 Figures, Submitted to the Journal of Computational Science. arXiv admin note: text overlap with arXiv:2303.02252

The numerical stability of fluid flow is an important topic in computational fluid dynamics as fluid flow simulations usually become numerically unstable in the turbulent regime. Many mesh-based methods have already established numerical dissipation procedures that dampen the effects of the unstable advection term. When it comes to meshless methods, the prominent stabilisation scheme is hyperviscosity. It introduces numerical dissipation in the form of a higher-order Laplacian operator. Many papers have already discussed the general effects of hyperviscosity and its parameters. However, hyperviscosity in flow problems has not yet been analyzed in depth. In this paper, we discuss the effects of hyperviscosity on natural convection flow problems as we approach the turbulent regime., Comment: 6 pages, 4 figures, prepared for EUROTHERM 2024

On 13-01-2024 the annual wintersymposium of the Koninlijk Wiskundig Genootschap (KWG) was held in the academiegebouw in Utrecht. The symposium had the theme ``inzichtelijk abstract''. Thomas Rot gave a lecture on his favourite theorem from topology. This article is a written account of this lecture. Audience comprised mostly of high school teachers and that is also the target audience of this article. The slides (in Dutch), which contain more pictures, are available~[8]., Comment: Expository article, to appear in the Nieuw Archief voor Wiskunde

A bottleneck in modern active automata learning is to test whether a hypothesized Mealy machine correctly describes the system under learning. The search space for possible counterexamples is given by so-called test suites, consisting of input sequences that have to be checked to decide whether a counterexample exists. This paper shows that significantly smaller test suites suffice under reasonable assumptions on the structure of the black box. These smaller test suites help to refute false hypotheses during active automata learning, even when the assumptions do not hold. We combine multiple test suites using a multi-armed bandit setup that adaptively selects a test suite. An extensive empirical evaluation shows the efficacy of our approach. For small to medium-sized models, the performance gain is limited. However, the approach allows learning models from large, industrial case studies that were beyond the reach of known methods., Comment: Extended paper for TACAS 2024

We classify non-linear proper Fredholm maps between Hilbert spaces, up to proper homotopy, in terms of the stable homotopy groups of spheres. We show that there is a surjective map from the stable homotopy groups of spheres to the set of non-linear proper Fredholm maps up to proper homotopy and determine the non-trivial kernel. We also discuss the case of oriented non-linear proper Fredholm maps which are in bijection with the stable homotopy groups of spheres., Comment: 9 pages. Comments welcome

Using geometric arguments, we compute the group of homotopy classes of maps from a closed $(n+1)$-dimensional manifold to the $n$-sphere for $n \geq 3$. Our work extends results from Kirby, Melvin and Teichner for closed oriented 4-manifolds and from Konstantis for closed $(n+1)$-dimensional spin manifolds, considering possibly non-orientable and non-spinnable manifolds. In the process, we introduce two types of manifolds that generalize the notion of odd and even 4-manifolds. Furthermore, for the case that $n \geq 4$, we discuss applications for rank $n$ spin vector bundles and obtain a refinement of the Euler class in the cohomotopy group that fully obstructs the existence of a non-vanishing section., Comment: cleaner argument for framings on surfaces, removed equation number without reference

Given an arbitrary basis for a mathematical lattice, to find a ``good" basis for it is one of the classic and important algorithmic problems. In this note, we give a new and simpler proof of a theorem by Regavim (arXiv:2106.03183): we construct a 18-dimensional lattice that does not have a basis that satisfies the following two properties simultaneously: 1. The basis includes the shortest non-zero lattice vector. 2. The basis is shortest, that is, minimizes the longest basis vector (alternatively: the sum or the sum-of-squares of the basis vectors). The vectors' length can be measured in any $\ell^q$ norm, for $q\in \mathbb{N}_+$ (albeit, via another lattice, of a somewhat larger dimension)., Comment: 16 pages

We provide a categorical notion called uncertain bisimilarity, which allows to reason about bisimilarity in combination with a lack of knowledge about the involved systems. Such uncertainty arises naturally in automata learning algorithms, where one investigates whether two observed behaviours come from the same internal state of a black-box system that can not be transparently inspected. We model this uncertainty as a set functor equipped with a partial order which describes possible future developments of the learning game. On such a functor, we provide a lifting-based definition of uncertain bisimilarity and verify basic properties. Beside its applications to Mealy machines, a natural model for automata learning, our framework also instantiates to an existing compatibility relation on suspension automata, which are used in model-based testing. We show that uncertain bisimilarity is a necessary but not sufficient condition for two states being implementable by the same state in the black-box system. To remedy the failure of the one direction, we characterize uncertain bisimilarity in terms of coalgebraic simulations.

When solving partial differential equations on scattered nodes using the Radial Basis Function generated Finite Difference (RBF-FD) method, one of the parameters that must be chosen is the stencil size. Focusing on Polyharmonic Spline RBFs with monomial augmentation, we observe that it affects the approximation accuracy in a particularly interesting way - the solution error oscillates under increasing stencil size. We find that we can connect this behaviour with the spatial dependence of the signed approximation error. Based on this observation we are then able to introduce a numerical quantity that indicates whether a given stencil size is locally optimal., Comment: 8 pages, 6 figures, ICCS 2023 Conference Paper

In this paper, we address a way to reduce the total computational cost of meshless approximation by reducing the required stencil size through spatial variation of computational node regularity. Rather than covering the entire domain with scattered nodes, only regions with geometric details are covered with scattered nodes, while the rest of the domain is discretised with regular nodes. Consequently, in regions covered with regular nodes the approximation using solely the monomial basis can be performed, effectively reducing the required stencil size compared to the approximation on scattered nodes where a set of polyharmonic splines is added to ensure convergent behaviour. The performance of the proposed hybrid scattered-regular approximation approach, in terms of computational efficiency and accuracy of the numerical solution, is studied on natural convection driven fluid flow problems. We start with the solution of the de Vahl Davis benchmark case, defined on square domain, and continue with two- and three-dimensional irregularly shaped domains. We show that the spatial variation of the two approximation methods can significantly reduce the computational complexity, with only a minor impact on the solution accuracy., Comment: Preprint(reviewed)

Local Morse cohomology associates cohomology groups to isolating neighborhoods of gradient flows of Morse functions on (generally non-compact) Riemannian manifolds $M$. We show that local Morse cohomology is a module over the cohomology of the isolating neighborhood, which allows us to define a cup-length relative to the cohomology of the isolating neighborhood that gives a lower bound on the number of critical points of functions on $M$ that are not necessarily Morse. Finally, we illustrate by an example that this lower bound can indeed be stronger than the lower bound given by the absolute cup-length., Comment: Minor edits, final version

Soft-biometric privacy-enhancing techniques represent machine learning methods that aim to: (i) mitigate privacy concerns associated with face recognition technology by suppressing selected soft-biometric attributes in facial images (e.g., gender, age, ethnicity) and (ii) make unsolicited extraction of sensitive personal information infeasible. Because such techniques are increasingly used in real-world applications, it is imperative to understand to what extent the privacy enhancement can be inverted and how much attribute information can be recovered from privacy-enhanced images. While these aspects are critical, they have not been investigated in the literature. We, therefore, study the robustness of several state-of-the-art soft-biometric privacy-enhancing techniques to attribute recovery attempts. We propose PrivacyProber, a high-level framework for restoring soft-biometric information from privacy-enhanced facial images, and apply it for attribute recovery in comprehensive experiments on three public face datasets, i.e., LFW, MUCT and Adience. Our experiments show that the proposed framework is able to restore a considerable amount of suppressed information, regardless of the privacy-enhancing technique used, but also that there are significant differences between the considered privacy models. These results point to the need for novel mechanisms that can improve the robustness of existing privacy-enhancing techniques and secure them against potential adversaries trying to restore suppressed information.

In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.