Reducing clocks in timed automata while preserving bisimulation

DOI10.1007/978-3-662-44584-6_36MaRDI QIDQ3190141zbMATH OpenOpenAlexFDO

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

Publication date 15 September 2014

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

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

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)

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.

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

Cited in

(8)

• An automated system repair framework with signal temporal logic
• An efficient customized clock allocation algorithm for a class of timed automata
• Clock allocation in timed automata and graph colouring
• 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
• CONCUR 2005 – Concurrency Theory
• Reducing quasi-equal clocks in networks of timed automata
• Untangling the graphs of timed automata to decrease the number of 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)