Fast Algorithms for Handling Diagonal Constraints in Timed Automata

Conference Paper

A popular method for solving reachability in timed automata proceeds by enumerating reachable sets of valuations represented as zones. A naïve enumeration of zones does not terminate. Various termination mechanisms have been studied over the years. Coming up with efficient termination mechanisms has been remarkably more challenging when the automaton has diagonal constraints in guards. In this paper, we propose a new termination mechanism for timed automata with diagonal constraints based on a new simulation relation between zones. Experiments with an implementation of this simulation show significant gains over existing methods.

Full Text

Duke Authors

Cited Authors

  • Gastin, P; Mukherjee, S; Srivathsan, B

Published Date

  • January 1, 2019

Published In

Volume / Issue

  • 11561 LNCS /

Start / End Page

  • 41 - 59

Electronic International Standard Serial Number (EISSN)

  • 1611-3349

International Standard Serial Number (ISSN)

  • 0302-9743

International Standard Book Number 13 (ISBN-13)

  • 9783030255398

Digital Object Identifier (DOI)

  • 10.1007/978-3-030-25540-4_3

Citation Source

  • Scopus