arXiv subjects

Erik de Vink

Publications and source records attributed to Erik de Vink.

9 recordsLinked to original sources

arXiv2025

A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice

This paper proposes a notion of branching bisimilarity for non-deterministic probabilistic processes. In order to characterize the corresponding notion of rooted branching probabilistic bisimilarity, an equational theory is proposed for a basic, recursion-free process language with non-deterministic as well as probabilistic choice. The proof of completeness of the axiomatization builds on the completeness of strong probabilistic bisimilarity on the one hand and on the notion of a concrete process, i.e. a process that does not display (partially) inert $τ$-moves, on the other hand. The approach is first presented for the non-deterministic fragment of the calculus and next generalized to incorporate probabilistic choice, too.

cs.LO↗

arXiv2023

A Cancellation Law for Probabilistic Processes

We show a cancellation property for probabilistic choice. If distributions mu + rho and nu + rho are branching probabilistic bisimilar, then distributions mu and nu are also branching probabilistic bisimilar. We do this in the setting of a basic process language involving non-deterministic and probabilistic choice and define branching probabilistic bisimilarity on distributions. Despite the fact that the cancellation property is very elegant and concise, we failed to provide a short and natural combinatorial proof. Instead we provide a proof using metric topology. Our major lemma is that every distribution can be unfolded into an equivalent stable distribution, where the topological arguments are required to deal with uncountable branching.

cs.LO↗

arXiv2020

Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations

The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial structures, such as finite graphs and digital images, with applications in various case studies including medical image analysis. These recent developments required a generalisation step, from topological spaces to closure spaces. In this work we initiate the study of bisimilarity and minimisation algorithms that are consistent with the closure spaces semantics. For this purpose we employ coalgebraic models. We present a coalgebraic definition of bisimilarity for quasi-discrete models, which is adequate with respect to a spatial logic with reachability operators, complemented by a free and open-source minimisation tool for finite models. We also discuss the non-quasi-discrete case, by providing a generalisation of the well-known set-theoretical notion of topo-bisimilarity, and a categorical definition, in the same spirit as the coalgebraic rendition of neighbourhood frames, but employing the covariant power set functor, instead of the contravariant one. We prove its adequacy with respect to infinitary modal logic.

cs.LO↗

arXiv2017

Proceedings 15th Workshop on Quantitative Aspects of Programming Languages and Systems

This volume of the EPTCS contains the proceedings of the 15th international workshop on Qualitative Aspects of Programming Languages and Systems, QAPL 2017, held at April 23, 2017 in Uppsala, Sweden as a satellite event of ETAPS 2017, the 20th European Joint Conferencec on Theory and Practice of Software. The volume contains two invited contributions by Erika Abraham and by Andrea Vandin as well as six technical papers selected by the QAPL 2017 program committee.

cs.PL↗

arXiv2015

A Definition Scheme for Quantitative Bisimulation

FuTS, state-to-function transition systems are generalizations of labeled transition systems and of familiar notions of quantitative semantical models as continuous-time Markov chains, interactive Markov chains, and Markov automata. A general scheme for the definition of a notion of strong bisimulation associated with a FuTS is proposed. It is shown that this notion of bisimulation for a FuTS coincides with the coalgebraic notion of behavioral equivalence associated to the functor on Set given by the type of the FuTS. For a series of concrete quantitative semantical models the notion of bisimulation as reported in the literature is proven to coincide with the notion of quantitative bisimulation obtained from the scheme. The comparison includes models with orthogonal behaviour, like interactive Markov chains, and with multiple levels of behavior, like Markov automata. As a consequence of the general result relating FuTS bisimulation and behavioral equivalence we obtain, in a systematic way, a coalgebraic underpinning of all quantitative bisimulations discussed.

cs.LO↗

arXiv2011

Proceedings Third International Workshop on Computational Models for Cell Processes

This volume contains the final versions of the papers presented at the 3rd International Workshop on Computational Models for Cell Processes (CompMod 2011). The workshop took place on September 10, 2011 at the University of Aachen, Germany, in conjunction with CONCUR 2011. The first edition of the workshop (2008) took place in Turku, Finland, in conjunction with Formal Methods 2008 and the second edition (2009) took place in Eindhoven, the Netherlands, as well in conjunction with Formal Methods 2009. The goal of the CompMod workshop series is to bring together researchers in Computer Science (especially in Formal Methods) and Mathematics (both discrete and continuous), interested in the opportunities and the challenges of Systems Biology.

cs.CE↗

arXiv2011

Towards reduction of Paradigm coordination models

The coordination modelling language Paradigm addresses collaboration between components in terms of dynamic constraints. Within a Paradigm model, component dynamics are consistently specified at a detailed and a global level of abstraction. To enable automated verification of Paradigm models, a translation of Paradigm into process algebra has been defined in previous work. In this paper we investigate, guided by a client-server example, reduction of Paradigm models based on a notion of global inertness. Representation of Paradigm models as process algebraic specifications helps to establish a property-preserving equivalence relation between the original and the reduced Paradigm model. Experiments indicate that in this way larger Paradigm models can be analyzed.

cs.LO↗

arXiv2011

Decoupled execution of synchronous coordination models via behavioural automata

Synchronous coordination systems allow the exchange of data by logically indivisible actions involving all coordinated entities. This paper introduces behavioural automata, a logically synchronous coordination model based on the Reo coordination language, which focuses on relevant aspects for the concurrent evolution of these systems. We show how our automata model encodes the Reo and Linda coordination models and how it introduces an explicit predicate that captures the concurrent evolution, distinguishing local from global actions, and lifting the need of most synchronous models to involve all entities at each coordination step, paving the way to more scalable implementations.

cs.FL↗

arXiv2009

Proceedings Second International Workshop on Computational Models for Cell Processes

The second international workshop on Computational Models for Cell Processes (ComProc 2009) took place on November 3, 2009 at the Eindhoven University of Technology, in conjunction with Formal Methods 2009. The workshop was jointly organized with the EC-MOAN project. This volume contains the final versions of all contributions accepted for presentation at the workshop.

cs.CE↗