Model-checking ecological state-transition graphs

Model-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as a state-transition graph satisfies a dynamical property written as a temporal logic formula. The dynamics of ecosystems have been drawn as state-transition graphs for more than a century, from state-and-transition models to assembly graphs. Thus, model-checking can provide insights into both empirical data and theoretical models, as long as they sum up into state-transition graphs. While model-checking proved to be a valuable tool in systems biology, it remains largely underused in ecology. Here we promote the adoption of the model-checking toolbox in ecology through its application to an illustrative example. We assessed the dynamics of a vegetation model inspired from state-and-transition models by model-checking Computation Tree Logic formulas built from a proposed catalogue of patterns. Model-checking encompasses a wide range of concepts and available software, mentioned in discussion, thus its implementation can be fitted to the specific features of the described system. In addition to the automated analysis of ecological state-transition graphs, we believe that defining ecological concepts with temporal logics could help clarifying and comparing them.

Multiscale representations of community structures in attractor neural networks

Our cognition relies on the ability of the brain to segment hierarchically structured events on multiple scales. Recent evidence suggests that the brain performs this event segmentation based on the structure of state-transition graphs behind sequential experiences. However, the underlying circuit mechanisms are poorly understood. In this paper we propose an extended attractor network model for graph-based hierarchical computation which we call the Laplacian associative memory. This model generates multiscale representations for communities (clusters) of associative links between memory items, and the scale is regulated by the heterogenous modulation of inhibitory circuits. We analytically and numerically show that these representations correspond to graph Laplacian eigenvectors, a popular method for graph segmentation and dimensionality reduction. Finally, we demonstrate that our model exhibits chunked sequential activity patterns resembling hippocampal theta sequences. Our model connects graph theory and attractor dynamics to provide a biologically plausible mechanism for abstraction in the brain.

Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

Computing Bottom SCCs Symbolically Using Transition Guided Reduction

Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamical systems. However, these graphs’ size is often entirely out of reach for algorithms using explicit state-space exploration, necessitating alternative approaches such as the symbolic one.Symbolic methods for BSCC detection often show impressive performance, but can sometimes take a long time to converge in large graphs. In this paper, we provide a symbolic state-space reduction method for labelled transition systems, called interleaved transition guided reduction (ITGR), which aims to alleviate current problems of BSCC detection by efficiently identifying large portions of the non-BSCC states.We evaluate the suggested heuristic on an extensive collection of 125 real-world biologically motivated systems. We show that ITGR can easily handle all these models while being either the only method to finish, or providing at least an order-of-magnitude speedup over existing state-of-the-art methods. We then use a set of synthetic benchmarks to demonstrate that the technique also consistently scales to graphs with more than $$2^{1000}$$ 2 1000 vertices, which was not possible using previous methods.

Associative memory networks for graph-based abstraction

Our cognition relies on the ability of the brain to segment hierarchically structured events on multiple scales. Recent evidence suggests that the brain performs this event segmentation based on the structure of state-transition graphs behind sequential experiences. However, the underlying circuit mechanisms are only poorly understood. In this paper, we propose an extended attractor network model for the graph-based hierarchical computation, called as Laplacian associative memory. This model generates multiscale representations for communities (clusters) of associative links between memory items, and the scale is regulated by heterogenous modulation of inhibitory circuits. We analytically and numerically show that these representations correspond to graph Laplacian eigenvectors, a popular method for graph segmentation and dimensionality reduction. Finally, we demonstrate that our model with asymmetricity exhibits chunking resembling to hippocampal theta sequences. Our model connects graph theory and the attractor dynamics to provide a biologically plausible mechanism for abstraction in the brain.

Companions and an Essential Motion of a Reaction System

For a family of sets we consider elements that belong to the same sets within the family as companions. The global dynamics of a reactions system (as introduced by Ehrenfeucht and Rozenberg) can be represented by a directed graph, called a transition graph, which is uniquely determined by a one-out subgraph, called the 0-context graph. We consider the companion classes of the outsets of a transition graph and introduce a directed multigraph, called an essential motion, whose vertices are such companion classes. We show that all one-out graphs obtained from an essential motion represent 0-context graphs of reactions systems with isomorphic transition graphs. All such 0-context graphs are obtained from one another by swapping the outgoing edges of companion vertices.