Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power

Davide Bresolin
(University of Bologna)
Khaled El-Fakih
(American University of Sharjah)
Tiziano Villa
(University of Verona)
Nina Yevtushenko
(Tomsk State University)

There has been a growing interest in defining models of automata enriched with time. For instance, timed automata were introduced as automata extended with clocks. In this paper, we study models of timed finite state machines (TFSMs), i.e., FSMs enriched with time, which accept timed input words and generate timed output words. Here we discuss some models of TFSMs with a single clock: TFSMs with timed guards, TFSMs with timeouts, and TFSMs with both timed guards and timeouts. We solve the problem of equivalence checking for all three models, and we compare their expressive power, characterizing subclasses of TFSMs with timed guards and of TFSMs with timeouts that are equivalent to each other.

In Adriano Peron and Carla Piazza: Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2014), Verona, Italy, 10th - 12th September 2014, Electronic Proceedings in Theoretical Computer Science 161, pp. 203–216.
Published: 24th August 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: