The synthesis problem for nets consists in deciding whether a given graph is isomorphic to
the marking graph of some net and then constructing it. This problem has been solved in the …

Temporal logic model checking is a useful method for verifying properties of finite-state
concurrent systems. However, due to the state explosion problem modular methods like …

We compare propositional temporal logics by comparing the equivalences that they induce
on models. Linear time, branching time and partial order temporal logics are considered …

We introduce an operational model of concurrent systems, called automata with concurrency
relations. These are labeled transition systems in which the event set is endowed with a …

We introduce an operational model of concurrent systems, called concurrent automata.
These are labeled transition systems A in which the event set is endowed with a collection of …

Abstract Automata with concurrency relations are labelled transition systems with a
collection of state-dependent binary independence relations for the actions. We show how to …

Given suitable categories T, C and functor F: T→ C, if X, Y are objects of T, then we define an
(X, Y)-relation in C to be a triple\left (R,\raise0. 3em \scriptscriptstyle- r, ̄ r\right), where R is …

We define families of posets, ordered by prefixes, as the counterpart of the usual families of
configurations ordered by subsets. On these objects we define two types of morphism: event …

We provide a counterexample to a conjecture by Thiagarajan (1996, 2002) that regular
event structures correspond to event structures obtained as unfoldings of finite 1-safe Petri …

In this paper, we investigate how rewriting systems and especially graph grammars as
operational models of parallel and distributed systems can be related to event structures as …