Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

State estimation of timed automata under partial observation [Draft version]

Chao Gao, Dimitri Lefebvre, Carla Seatzu, Zhiwu Li, Alessandro Giua

TL;DR

An algorithm is formulated to provide an approach for state estimation of a timed automaton based on the assumption that the clock is reset upon the occurrence of each observable transition.

Abstract

In this paper, we consider partially observable timed automata endowed with a single clock. A time interval is associated with each transition specifying at which clock values it may occur. In addition, a resetting condition associated to a transition specifies how the clock value is updated upon its occurrence. This work deals with the estimation of the current state given a timed observation, i.e., a succession of pairs of an observable event and the time instant at which the event has occurred. The problem of state reachability in the timed automaton is reduced to the reachability analysis of the associated zone automaton, which provides a purely discrete event description of the behaviour of the timed automaton. An algorithm is formulated to provide an offline approach for state estimation of a timed automaton based on the assumption that the clock is reset upon the occurrence of each observable transition.

State estimation of timed automata under partial observation [Draft version]

TL;DR

An algorithm is formulated to provide an approach for state estimation of a timed automaton based on the assumption that the clock is reset upon the occurrence of each observable transition.

Abstract

In this paper, we consider partially observable timed automata endowed with a single clock. A time interval is associated with each transition specifying at which clock values it may occur. In addition, a resetting condition associated to a transition specifies how the clock value is updated upon its occurrence. This work deals with the estimation of the current state given a timed observation, i.e., a succession of pairs of an observable event and the time instant at which the event has occurred. The problem of state reachability in the timed automaton is reduced to the reachability analysis of the associated zone automaton, which provides a purely discrete event description of the behaviour of the timed automaton. An algorithm is formulated to provide an offline approach for state estimation of a timed automaton based on the assumption that the clock is reset upon the occurrence of each observable transition.
Paper Structure (9 sections, 4 theorems, 1 equation, 2 figures, 2 tables, 2 algorithms)

This paper contains 9 sections, 4 theorems, 1 equation, 2 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Problem Statement
  4. Zone automaton
  5. Dynamics of a zone automaton
  6. State estimation of TFA
  7. State estimation under no observation
  8. State estimation under partial observation
  9. Conclusions and future work

Key Result

Theorem 1

Given a TFA $G=(X, E, \Delta, \Gamma, Reset, X_0)$, zone automaton $G_z=(V, E_\tau, \Delta_z, V_0)$ and a time instant $T\in\mathbb{R}_{\geq 0}$, $x^\prime\in X$ is $T$-reachable from $x\in X$ if and only if there exists a run $\bar{\rho}$ in $G_z$ such that $T\in d(\bar{\rho})$, $v_{st}(\bar{\rho})

Figures (2)

  • Figure 1: A TFA $G$ w.r.t. the given timing function and clock resetting function.
  • Figure 2: Zone automaton $G_z$ of the TFA $G$ in Fig. \ref{['tfaG']}.

Theorems & Definitions (24)

  • Definition 1
  • Definition 2
  • Example 1
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Example 2
  • Definition 7: gao2023ifac
  • Example 3
  • ...and 14 more