Equivalence checking and intersection of deterministic timed finite state machines

DOI10.1007/S10703-022-00396-6MaRDI QIDQ6108432zbMATH OpenWikidataFDO

Authors Davide Bresolin, Khaled El-Fakih, Tiziano Villa, Nina Yevtushenko

Publication date 29 June 2023

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2103.04868

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

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 viceversa. 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.

Recommendations

• Deterministic timed finite state machines: equivalence checking and expressive power
• A theory of timed automata
• Automata, Languages and Programming
• Formal Methods for the Design of Real-Time Systems
• Distinguishing experiments for timed nondeterministic finite state machines

Cites work

• A menagerie of timed automata
• A survey of timed automata for the development of real-time systems
• A theory of timed automata
• Automata, Languages and Programming
• Compositional specification of timed systems
• CONCUR 2004 - Concurrency Theory
• Deterministic timed finite state machines: equivalence checking and expressive power
• Distinguishing experiments for timed nondeterministic finite state machines
• Event clock automata: from theory to practice
• Event-clock automata: a determinizable class of timed automata
• Formal language properties of hybrid systems with strong resets
• Formal Methods for the Design of Real-Time Systems
• Formal testing from timed finite state machines
• scientific article; zbMATH DE number 5605076 (Why is no real title available?)
• scientific article; zbMATH DE number 1337733 (Why is no real title available?)
• scientific article; zbMATH DE number 1444359 (Why is no real title available?)
• Learning Mealy machines with one timer
• Learning one-clock timed automata
• On the power of non-observable actions in timed automata
• On the verification of timed discrete-event models
• One-Clock Deterministic Timed Automata Are Efficiently Identifiable in the Limit
• Reachability in two-clock timed automata is PSPACE-complete
• Real-time automata
• Removing -transitions in timed automata
• Removing all silent transitions from timed automata
• Switching and Finite Automata Theory
• Testing from a stochastic timed system with a fault model
• Testing Software Design Modeled by Finite-State Machines
• Testing timed automata
• The efficiency of identifying timed automata and the power of clocks
• The Unknown Component Problem
• Timed automata with non-instantaneous actions
• Undecidability Results for Timed Automata with Silent Transitions
• Undecidable Problems About Timed Automata
• Universality analysis for one-clock timed automata
• Updatable timed automata

Cited in

(1)

• Deterministic timed finite state machines: equivalence checking and expressive power

This page was built for publication: Equivalence checking and intersection of deterministic timed finite state machines

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6108432)