There has been a growing interest in defining models of automata enriched with time, such as finite automata extended with clocks (timed automata). In this paper, we study deterministic timed finite state machines (TFSMs), i.e., finite state machines with a single clock, timed guards and timeouts which transduce timed input words into timed output words. We solve the problem of equivalence checking by defining a bisimulation from timed FSMs to untimed ones and vice versa. Moreover, we apply these bisimulation relations to build the intersection of two timed finite state machines by untiming them, intersecting them and transforming back to the timed intersection. It is known that many problems like inclusion and equivalence checking are undecidable for timed automata. Our results show that TFSMs correspond to a decidable subclass of timed automata that admits a restricted form of ε-transitions (i.e., timeouts) where most of the relevant problems like equivalence and intersection are decidable.

Equivalence checking and intersection of deterministic timed finite state machines

Tiziano Villa;
2022

Abstract

There has been a growing interest in defining models of automata enriched with time, such as finite automata extended with clocks (timed automata). In this paper, we study deterministic timed finite state machines (TFSMs), i.e., finite state machines with a single clock, timed guards and timeouts which transduce timed input words into timed output words. We solve the problem of equivalence checking by defining a bisimulation from timed FSMs to untimed ones and vice versa. Moreover, we apply these bisimulation relations to build the intersection of two timed finite state machines by untiming them, intersecting them and transforming back to the timed intersection. It is known that many problems like inclusion and equivalence checking are undecidable for timed automata. Our results show that TFSMs correspond to a decidable subclass of timed automata that admits a restricted form of ε-transitions (i.e., timeouts) where most of the relevant problems like equivalence and intersection are decidable.
Timed finite state machines, equivalence checking, bisimulation
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1075266
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact