We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Formal Languages and Automata Theory

Title: Reducing Clocks in Timed Automata while Preserving Bisimulation

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.
Comments: 28 pages including reference, 8 figures, full version of paper accepted in CONCUR 2014
Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
ACM classes: F.1.1
Cite as: arXiv:1404.6613 [cs.FL]
  (or arXiv:1404.6613v2 [cs.FL] for this version)

Submission history

From: Shibashis Guha [view email]
[v1] Sat, 26 Apr 2014 06:00:58 GMT (440kb,D)
[v2] Wed, 20 May 2015 11:51:20 GMT (330kb,D)

Link back to: arXiv, form interface, contact.