State estimation of timed automata under partial observation [Draft version]
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913494222241792 |
|---|---|
| author | Gao, Chao Lefebvre, Dimitri Seatzu, Carla Li, Zhiwu Giua, Alessandro |
| author_facet | Gao, Chao Lefebvre, Dimitri Seatzu, Carla Li, Zhiwu Giua, Alessandro |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_05810 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | State estimation of timed automata under partial observation [Draft version] Gao, Chao Lefebvre, Dimitri Seatzu, Carla Li, Zhiwu Giua, Alessandro Formal Languages and Automata Theory 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. |
| title | State estimation of timed automata under partial observation [Draft version] |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2409.05810 |