Robust model checking of timed automata under clock drifts

Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Timed automata have an idealized semantics where clocks are assumed to be perfectly continuous and synchronized, and guards have infinite precision. These assumptions cannot be realized physically. In order to ensure that correct timed automata designs can be implemented on real-time platforms, several authors have suggested that timed automata be studied under robust semantics. A timed automaton T-L is said to robustly satisfy a property if there is a positive e and/or a positive 5 such that the automaton satisfies the property even when the clocks are allowed to drift by e and/or guards are enlarged by 5. In this paper we show that, 1. checking ω-regular properties when only clocks are perturbed or when both clocks and guards are perturbed, is PSPACE-complete; and 2. one can compute the exact reachable set of a bounded timed automaton when clocks are drifted by infinitesimally small amount, using polynomial space. In particular, we remove the restrictive assumption on the timed automaton that its region graph only contains progress cycles, under which the second result above has been previously established.

Original languageEnglish (US)
Title of host publicationHSCC 2017 - Proceedings of the 20th International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control (part of CPS Week)
PublisherAssociation for Computing Machinery
Pages153-162
Number of pages10
ISBN (Electronic)9781450345903
DOIs
StatePublished - Apr 13 2017
Event20th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2017 - Pittsburgh, United States
Duration: Apr 18 2017Apr 20 2017

Publication series

NameHSCC 2017 - Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Other

Other20th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2017
Country/TerritoryUnited States
CityPittsburgh
Period4/18/174/20/17

ASJC Scopus subject areas

  • Computer Science Applications
  • Computer Networks and Communications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Robust model checking of timed automata under clock drifts'. Together they form a unique fingerprint.

Cite this