Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Myhill-Nerode Theorem for Higher-Dimensional Automata

Uli Fahrenberg, Krzysztof Ziemiański

TL;DR

A Myhill-Nerode type theorem is established, stating that a language is regular if and only if it has finite prefix quotient, and introduces deterministic HDAs and shows that not all HDAs are determinizable.

Abstract

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.

Myhill-Nerode Theorem for Higher-Dimensional Automata

TL;DR

A Myhill-Nerode type theorem is established, stating that a language is regular if and only if it has finite prefix quotient, and introduces deterministic HDAs and shows that not all HDAs are determinizable.

Abstract

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.
Paper Structure (2 sections, 1 theorem, 1 equation, 2 figures)

This paper contains 2 sections, 1 theorem, 1 equation, 2 figures.

Table of Contents

  1. Introduction
  2. Pomsets with interfaces

Key Result

Lemma 2.2

If $P$ is an (interval) iposet and $A\subseteq P$, then the set difference $P-A$ is an (interval) iposet as well.

Figures (2)

  • Figure 1: Petri net and HDA models distinguishing interleaving from non-interleaving concurrency. Left: Petri net and HDA models for $a. b+ b. a$; right: HDA and Petri net models for $a\mathrel{\|} b$.
  • Figure 2: Activity intervals (top) and corresponding iposets (bottom), see Example \ref{['ex:iposets1']}. Full arrows indicate precedence order; dashed arrows indicate event order; bullets indicate interfaces.

Theorems & Definitions (3)

  • Example 2.1
  • Lemma 2.2
  • Example 2.3