arXiv subjects
Publications and source records attributed to Krzysztof Ziemiański.
Using the formalism of presheaf automata, we introduce new classes of automata for modelling concurrency that extend higher-dimensional automata and symmetric higher-dimensional automata. We study their languages and characterise these languages in terms of posetal cospans.
Higher-Dimensional Automata (HDAs) provide a geometric model of true concurrency. While hereditary history-preserving (hhp) bisimilarity is the finest behavioural equivalence in van Glabbeek's spectrum, no modal logic has previously characterised it on HDAs. We introduce several new intermediate equivalences that sit strictly between ST- and hhp-bisimilarity. We show how separating similarity and subsumption of paths leads to a clean formulation of these equivalences, and we present a modal logic that characterises hhp-bisimilarity. Natural fragments characterise ST-bisimilarity and the intermediate notions.
Higher-dimensional automata (HDA) are a model of concurrency that models simultaneous execution of events using higher dimensional cells. HDA recognize languages of pomsets, a generalization of finite words whose letters are partially ordered. We prove a new algebraic characterization of HDA languages: a language of pomsets is regular if and only if it is the inverse image of a functor from the category of pomsets into a finite category. Furthermore, the language is definable in first-order logic exactly when it is recognized by an aperiodic category, generalizing the McNaughton-Papert theorem to HDA languages. We also investigate a notion of counter-free HDA, and show that if a language is accepted by a counter-free HDA, it must be definable in first-order logic. The converse, however, is still open.
The theory of higher-dimensional automata (HDAs) has seen rapid progress in recent years, and first applications, notably to Petri net analysis, are starting to show. It has, however, emerged that HDAs themselves often are too strict a formalism to use and reason about. In order to solve specific problems, weaker variants of HDAs have been introduced, such as HDAs with interfaces, partial HDAs, ST-automata or even relational HDAs. In this paper we collect definitions of these and a few other variants into a coherent whole and explore their properties and translations between them. We show that with regard to languages, the spectrum of variants collapses into two classes, languages closed under subsumption and those that are not. We also show that partial HDAs admit a Kleene theorem and that, contrary to HDAs, they are determinizable.
We introduce presheaf automata as a generalisation of different variants of higher-dimensional automata and other automata-like formalisms, including Petri nets and vector addition systems. We develop the foundations of a language theory for them based on notions of paths and track objects. We also define open maps for presheaf automata, extending the standard notions of simulation and bisimulation for transition systems. Apart from these conceptual contributions, we show that certain finite-type presheaf automata subsume all Petri nets, generalising a previous result by van Glabbeek, which applies to higher-dimensional automata and safe Petri nets. We also present a class of presheaf automata for which there is no Kleene theorem with respect to the notions of rational and regular languages introduced.
In this paper we explore languages of higher-dimensional automata (HDAs) from an algebraic and logical point of view. Such languages are sets of finite width-bounded interval pomsets with interfaces (ipomsets) closed under order extension. We show that ipomsets can be represented as equivalence classes of words over a particular alphabet, called step sequences. We introduce an automaton model that recognize such languages. Doing so allows us to lift the classical Büchi-Elgot-Trakhtenbrot Theorem to languages of HDAs: we prove that a set of interval ipomsets is the language of an HDA if and only if it is simultaneously MSO-definable, of bounded width, and closed under order refinement.
We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.
Higher-dimensional automata (HDAs) are models of non-interleaving concurrency for analyzing concurrent systems. There is a rich literature that deals with bisimulations for concurrent systems, and some of them have been extended to HDAs. However, no logical characterizations of these relations are currently available for HDAs. In this work, we address this gap by introducing Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and show that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation. We also define a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel, and establish the relationship between these bisimulations (and also their "strong" variants, which take restrictions into account). In our work, we rely on the new categorical definition of HDAs as presheaves over concurrency lists and on track objects.
We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular if and only if it has finite prefix quotient. HDAs extend standard automata with additional structure, making it possible to distinguish between interleavings and concurrency. We also introduce deterministic HDAs and show that not all HDAs are determinizable, that is, there exist regular languages that cannot be recognised by a deterministic HDA. Using our theorem, we develop an internal characterisation of deterministic languages. Lastly, we develop analogues of the Myhill-Nerode construction and of determinacy for HDAs with interfaces.
We report some further developments regarding the language theory of higher-dimensional automata (HDAs). Regular languages of HDAs are sets of finite interval partially ordered multisets (pomsets) with interfaces. We show a pumping lemma which allows us to expose a class of non-regular languages. Concerning decision and closure properties, we show that inclusion of regular languages is decidable (hence is emptiness), and that intersections of regular languages are again regular. On the other hand, complements of regular languages are not always regular. We introduce a width-bounded complement and show that width-bounded complements of regular languages are again regular. We also study determinism and ambiguity. We show that it is decidable whether a regular language is accepted by a deterministic HDA and that there exists regular languages with unbounded ambiguity. Finally, we characterize one-letter deterministic languages in terms of utlimately periodic functions.
Interval-order partially ordered multisets with interfaces (ipomsets) have shown to be a versatile model for executions of concurrent systems in which both precedence and concurrency need to be taken into account. In this paper, we develop a presentation of ipomsets as generated by a graph of certain discrete ipomsets (starters and terminators) under the relation which composes subsequent starters and subsequent terminators. Using this presentation, we show that also subsumptions are generated by elementary relations. We develop a similar correspondence on the automata side, relating higher-dimensional automata, which generate ipomsets, and ST-automata, which generate step sequences, and their respective languages.
We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternatively, taking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of a poset. We show that iposets under gluing composition form a category, which generalises the monoid of posets under serial composition up to isomorphism. They form a 2-category when a subsumption order and a lax tensor in the form of a non-commutative parallel composition are added, which generalises the interchange monoids used for modelling series-parallel posets. We also study the gluing-parallel hierarchy of iposets, which generalises the standard series-parallel one. The class of gluing-parallel iposets contains that of series-parallel posets and the class of interval orders, which are well studied in concurrency theory, too. We also show that it is strictly contained in the class of all iposets by identifying several forbidden substructures.
We generate and count isomorphism classes of gluing-parallel posets with interfaces (iposets) on up to eight points, and on up to ten points with interfaces removed. In order to do so, we introduce a new class of iposets with full interfaces and show that considering these is sufficient. We also describe the software (written in Julia) that we have used for our exploration and define a new incomplete isomorphism invariant which may be computed in polynomial time yet identifies only very few pairs of non-isomorphic iposets.
We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.
We show how modal quantales arise as convolution algebras of functions from lr-multisemigroups that is, multisemigroups with a source map l and a target map r, into modal quantales which can be seen as weight or value algebras. In the tradition of boolean algebras with operators we study modal correspondences between algebraic laws in the three algebras. The class of lr-multisemigroups introduced in this article generalises Schweizer and Sklar's function systems and object-free categories to a setting isomorphic to algebras of ternary relations as used in boolean algebras with operators and in substructural logics. Our results provide a generic construction recipe for weighted modal quantales from such multisemigroups. This is illustrated by many examples, ranging from modal algebras of weighted relations as used in fuzzy mathematics, category quantales in the tradition of category algebras or group rings, incidence algebras over partial orders, discrete and continuous weighted path algebras, weighted languages of pomsets with interfaces, and weighted languages associated with presimplicial and precubical sets. We also discuss how these results can be combined with previous ones for concurrent quantales and generalised to a setting that supports reasoning with stochastic matrices or probabilistic predicate transformers.
We give a formalization of Pratt's intuitive sculpting process for higher-dimensional automata (HDA). Intuitively, an HDA is a sculpture if it can be embedded in (i.e., sculpted from) a single higher dimensional cell (hypercube). A first important result of this paper is that not all HDA can be sculpted, exemplified through several natural acyclic HDA, one being the famous "broken box" example of van Glabbeek. Moreover, we show that even the natural operation of unfolding is completely unrelated to sculpting, e.g., there are sculptures whose unfoldings cannot be sculpted. We investigate the expressiveness of sculptures, as a proper subclass of HDA, by showing them to be equivalent to regular ST-structures (an event-based counterpart of HDA) and to (regular) Chu spaces over 3 (in their concurrent interpretation given by Pratt). We believe that our results shed new light on the intuitions behind sculpting as a method of modeling concurrent behavior, showing the precise reaches of its expressiveness. Besides expressiveness, we also develop an algorithm to decide whether an HDA can be sculpted. More importantly, we show that sculptures are equivalent to Euclidean cubical complexes (being the geometrical counterpart of our combinatorial definition), which include the popular PV models used for deadlock detection. This exposes a close connection between geometric and combinatorial models for concurrency which may be of use for both areas.
The main goal of this paper is to prove that the space of directed loops on the final precubical set is homotopy equivalent to the "total" configuration space of points on the plane; by "total" we mean that any finite number of points in a configuration is allowed. We also provide several applications: we define new invariants of precubical sets, prove that directed path spaces on any precubical complex have the homotopy types of CW-complexes and construct certain presentations of configuration spaces of points on the plane as nerves of categories.
For a given pre-cubical set ($\square$--set) $K$ with two distinguished vertices $\bO$, $\bI$, we prove that the space $\vP(K)_\bO^\bI$ of d-paths on the geometric realization of $K$ with source $\bO$ and target $\bI$ is homotopy equivalent to its subspace $\vP^t(K)_\bO^\bI$ of tame d-paths. When $K$ is the underlying $\square$--set of a Higher Dimensional Automaton $A$, tame d-paths on $K$ represent step executions of $A$. Then, we define the cube chain category of $K$ and prove that its nerve is weakly homotopy equivalent to $\vP(K)_\bO^\bI$.