arXiv subjects

Uli Fahrenberg

Publications and source records attributed to Uli Fahrenberg.

At least 19 recordsLinked to original sources

arXiv2026

Automata on Graph Alphabets

The theory of finite automata concerns itself with words in a free monoid together with concatenation and without further structure. There are, however, important applications which use alphabets which are structured in some sense. We introduce automata over a particular type of structured data, namely an alphabet which is given as a (finite or infinite) directed graph. This constrains concatenation: two strings may only be concatenated if the end vertex of the first is equal to the start vertex of the second. We develop the beginnings of an automata theory for languages on graph alphabets. We show that they admit a Kleene theorem, relating rational and regular languages, and a Myhill-Nerode theorem, stating that languages are regular iff they have finite prefix or, equivalently, suffix quotient. We present determinization and minimization algorithms, but we also exhibit that regular languages are not stable by complementation. Finally, we mention how these structures could be generalized to presimplicial alphabets, where languages are no more freely generated.

cs.FL↗

arXiv2026

Higher-Dimensional Automata : Extension to Infinite Tracks

We introduce higher-dimensional automata for infinite interval ipomsets ($ω$-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by $ω$-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with $ω$-HDAs and show that while languages of $ω$-HDAs are $ω$-rational, not all $ω$-rational languages can be expressed by $ω$-HDAs.

cs.FL↗

arXiv2026

Variants of Higher-Dimensional Automata

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.

cs.FL↗

arXiv2025

Büchi-Elgot-Trakhtenbrot Theorem for Higher-Dimensional Automata

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.

cs.FL↗

arXiv2025

Higher-Dimensional Timed Automata for Real-Time Concurrency

We present a new language semantics for real-time concurrency. Its operational models are higher-dimensional timed automata (HDTAs), a generalization of both higher-dimensional automata and timed automata. In real-time concurrent systems, both concurrency of events and timing and duration of events are of interest. Thus, HDTAs combine the non-interleaving concurrency model of higher-dimensional automata with the real-time modeling, using clocks, of timed automata. We define languages of HDTAs as sets of interval-timed pomsets with interfaces. We show that language inclusion of HDTAs is undecidable. On the other hand, using a region construction we can show that untimings of HDTA languages have enough regularity so that untimed language inclusion is decidable. On a more practical note, we give new insights on when practical applications, like checking reachability, might benefit from using HDTAs instead of classical timed automata.

cs.FL↗

arXiv2025

Petri Nets and Higher-Dimensional Automata

Petri nets and their variants are often considered through their interleaved semantics, i.e. considering executions where, at each step, a single transition fires. This is clearly a miss, as Petri nets are a true concurrency model. This paper revisits the semantics of Petri nets as higher-dimensional automata (HDAs) as introduced by van Glabbeek, which methodically take concurrency into account. We extend the translation to include some common features. We consider nets with inhibitor arcs, under both concurrent semantics used in the literature, and generalized self-modifying nets. Finally, we present a tool that implements our translations.

cs.LO↗

arXiv2024

Kleene Theorem for Higher-Dimensional Automata

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.

cs.FL↗

arXiv2024

Bisimulations and Logics for Higher-Dimensional Automata

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.

cs.LO↗

arXiv2024

Myhill-Nerode Theorem for Higher-Dimensional Automata

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.

cs.FL↗

arXiv2024

$ω$-Regular Energy Problems

We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm interleaved with Couvreur's algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source platforms TChecker and~Spot.

cs.LO↗

arXiv2024

Closure and Decision Properties for Higher-Dimensional Automata

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.

cs.FL↗

arXiv2024

Presenting Interval Pomsets with Interfaces

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.

cs.FL↗

arXiv2024

Logic and Languages of Higher-Dimensional Automata

In this paper we study finite higher-dimensional automata (HDAs) from the logical point of view. Languages of HDAs are sets of finite bounded-width interval pomsets with interfaces (iiPoms<=k) closed under order extension. We prove that languages of HDAs are MSO-definable. For the converse, we show that the order extensions of MSO-definable sets of iiPoms<=k are languages of HDAs. As a consequence, unlike the case of all pomsets, order extension of MSO-definable sets of iiPoms<=k is also MSO-definable.

cs.FL↗

arXiv2022

Posets with Interfaces as a Model for Concurrency

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.

cs.FL↗

arXiv2022

A Generic Approach to Quantitative Verification

This thesis is concerned with quantitative verification, that is, the verification of quantitative properties of quantitative systems. These systems are found in numerous applications, and their quantitative verification is important, but also rather challenging. In particular, given that most systems found in applications are rather big, compositionality and incrementality of verification methods are essential. In order to ensure robustness of verification, we replace the Boolean yes-no answers of standard verification with distances. Depending on the application context, many different types of distances are being employed in quantitative verification. Consequently, there is a need for a general theory of system distances which abstracts away from the concrete distances and develops quantitative verification at a level independent of the distance. It is our view that in a theory of quantitative verification, the quantitative aspects should be treated just as much as input to a verification problem as the qualitative aspects are. In this work we develop such a general theory of quantitative verification. We assume as input a distance between traces, or executions, and then employ the theory of games with quantitative objectives to define distances between quantitative systems. Different versions of the quantitative bisimulation game give rise to different types of distances, viz.~bisimulation distance, simulation distance, trace equivalence distance, etc., enabling us to construct a quantitative generalization of van Glabbeek's linear-time--branching-time spectrum. We also extend our general theory of quantitative verification to a theory of quantitative specifications. For this we use modal transition systems, and we develop the quantitative properties of the usual operators for behavioral specification theories.

cs.LO↗

arXiv2022

Generating Posets with Interfaces

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.

math.CO↗

arXiv2021

Languages of Higher-Dimensional Automata

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.

cs.FL↗

arXiv2021

lr-Multisemigroups and Modal Convolution Algebras

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.

cs.LO↗