A decidable class of planar linear hybrid systems

Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, Geir Dullerud

Research output: Contribution to journalArticle

Abstract

In this paper, we show the decidability of a new subclass of linear hybrid automata. These automata are planar, that is, consist of two state variables, monotonic along some direction in the plane and have identity resets, that is, the values of the continuous variables are not reset to a different value on a discrete transition. Our proof uses a combination of a tree construction capturing the edge-to-edge reachability and a finite bisimulation construction. Our class strictly contains the class of two dimensional piecewise constant derivative systems for which decidability of the reachability problem is known.

Original languageEnglish (US)
Pages (from-to)1-17
Number of pages17
JournalTheoretical Computer Science
Volume574
DOIs
StatePublished - Apr 1 2015

Keywords

  • Bisimulations
  • Decidability
  • Hybrid systems
  • Piecewise constant derivatives
  • Planar systems
  • Reachability
  • Safety
  • Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A decidable class of planar linear hybrid systems'. Together they form a unique fingerprint.

  • Cite this