key: cord-0060831-inej3dw6
authors: Dubut, Jérémy
title: Bisimilarity of Diagrams
date: 2020-04-01
journal: Relational and Algebraic Methods in Computer Science
DOI: 10.1007/978-3-030-43520-2_5
sha: af75b7d6985a698d3f405ff75b6d79367a39d185
doc_id: 60831
cord_uid: inej3dw6

In this paper, we investigate diagrams, namely functors from any small category to a fixed category, and more particularly, their bisimilarity. Initially defined using the theory of open maps of Joyal et al., we prove two characterisations of this bisimilarity: it is equivalent to the existence of a bisimulation-like relation and has a logical characterisation à la Hennessy and Milner. We then prove that we capture both path bisimilarity and strong path bisimilarity of any small open maps situation. We then look at the particular case of finitary diagrams with values in real or rational vector spaces. We prove that checking bisimilarity and satisfiability of a positive formula by a diagram are both decidable by reducing to a problem of existence of invertible matrices with linear conditions, which in turn reduces to the existential theory of the reals.

Diagrams in a category, namely functors from any small category to this specified category, are essential objects in category theory. Numerous basic constructions in category theory can be seen as a limit or colimit of a suitable diagram. However, their usefulness is not limited to those.

In the context of directed algebraic topology (see [7] for a textbook), Dubut et al. used diagrams with values in a category of modules to encode local geometric properties of a directed space and their evolution [5] . The domains of those diagrams are given by directed paths of the space and their extensions, while the diagrams themselves map such a path to some homology modules describing the default of directed homotopy of the space. It was then observed that a suitable notion of bisimilarity of diagrams, using the general theory of open maps from [10] was the right notion to compare such defaults of dihomotopy.

In the first part of this paper, we propose to look at the general theory of bisimilarity of diagrams, extending it to any category of observations. After describing the original definition using open morphisms (Sect. 2.2), we describe two equivalent characterisations. First (Sect. 2.3), it is equivalent to the existence of a relation, similar to history preserving bisimulations of event structures from [14] . This result generalises a result from [5] . Secondly (Sect. 3), it has a logical characterisation, similar to a Hennessy-Milner theorem: two diagrams are bisimilar if and only if they both satisfy the same formulae of a path logic. We finally prove in Sect. 4 that we capture path and strong path bisimilarities of any open map situation [10] as the bisimilarity of a suitable notion of diagrams.

In a second part, we consider two decision problems for a class of diagrams with values in real or rational vector spaces, used in [5] for describing defaults of dihomotopy of geometric models of truly concurrent systems (See Sect. 5). For those diagrams, we prove in Sect. 7 that bisimilarity and the satisfaction of a positive formula are both decidable by reduction to a problem of invertible matrices, itself reduced to the existential theory of the reals (Sect. 6).

Existing Work: This theory of bisimilarity of diagrams is intimately related to categorical theories of bisimulations. If the relation with open maps is developed in Sects. 2.2 and 4, its relation with coalgebra is less clear. Relations between open maps and coalgebra are investigated in [11, 19] , however those cannot be applied in general to a category of diagrams. The main problem is that diagrams are not naturally coalgebras in general, and so there is no clear relationship between open maps as described in Sect. 2.2, and coalgebra homomorphisms (also called coverings of processes in [18] ). Another important related line of work is the theory of bisimilarity of presheaves [4] , which considers similar objects (presheaves are particular cases of diagrams), but from a very different point of view.

Diagrams with values in a fixed category A are functors F : C −→ A from any small category to A. If A is thought as a category of "observations" and C as the category of executions of a system, a diagram encodes the trace of observations along every execution (typically, a label), and its actions on morphisms of C encodes how these observations change when the system evolves.

In this section, we describe the original form of the bisimilarity from [5] , defined as the existence of a span of particular morphisms of diagrams having some lifting properties. We then develop an equivalent characterization using relations, similar to bisimulations of event structures as introduced in [14] .

The original definition of bisimilarity of diagrams was designed using particular morphisms of diagrams. Such a morphism, say from the diagram F :

. We denote this category by Diag(A). Example 1. Throughout the next two sections, we will develop a particular example of diagrams in which transition systems can be encoded. This example will allow us to relate constructions in diagrams to classical constructions in concurrency theory. From now, we fix a set L called the alphabet. Such a set induces a poset (which can be seen as a category) A L whose elements are the finite words on L and whose order is the prefix order. A transition system T on L produces a diagram F T : C T −→ A L as follows. The category C T is formed by considering as objects the runs of T , that is, sequences i

an − − → q n of transitions of T where i is the initial state, and by ordering them by prefix. F T then maps a run to its sequence of labels. This construction extends to a functor Π from the category TS(L) of transition systems on L to the category Diag(A L ). Conversely, a diagram F : C −→ A L produces a transition system T as follows. First, such a diagram can be identified with a diagram with values in TS(L) by identifying a word a 1 .a 2 . . . . .a n with the finite linear transition system 0

T is then obtained by forming the colimit of this diagram in TS(L). This extends to a functor Γ from Diag(A L ) to TS(L). Note that Γ • Π is the unfolding of transition systems and that Γ is the left adjoint of Π.

The reason why we need natural isomorphisms in the definition of a morphism of diagram is not clear yet, as the only isomorphisms in the category A L are the identities. This will be illustrated in the case where A is a category of vector spaces. Intuitively, two isomorphic vector spaces represent the same kind of observations (in the case of directed algebraic topology, the same kind and number of holes), which we do not want to discriminate.

The original idea from [5] was to compare diagrams similarly to transition systems using the theory of [10] . Let us call branch a diagram from n to A for n ∈ N, where n is the poset (seen as a category) {1, . . . , n} with the usual ordering. An evolution of a diagram F : C −→ A is then a morphism from any branch to F . Much as transition systems and executions, a morphism of diagrams (Φ, σ) from F : C −→ A to G : D −→ A maps evolutions of F to evolutions of G: if (Ψ, τ ) is an evolution of F , i.e., a morphism from a branch to F , then (Φ, σ) • (Ψ, τ ) is an evolution of G. Then morphisms act as particular simulations of diagrams. The idea from [10] was to provide conditions on morphisms for them to act as particular bisimulations. The general idea is that a morphism induces a bisimulation if it lifts evolutions of G to evolutions of F . In the context of diagrams, this will be defined using extensions of branches. An extension of a branch B : n −→ A is a morphism of diagrams (Π, θ) from B : n −→ A to a branch B : n −→ A, with n ≥ n such that:

-for every i ≤ n, B(i) = B (i), -for every i ≤ j ≤ n, the morphism B (i ≤ j) of A is equal to B(i ≤ j), -for every i ≤ n, Π(i) = i, -for every i ≤ n, θ i = id B(i) . Those conditions mean that the restriction of B to n is B and that the morphism (Π, θ) is the inclusion of B in B (Fig. 1) .

Following [10] , we then say that a morphism (Φ, σ) from F :

is an extension of branches, there is an evolution of F (in dots) which makes the two triangles commute. This means that if we can extend an evolution of F , mapped on an evolution of G by (Φ, σ), as a longer evolution of G, then we can extend it as a longer evolution of F that is mapped to this longer evolution of G. This means in particular that F and G have exactly the same evolutions. As observed in [5] , the definition of an open map can be simplified as follows: 

In this section, we generalise a notion of bisimulation relations from [5] , which is equivalent to the existence of a span of open morphisms. This result is an equivalent of Theorem 3.1 in [18] in the context of open maps of diagrams.

A bisimulation R between two diagrams F :

Example 3. In the case of diagrams in A L , a bisimulation between diagrams Π(T ) and Π(S) is just a rephrasing for a path bisimulation in the sense of [10] between the transition systems T and S. In the particular case of transition systems, the existence of a path bisimulation is equivalent to the existence of a strong path bisimulation and is equivalent to the existence of a bisimulation. Consequently:

In this section, we focus on a logical characterization of bisimilarity of diagrams. The logic used, which we call diagrammatic path logic, is similar to the logic introduced in [9] for transition systems, or to path logics developed in [10] . A formula in this logic allows one to express that a diagram has some kind of evolutions or not.

The formulae used are generated by the following grammar: where Ob(A) is the class of objects of A and Mor(A) is its class of morphisms. Intuitively, the object formula [x]P means that the current object is isomorphic to x, and the morphism formula f P means that from the current object, one can fire a transition labelled by a morphism equivalent (in the sense of matrices, or conjugate in the language of group theory) to f . Observe that we have arbitrary conjunctions, in particular infinite and empty (we will denote the empty conjunction by ).

In the case of diagrams in A L , [w] means that the current run is labeled by the word w and w ≤ w means that the current run is labeled by w and that it can be extended to a run labeled by w . The idea is very similar to the Hennessy-Milner logic [9] and the forward path logic [10] . The next theorem proves that, for two transition systems, satisfying the same Hennessy-Milner formulae, forward path formulae or path formulae is the same as their diagrams satisfying the same diagrammatic formulae.

For a diagram F : C −→ A, an object c of C, and an isomorphism f of A of the form f : F (d) −→ x for some d and x, we define F, c |= S for an object formula S and F, f, d |= P for a morphism formula P by induction on S (resp. P ) as follows:

We say that a diagram F : C −→ A is logically simulated by another diagram G : D −→ A if for every object c of C, there exists an object d of D such that for all object formula S, F, c |= S iff G, d |= S. Two diagrams F and G are logically equivalent if F is logically simulated by G and vice-versa. 

In Sect. 2.2, we understood bisimilarity of diagrams using branches, as the existence of a span of open maps. In the context of [10] , it means that diagrams, together with their subcategory of branches is an open map situation. Concretely, an open map situation is a category M, called the category of systems (in our case Diag(A)), together with a subcategory P → M, said of paths (here the subcategory of branches). Another typical example is the category of transition systems TS(L) with its subcategory of finite linear systems.

In [10] , two notions of bisimulations between objects of M are described: the path bisimulations and the strong path bisimulations. However, for them to make sense, some conditions on the open map situation are required: P need to be small and P and M must have a common initial object, which we denote by I. For example, the open maps situation of transition systems satisfies those requirements, while the one of diagrams does not in general (smallness is the issue).

Concretely, a path bisimulation R between objects X and Y of M is a set of pairs of morphisms of the form (x : P −→ X, y : P −→ Y ) for some object P of P such that:

-Symmetrically, swapping the roles of X and Y .

Furthermore, we say that R is strong if it additionally satisfies that for every (x : P −→ X, y : P −→ Y ) in R, and for every morphism p : Q −→ P of P,

It has to be remarked that those bisimulations induce different notions of bisimilarity in general. Furthermore, they both are different to the existence of a span of open morphisms, although strong path bisimilarity coincide with this existence in many concrete cases [6] . In the case of transition systems and finite linear systems, those three notions coincide.

We propose now to characterise those two notions of bisimulations using diagrams, namely, we will now describe two functors Ex : M −→ Diag(P) and Ex : M −→ Diag(P) such that the existence of a path (resp. strong path) bisimulation between X and Y is equivalent to the fact that Ex(X) and Ex(Y ) (resp. Ex(X) and Ex(Y )) are bisimilar as diagrams.

First, Ex(X) is the functor from P ↓ X, the category of morphisms from any objects of P to X and commutative triangles, to the category P which maps any morphism x : P −→ X to P and every commutative triangles x • p = x to p. Given a category C, we denote by Zig(C) the category whose objects are those of C and whose morphisms are generated by those of C and those of C op . This naturally extends to an endofunctor Zig : Cat −→ Cat. We then define Ex = Zig(Ex) from Zig(Ex(X)) to Zig(P). Theorem 5. X and Y are strong path bisimilar if and only if Ex(X) and Ex(Y ) are bisimilar. Remark 1. This pattern of characterising a notion bisimilarity as bisimilarity of suitable diagrams whose domain is a category of "runs" and whose codomain is a category of "observations" is more general than for (strong) path bisimilarity of open maps situations, and can be pursued for Higher-Dimensional Automata [8, 13] for example.

In the first part of the paper, we focused on the general theory of bisimilarity of diagrams and its relationship with usual notions of bisimilarity of transition systems (and so of process algebra). In the second part of the paper, we would like to turn our attention to other kinds of diagrams that appeared in the theory of directed algebraic topology [5] . While diagrams in Sect. 4 were typically with values in a category of words, we will now consider diagrams with values in modules on a ring. More precisely, we will focus on the following two problems for such diagrams:

bisimilarity: given two diagrams, are they bisimilar? diagrammatic model-checking: given a diagram F , an object c of its domain and a state formula S, does F, c S hold?

The difficulty of those problems lies in the possibility to decide whether two modules are isomorphic, problem which does not appear in the context of process algebras and transition systems. Indeed, it is known that those problems are decidable in the category of transition systems (see [16] for a dynamic list of such (un)decidability results), while they would be undecidable for diagrams with values in groups and group morphisms because it is undecidable whether two groups are isomorphic. In this paper, we will focus on the category of finite dimensional real or rational vector spaces and matrices.

More precisely, we will stick to finitary diagrams and finitary positive formulae defined as follows. By a finitary diagram F , we mean the following data:

-a finite poset (C, ≤), the domain, -for every element c of C, a natural number F (c) (which stands for the real vector space R F (c) ), -for every pair c ≤ c of C, a matrix F (c ≤ c ) of size F (c) × F (c ), with coefficients in rational numbers, presented as the list of all its elements, such that:

denotes the matrix multiplication.

In short, a finitary diagram is a functor from a finite poset to the category of matrices with coefficients in rational numbers. One may argue that those assumptions are not reasonable, because they are not satisfied by the diagrams from Sect. 4 as soon as there is a loop. The reason is that when deciding this bisimilarity, there are two problems: finding out how to relate the executions and constructing the bisimulation, in particular, the isomorphism part. Loops make the first part difficult, because this relation is necessarily infinite in this case. In this paper, we want to focus on the second problem because: (1) reducing the problem of existence of a bisimulation to a problem of isomorphisms in a category is the main difference from existence of bisimulation for process algebra, (2) solving this question addresses the problem of comparing natural homologies of geometric models of true concurrency from [5] .

We call finitary formulae, the formulae generated by the following grammar:

Object where M is a matrix with coefficients in rational numbers. Here, [n]P stands for [R n ]P which makes finitary formulae diagrammatic formulae in real vector spaces. This time, since we only have finitely branching diagrams, we only consider finite conjunctions. We will more particularly consider positive formulae, i.e., formulae without any occurrences of the negation. For example, a formula of the form M 1 . . . M k means that there is a sequence of matrices N 1 , . . . , N k in the diagrams where N i is equivalent to M i , and those equivalences are natural (in the categorical meaning).

In this case, bisimilarity and model checking problems become a problem of existence of invertible matrices satisfying some linear conditions, as we will see in Sect. 7. In Sect. 6, we will start by proving that this problem of matrices can be encoded in the existential theory of the reals, which is known to be decidable.

In the present section, we focus on an existential theory of matrices. We first recall the case of the existential theory of the reals, which is known to be decidable. We then introduce the existential theory of invertible matrices in R and Q and we finally prove the decidability of their satisfiability problems.

Designing algorithms for finding solutions of equations is an old problem in mathematics. The famous Hilbert's tenth problem posed the problem for polynomial equations in integers, but the question can be asked for other rings.

Tarski in [17] solved this question for real numbers: the first-order logic of real closed fields is decidable, although the solution is of non-elementary complexity. Several improvements have been made: it was proved to be in EXPSPACE in [2] and that the existential theory of the reals is in PSPACE in [3] . On the contrary, Matiyasevich's negative answer of the tenth problem [12] , means that the existential theory of the integers is undecidable. In particular, since it is possible to express that a rational number is an integer (using possibly universal quantifiers), the full first-order logic of the rationals is undecidable. However, it is still an open question whether its existential fragment is decidable or not.

In this section, we will consider a logic of matrices that will be expressible in the existential theory of the reals. It will be the main ingredient to decide some problems in diagrams with values in vector spaces. Namely, we consider formulae of the form:

where:

-n i ≥ 0, is a natural number, -X i is a variable ranging over invertible matrices of dimension n i , -P j is a predicate of the form A.X i = X k .B for some i, k and matrices A, B with coefficients in rational numbers, A and B are of size n k × n i , and . denotes the matrix multiplication. We call it the existential theory of invertible matrices.

We will consider the following decision problem: given such a formula, is it satisfiable, that is, are there matrices M 1 , ..., M k , with M i of size n i × n i , invertible such that for every j, P j (M 1 , ..., M k ) is true?

We may ask this question for matrices M i in coefficients in real or rational numbers. We will prove that both problems actually coincide and are decidable in PSPACE.

We stick here to the case of real numbers. We prove that we have a reduction to the existential theory of the reals. Given a formula

we will construct a formula Ψ in the existential theory of the reals which is satisfiable if and only if Φ is.

First, for every variable X i , check if it appears in some P j . If not, forget it. Indeed, if it does not appear in any predicate, then we can just choose the identity. Then, for every other quantifier ∃ ni X i , we fix 2.n 2 i fresh first-order variables x r,s i and y r,s i for r, s ∈ {1, ..., n i }. Let X i be the matrix of size n i × n i whose coefficients are x r,s i , and Y i whose coefficients are y r,s i . Developing A.X i = X j .B leads to n j n i linear equations on the variables x r,s i and x r,s j . So every predicate P j induces a set L j of linear equations. It remains to express that X i is invertible in the first-order logic. The idea is to express that Y i is its inverse. Developing X i .Y i = Id and Y i .X i = Id, leads to 2.n 2 i polynomial equations on the variables x r,s i and y r,s i . Let S i be the set of these equations. We denote by Ψ the formula:

Ψ is of polynomial size on the size of Φ: indeed, the only problem might be that we fix 2n 2 i variables while n i is of size log(n i ), which may say that we fix an exponential number of variables. The point is that if we fixed those 2n 2 i variables, then it means that X i appears in some P j , and that the matrices appearing in P j have a polynomial size in n i . Consequently, we fix only a polynomial number of variables.

As we have seen previously, first-order theories of rationals are in general harder than those in reals. But there are some algebraic problems that are known to coincide when considering real and rational numbers. Given a linear system with coefficients in rational numbers, Gaussian elimination works independently of the coefficient field. Consequently, the real subspace F R of solutions of this system has the same dimension as the rational subspace F Q of solutions of the system. Actually, F R ∩ Q n = F Q and they have a common basis whose vectors are with coefficients in rational numbers. Similarly, the problem of equivalence of matrices coincides in the fields of real and rational numbers. Given two matrices A and B with coefficients in rational numbers, A and B are equivalent if there are two invertible matrices X and Y such that A.X = Y.B. This problem is also solvable using Gaussian elimination by computing the rank of A and B, which is independent of the coefficient field. Our problem is a generalization of the equivalence problem and it is not surprising that the same kind of results hold:

Finally, we prove two decidability results for bisimilarity of diagrams and diagrammatic logic using the existential theory of invertible matrices. In this section, we consider diagrams with values in real vector spaces (or rational, but as we have seen in the previous section, both theories will coincide). We prove the decidability of the following two problems:

bisimilarity: given two finitary diagrams, are they bisimilar? diagram model-checking: given a finitary diagram F , an object c of its domain and a positive finitary state formula S, does F, c S hold?

We start with the bisimilarity problem. Assume given two finitary diagrams Create a fresh variable X and add the pair (X, n) to var; 7:

Add (c, X, d) to R and do not mark it; 8:

while there is a non-marked element in R do 9:

Pick a non-marked element (c, X, d) ∈ R, with F (c) = G(d) = n; 10:

Mark (c, X, d); 11:

Non-deterministically choose a relation

such that for every c > c, there is d d with (c , d ) in Q, and symmetrically; 12: where M is a matrix with coefficients in real (or rational) numbers satisfying the properties of a bisimulation from Sect. 2. The only exception is that we will not guess explicitly the matrices M , but a formula in the existential theory of invertible matrices that encodes the fact that there exist some matrices M such that the bisimulation constructed satisfies those properties.

Consider the Algorithm 1 written in pseudo-code. It maintains the bisimulation R and two sets var, encoding the variables of the formula we are constructing and lin, encoding its predicates.

The algorithm always terminates. First, the innermost while loop terminates since after every loop an element (c, X, d) is marked and only elements of the form (c , X , d ) with either c < c and d d or c ≤ c and d ≺ d are added. The outer loop terminates since after every loop at least one element of S is removed.

Assume that there is an execution of the algorithm that answers Yes. Let R and Φ constructed during this execution. Since the algorithm answers Yes, the formula Φ is satisfiable, that is, for every (X, n) ∈ var, there is an invertible matrix M X of size n × n such that for every equation

Then by construction of R and Φ, R is a bisimulation between F and G.

Assume that there is a bisimulation R between F and G. We show that there are non-deterministic choices that lead to the answer Yes. The idea is to ensure that every (c, X, d) that belongs to R at some point corresponds to an element (c, f, d) of R . To ensure this, we must: 

. Such a Q always exists since R is a bisimulation.

With this, the algorithm does not FAIL and the formula Φ is valid: the assignment that map X to the corresponding f satisfies Φ. Consequently, the algorithm answers Yes. Finally, this algorithm non-deterministically construct in exponential space a formula of exponential size in the size of the data. By Theorem 5, this algorithm is in NEXPSPACE. Consequently, by Savitch's theorem [15] , since NEXPSPACE = EXPSPACE: 1) ; (X 2 , 2); (X 3 , 1); (X 4 , 1); (X 5 , 1)],

At the end, the algorithm produces var = [(X 1 , 1); (X 2 , 2); (X 3 , 1); (X 4 , 1); (X 5 , 1); (X 6 , 2); (X 7 , 1); (X 8 , 1)]

and their linear equations:

The induced problem of invertible matrices is satisfiable, which means that both diagrams are bisimilar. 

Starting with a finitary diagram F , an element c of its domain, and a positive finitary object formula S, we inductively construct two lists, initially empty, as previously:

-var of pairs (X, n) where X is a variable and n an integer. This will stand for ∃ n X. The formula S is of the form [n]P . We first check if n = F (c). If it is not the case then we fail. Otherwise, let X be a fresh variable. Add the pair (X, n) to var. Continue with F , c, X, and P . Now, assume that we consider the following data: a finitary diagram F , an element of its domain c, an X with (X, n) in var for some integer n and a positive finitary morphism formula P . Several cases: -if P =?S , continue with F , c and S , -if P = , stop, -if P = P 1 ∧P 2 , first continue with F , c, X and P 1 . When this part terminates, continue with F , c, X and P 2 , -if P = M P , with M of size n 1 × n 2 . If n 1 = F (c), then we fail. Otherwise, non-deterministically choose an element c ≥ c, with F (c ) = n 2 . If such a c does not exist, then we fail. Then, create a fresh variable X , add (X , n 2 ) to var and M.X = X .F (c ≤ c ) to lin. Finally, continue with F , c , X and P .

If the algorithm does not fail, construct a formula Φ from var and lin as previously and check if it is satisfiable using the existential theory of invertible matrices. The formula Φ is non-deterministically constructed in polynomial time and so is of polynomial size. So, this algorithm is in NPSPACE and again, by Savitch's theorem [15] , since NPSPACE = PSPACE: It is not hard to check that F, 0 φ, and so that G, a φ (you can unroll the algorithm, the identities will give a solution of the problem of matrices). Let H be the following diagram: We will show that H, 0 φ, and that H is not bisimilar to F and G. Let us unroll the algorithm on H, 0 and φ. We are in the first case, and we create a fresh variable X 1 and var := [(X 1 , 1)]. We then continue the algorithm with H, 0, X 1 and 1 0 1 1

. We are then in the last case, and we can only choose 1 without failing. So, var = [(X 1 , 1); (X 2 , 2)] and lin = [ 1 0 .X 1 = X 2 . 1 0 ]. We continue with H, 1, X 2 and 1 1

. We still are in the last case and we can only choose 2 without failing. So, var = [(X 1 , 1); (X 2 , 2); (X 3 , 1)] and lin = [ 1 0 .X 1 = X 2 . 1 0 ; 1 1 .X 2 = X 3 . 0 1 ]. Let us prove that we cannot solve this problem of invertible matrices. If we could, we would have that:

which is impossible since X 1 must be invertible.

As a future work, we would like to investigate the case of diagrams with values in Z-modules (that is, Abelian groups), i.e., diagrams with values in matrices whose coefficients are integers, for which the existential theory is undecidable, but for which we can still decide some problems of matrices. Another interesting direction is the relation between our algorithm of Sect. 7 to find a bisimulation and the final chain algorithm [1] , which we let for a future work.

A coalgebraic perspective on minimization and determinization

The complexity of elementary algebra and geometry

Some algebraic and geometric computations in PSPACE

Presheaf models for the π-calculus

Natural homology. In: Halldórsson

Bisimulations and unfolding in Paccessible categorical models

Directed Algebraic Topology and Concurrency

On the expresiveness of higher dimensional automata. Electron

On observing nondeterminism and concurrency

Bisimulation from open maps

Coalgebra morphisms subsume open maps

Hilbert's 10th Problem

Modeling concurrency with geometry

Behavior structures and nets

Relationships between nondeterministic and deterministic tape complexities

Roadmap of infinite results

A Decision Method for Elementary Algebra and Geometry

A relational algebraic theory of bisimulations

Path category for free