Reducing clocks in timed automata while preserving bisimulation

DOI10.1007/978-3-662-44584-6_36zbMATH Open1417.68102arXiv1404.6613OpenAlexW325265439MaRDI QIDQ3190141FDOQ3190141

Authors: Shibashis Guha, Chinmay Narayan, S. Arun-Kumar 

Publication date: 15 September 2014

Published in: CONCUR 2014 – Concurrency Theory (Search for Journal in Brave)

Abstract: Model checking timed automata becomes increasingly complex with the increase in the number of clocks. Hence it is desirable that one constructs an automaton with the minimum number of clocks possible. The problem of checking whether there exists a timed automaton with a smaller number of clocks such that the timed language accepted by the original automaton is preserved is known to be undecidable. In this paper, we give a construction, which for any given timed automaton produces a timed bisimilar automaton with the least number of clocks. Further, we show that such an automaton with the minimum possible number of clocks can be constructed in time that is doubly exponential in the number of clocks of the original automaton.

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

Recommendations

• Untangling the graphs of timed automata to decrease the number of clocks
• Reducing quasi-equal clocks in networks of timed automata
• Folk theorems on the determinization and minimization of timed automata
• CONCUR 2004 - Concurrency Theory
• Analysis of timed systems using time-abstracting bisimulations

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (8)

• An automated system repair framework with signal temporal logic
• Clock allocation in timed automata and graph colouring
• Reducing quasi-equal clocks in networks of timed automata
• Untangling the graphs of timed automata to decrease the number of clocks
• CONCUR 2005 – Concurrency Theory
• An efficient customized clock allocation algorithm for a class of timed automata
• Automated verification for real-time systems. Via implicit clocks and an extended Antimirov algorithm
• Biased clocks: a novel approach to improve the ability to perform predicate detection with \(O(1)\) clocks

This page was built for publication: Reducing clocks in timed automata while preserving bisimulation

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