Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Higher-Dimensional Timed Automata for Real-Time Concurrency

Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg, Philipp Schlehuber-Caissier

TL;DR

The paper addresses modeling real-time concurrency with non-interleaving semantics by introducing higher-dimensional timed automata (HDTAs), which pair the concurrency-aware framework of HDAs with real-time timing via clocks. It develops two equivalent language formalisms for these models: interval delay words (combining delay words with step-like actions) and timed ipomsets (timed pomsets with interfaces), proving their equivalence. It then defines the languages of HDTAs and proves two main results: language inclusion for HDTAs is undecidable, while untimed (untimed) language inclusion is decidable via region-based arguments and the Glue isomorphism between step sequences and ipomsets. The work also provides a translation from timed automata to HDTAs that preserves languages and demonstrates practical benefits for reachability and parallel composition through tensor products, suggesting directions for real-time concurrent model checking and logic-based specifications. Overall, HDTAs offer a rich, compositional framework for real-time concurrency with potential impact on verification, semantics, and tool support for analysis of complex parallel real-time systems.

Abstract

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.

Higher-Dimensional Timed Automata for Real-Time Concurrency

TL;DR

The paper addresses modeling real-time concurrency with non-interleaving semantics by introducing higher-dimensional timed automata (HDTAs), which pair the concurrency-aware framework of HDAs with real-time timing via clocks. It develops two equivalent language formalisms for these models: interval delay words (combining delay words with step-like actions) and timed ipomsets (timed pomsets with interfaces), proving their equivalence. It then defines the languages of HDTAs and proves two main results: language inclusion for HDTAs is undecidable, while untimed (untimed) language inclusion is decidable via region-based arguments and the Glue isomorphism between step sequences and ipomsets. The work also provides a translation from timed automata to HDTAs that preserves languages and demonstrates practical benefits for reachability and parallel composition through tensor products, suggesting directions for real-time concurrent model checking and logic-based specifications. Overall, HDTAs offer a rich, compositional framework for real-time concurrency with potential impact on verification, semantics, and tool support for analysis of complex parallel real-time systems.

Abstract

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.
Paper Structure (4 sections, 2 theorems, 13 equations, 2 figures)

This paper contains 4 sections, 2 theorems, 13 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Timed automata and their languages
  3. Higher-dimensional automata and their languages
  4. Higher-dimensional automata

Key Result

lemma thmcounterlemma

Any equivalence class of delay words has a unique representative of the form $d_0 a_1 d_1 a_2\dotsc a_n d_n$. $\sqcap$$\sqcup$=0

Figures (2)

  • Figure 1: Petri net and HDA models for $a c\mathop{\|} b$
  • Figure 2: Taxonomy of some models for time and concurrency

Theorems & Definitions (11)

  • definition thmcounterdefinition
  • remark thmcounterremark
  • definition thmcounterdefinition
  • remark thmcounterremark
  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • proof
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • ...and 1 more