Searcharxiv⌕ Search

arXiv subjects

Jean Krivine

Publications and source records attributed to Jean Krivine.

12 recordsLinked to original sources
arXiv2026

Reversible computations are computations

Causality serves as an abstract notion of time for concurrent systems. A computation is causal, or simply valid, if each observation of a computation event is preceded by the observation of its causes. The present work establishes that this simple requirement is equally relevant when the occurrence of an event is invertible. We propose a conservative extension of causal models for concurrency that accommodates reversible computations. We first model reversible computations using a symmetric residuation operation in the general model of configuration structures. We show that stable configuration structures, which correspond to prime algebraic domains, remain stable under the action of this residuation. We then derive a semantics of reversible computations for prime event structures, which is shown to coincide with a switch operation that dualizes conflict and causality.

cs.LO↗
arXiv2023

Fundamentals of Compositional Rewriting Theory

A foundational theory of compositional categorical rewriting theory is presented, based on a collection of fibration-like properties that collectively induce and intrinsically structure the large collection of lemmata used in the proofs of theorems such as concurrency and associativity. The resulting highly generic proofs of these theorems are given. It is noteworthy that the proof of the concurrency theorem takes only a few lines and, while that of associativity remains somewhat longer, it would be unreadably long if written directly in terms of the basic lemmata. In essence, our framework improves the readability and ease of comprehension of these proofs by exposing latent modularity. A curated list of known instances of our framework is used to conclude the paper with a detailed discussion of the conditions under which the Double Pushout and Sesqui-Pushout semantics of graph transformation are compositional.

cs.LO↗
arXiv2021

Rewriting Theory for the Life Sciences: A Unifying Theory of CTMC Semantics (Long version)

The Kappa biochemistry and the MØD organic chemistry frameworks are amongst the most intensely developed applications of rewriting-based methods in the life sciences to date. A typical feature of these types of rewriting theories is the necessity to implement certain structural constraints on the objects to be rewritten (a protein is empirically found to have a certain signature of sites, a carbon atom can form at most four bonds, ...). In this paper, we contribute a number of original developments that permit to implement a universal theory of continuous-time Markov chains (CTMCs) for stochastic rewriting systems. Our core mathematical concepts are a novel rule algebra construction for the relevant setting of rewriting rules with conditions, both in Double- and in Sesqui-Pushout semantics, augmented by a suitable stochastic mechanics formalism extension that permits to derive dynamical evolution equations for pattern-counting statistics. A second main contribution of our paper is a novel framework of restricted rewriting theories, which comprises a rule-algebra calculus under the restriction to so-called constraint-preserving completions of application conditions (for rules considered to act only upon objects of the underlying category satisfying a globally fixed set of structural constraints). This novel framework in turn renders a faithful encoding of bio- and organo-chemical rewriting in the sense of Kappa and MØD possible, which allows us to derive a rewriting-based formulation of reaction systems including a full-fledged CTMC semantics as instances of our universal CTMC framework. While offering an interesting new perspective and conceptual simplification of this semantics in the setting of Kappa, both the formal encoding and the CTMC semantics of organo-chemical reaction systems as motivated by the MØD framework are the first such results of their kind.

cs.LO↗
arXiv2021

Concurrency Theorems for Non-linear Rewriting Theories

Sesqui-pushout (SqPO) rewriting along non-linear rules and for monic matches is well-known to permit the modeling of fusing and cloning of vertices and edges, yet to date, no construction of a suitable concurrency theorem was available. The lack of such a theorem, in turn, rendered compositional reasoning for such rewriting systems largely infeasible. We develop in this paper a suitable concurrency theorem for non-linear SqPO-rewriting in categories that are quasi-topoi (subsuming the example of adhesive categories) and with matches required to be regular monomorphisms of the given category. Our construction reveals an interesting "backpropagation effect" in computing rule compositions. We derive in addition a concurrency theorem for non-linear double pushout (DPO) rewriting in rm-adhesive categories. Our results open non-linear SqPO and DPO semantics to the rich static analysis techniques available from concurrency, rule algebra and tracelet theory.

cs.LO↗
arXiv2021

Compositionality of Rewriting Rules with Conditions

We extend the notion of compositional associative rewriting as recently studied in the rule algebra framework literature to the setting of rewriting rules with conditions. Our methodology is category-theoretical in nature, where the definition of rule composition operations encodes the non-deterministic sequential concurrent application of rules in Double-Pushout (DPO) and Sesqui-Pushout (SqPO) rewriting with application conditions based upon $\mathcal{M}$-adhesive categories. We uncover an intricate interplay between the category-theoretical concepts of conditions on rules and morphisms, the compositionality and compatibility of certain shift and transport constructions for conditions, and thirdly the property of associativity of the composition of rules.

cs.LO↗
arXiv2020

Rewriting Theory for the Life Sciences: A Unifying Theory of CTMC Semantics

The Kappa biochemistry and the MØD organo-chemistry frameworks are amongst the most intensely developed applications of rewriting theoretical methods in the life sciences to date. A typical feature of these types of rewriting theories is the necessity to implement certain structural constraints on the objects to be rewritten (a protein is empirically found to have a certain signature of sites, a carbon atom can form at most four bonds, ...). In this paper, we contribute to the theoretical foundations of these types of rewriting theory a number of conceptual and technical developments that permit to implement a universal theory of continuous-time Markov chains (CTMCs) for stochastic rewriting systems. Our core mathematical concepts are a novel rule algebra construction for the relevant setting of rewriting rules with conditions, both in Double- and in Sesqui-Pushout semantics, augmented by a suitable stochastic mechanics formalism extension that permits to derive dynamical evolution equations for pattern-counting statistics.

cs.LO↗
arXiv2019

A Tractable Logic for Molecular Biology

We introduce a logic for knowledge representation and reasoning on protein-protein interactions. Modulo a theory, formulas describe protein structures and dynamic changes. They can be composed in order to add or remove static and dynamic observations. A second-order circumscription operator then enables nonmonotonic reasoning on the changes implied by a formula. We introduce deduction rules that produce formulas which are, up to equivalence, in a first-order fragment with decidable satisfiability and validity. Importantly, the rules can produce circumscribed formulas.

cs.LO↗
arXiv2019

Interactions between Causal Structures in Graph Rewriting Systems

Graph rewrite formalisms are a powerful approach to modeling complex molecular systems. They capture the intrinsic concurrency of molecular interactions, thereby enabling a formal notion of mechanism (a partially ordered set of events) that explains how a system achieves a particular outcome given a set of rewrite rules. It is then useful to verify whether the mechanisms that emerge from a given model comply with empirical observations about their mutual interference. In this work, our objective is to determine whether a specific event in the mechanism for achieving X prevents or promotes the occurrence of a specific event in the mechanism for achieving Y. Such checks might also be used to hypothesize rules that would bring model mechanisms in compliance with observations. We define a rigorous framework for defining the concept of interference (positive or negative) between mechanisms induced by a system of graph-rewrite rules and for establishing whether an asserted influence can be realized given two mechanisms as an input.

cs.LO↗
arXiv2017

Dynamic Influence Networks for Rule-based Models

We introduce the Dynamic Influence Network (DIN), a novel visual analytics technique for representing and analyzing rule-based models of protein-protein interaction networks. Rule-based modeling has proved instrumental in developing biological models that are concise, comprehensible, easily extensible, and that mitigate the combinatorial complexity of multi-state and multi-component biological molecules. Our technique visualizes the dynamics of these rules as they evolve over time. Using the data produced by KaSim, an open source stochastic simulator of rule-based models written in the Kappa language, DINs provide a node-link diagram that represents the influence that each rule has on the other rules. That is, rather than representing individual biological components or types, we instead represent the rules about them (as nodes) and the current influence of these rules (as links). Using our interactive DIN-Viz software tool, researchers are able to query this dynamic network to find meaningful patterns about biological processes, and to identify salient aspects of complex rule-based models. To evaluate the effectiveness of our approach, we investigate a simulation of a circadian clock model that illustrates the oscillatory behavior of the KaiC protein phosphorylation cycle.

cs.GR↗
arXiv2012

Proceedings 7th International Workshop on Developments of Computational Methods

This volume contains the proceedings of the 7th International Workshop on Developments in Computational Models (DCM 2011) which was held on Sunday July 3, 2011, in Zurich, Switzerland, as a satelite workshop of ICALP 2011. Recently several new models of computation have emerged, for instance for bio-computing and quantum-computing, and in addition traditional models of computation have been adapted to accommodate new demands or capabilities of computer systems. The aim of DCM is to bring together researchers who are currently developing new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area.

cs.CE↗
arXiv2006

A verification algorithm for Declarative Concurrent Programming

A verification method for distributed systems based on decoupling forward and backward behaviour is proposed. This method uses an event structure based algorithm that, given a CCS process, constructs its causal compression relative to a choice of observable actions. Verifying the original process equipped with distributed backtracking on non-observable actions, is equivalent to verifying its relative compression which in general is much smaller. We call this method Declarative Concurrent Programming (DCP). DCP technique compares well with direct bisimulation based methods. Benchmarks for the classic dining philosophers problem show that causal compression is rather efficient both time- and space-wise. State of the art verification tools can successfully handle more than 15 agents, whereas they can handle no more than 5 following the traditional direct method; an altogether spectacular improvement, since in this example the specification size is exponential in the number of agents.

cs.DC↗