Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds

Andrei Sandler, Olga Tveretina

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

27 Downloads (Pure)


A hybrid automaton is a finite state machine combined with some k real-valued continuous variables, where k determines the number of the automaton dimensions. This formalism is widely used for modelling safety-critical systems, and verification tasks for such systems can often be expressed as the reachability problem for hybrid automata. Asarin, Mysore, Pnueli and Schneider defined classes of hybrid automata lying on the boundary between decidability and undecidability in their seminal paper ‘Low dimensional hybrid systems - decidable, undecidable, don’t know’ [9]. They proved that certain decidable classes become undecidable when given a little additional computational power, and showed that the reachability question remains unsolved for some 2-dimensional systems. Piecewise Constant Derivative Systems on 2-dimensional manifolds (or PCD2m) constitute a class of hybrid automata for which decidability of the reachability problem is unknown. In this paper we show that the reachability problem becomes decidable for PCD2m if we slightly limit their dynamics, and thus we partially answer the open question of Asarin, Mysore, Pnueli and Schneider posed in [9].
Original languageEnglish
Title of host publicationReachability Problems - 13th International Conference, RP 2019, Proceedings
EditorsEmmanuel Filiot, Raphaël Jungers, Igor Potapov
PublisherSpringer Nature
Number of pages15
ISBN (Electronic)9783030308063
ISBN (Print)9783030308056
Publication statusPublished - 6 Sept 2019

Publication series

NameLecture Notes in Computer Science


  • Hybrid Systems, reachability, decidability
  • Decidability
  • Hybrid systems
  • Reachability


Dive into the research topics of 'Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds'. Together they form a unique fingerprint.

Cite this