Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds

Andrei Sandler, Olga Tveretina

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

39 Downloads (Pure)

Abstract

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
Pages178-192
Number of pages15
Volume11674
ISBN (Electronic)9783030308063
ISBN (Print)9783030308056
DOIs
Publication statusPublished - 6 Sept 2019

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11674

Keywords

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

Fingerprint

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

Cite this