Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computing the Bandwidth of Meager Timed Automata

Eugene Asarin, Aldric Degorre, Catalin Dima, Bernardo Jacobo Inclán

TL;DR

This work develops a finite-state, barycentric abstraction to compute the bandwidth of meager timed automata. It shows that the bandwidth of a region-split-timed automaton can be obtained by abstracting to a simply-timed graph whose states are barycenters of region faces, and proves that this abstraction preserves the bandwidth. The computation proceeds by 0-elimination, determinization, formulating an adjacency matrix $M(z)$, and solving $\det(I-M(z))=0$ to find the smallest root $z_0$, with the bandwidth given by $-\log|z_0|$; the overall procedure is doubly exponential due to region-splitting and determinization. The result enables a concrete, algebraic measure of information rate for meager automata and points to extending the approach to normal and obese classes in future work.

Abstract

The bandwidth of timed automata characterizes the quantity of information produced/transmitted per time unit. We previously delimited 3 classes of TA according to the nature of their asymptotic bandwidth: meager, normal, and obese. In this paper, we propose a method, based on a finite-state simply-timed abstraction, to compute the actual value of the bandwidth of meager automata. The states of this abstraction correspond to barycenters of the faces of the simplices in the region automaton. Then the bandwidth is $\log 1/|z_0|$ where $z_0$ is the smallest root (in modulus) of the characteristic polynomial of this finite-state abstraction.

Computing the Bandwidth of Meager Timed Automata

TL;DR

This work develops a finite-state, barycentric abstraction to compute the bandwidth of meager timed automata. It shows that the bandwidth of a region-split-timed automaton can be obtained by abstracting to a simply-timed graph whose states are barycenters of region faces, and proves that this abstraction preserves the bandwidth. The computation proceeds by 0-elimination, determinization, formulating an adjacency matrix , and solving to find the smallest root , with the bandwidth given by ; the overall procedure is doubly exponential due to region-splitting and determinization. The result enables a concrete, algebraic measure of information rate for meager automata and points to extending the approach to normal and obese classes in future work.

Abstract

The bandwidth of timed automata characterizes the quantity of information produced/transmitted per time unit. We previously delimited 3 classes of TA according to the nature of their asymptotic bandwidth: meager, normal, and obese. In this paper, we propose a method, based on a finite-state simply-timed abstraction, to compute the actual value of the bandwidth of meager automata. The states of this abstraction correspond to barycenters of the faces of the simplices in the region automaton. Then the bandwidth is where is the smallest root (in modulus) of the characteristic polynomial of this finite-state abstraction.
Paper Structure (6 sections, 3 theorems, 7 equations, 5 figures)

This paper contains 6 sections, 3 theorems, 7 equations, 5 figures.

Table of Contents

  1. Preliminaries
  2. Timed words, languages and automata
  3. Region-split form.
  4. Pseudo-distance on timed words
  5. Bandwidth of timed languages
  6. Simply-timed graphs and their bandwidth

Key Result

proposition thmcounterproposition

Operation $\mathop{\nu}$ maps timed words on $\Sigma$ to $0$-free ones on $2^\Sigma\setminus\{\emptyset\}$. $\mathop{\nu}(w_1)=\mathop{\nu}(w_2)$ if and only if the words $w_i, i=1,2$ admit decompositions $w_i=u_iv_i$ with $\mathop{\mathrm{dur}}(u_i)=0$ and $d(v_1,v_2)=0$.

Figures (5)

  • Figure 1: 7 running examples of timed automata, $I(q)=\{\mathbf{0}\}$, $F(\cdot)=\mathbf{true}$ for marked locations. An arrow labeled with $a,b$ is a shorthand for two transitions with the same guards and resets.
  • Figure 2: Pseudo-distance between two timed words (dotted lines with arrows represent directed matches between letters). $\overrightarrow{d}(u,v)=0.2;\ \overrightarrow{d}(v,u)=0.3$, thus $d(u,v)=0.3$.
  • Figure 3: A run of $\mathcal{A}_6$ on $(a,.9)(b,1.2)(a,1.8)(b,2.4)(a,2.7)(b,3.5)(a,3.6)(b,4.52)\\(a,4.59)(b,5.53)(a,5.58)(b,6.535)(a,6.575)$.
  • Figure 4: The region-split form of $\mathcal{A}_6$, constraints within states correspond to start conditions $S(\cdot)$.
  • Figure 5: A simply-timed graph (left), and its 0-free form (middle). Right: a 2-dimensional region, its 7 faces, and their barycenters.

Theorems & Definitions (15)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition: 0-elimination, words
  • proposition thmcounterproposition
  • definition thmcounterdefinition
  • definition thmcounterdefinition: bandwidth, formats2022
  • definition thmcounterdefinition: 3 classes, 3classes
  • definition thmcounterdefinition: Simply-timed graphs
  • ...and 5 more