Deciding concurrent planar monotonic linear hybrid systems

Pavithra Prabhakar, Nima Roohi, Mahesh Viswanathan

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

Abstract

Decidability results for hybrid automata often exploit subtle properties about dimensionality (number of continuous variables), and interaction between discrete transitions and continuous trajectories of variables. Thus, the decidability results often do not carry over to parallel compositions of hybrid automata, even when there is no communication other than the implicit synchronization of time. In this paper, we show that the reachability problem for concurrently running planar, monotonic hybrid automata is decidable. Planar, monotonic hybrid automata are a special class of linear hybrid automata with only two variables, whose flows in all states are simultaneously monotonic along some direction in the plane. The reachability problem is known to be decidable for this class. Our concurrently running automata synchronize with respect to a global clock, and through labeled discrete transitions. The proof of decidability hinges on a new observation that the timed trace language of a planar monotonic automaton can be recognized by a timed automaton, and the decidability result follows from the decidability of composition of timed automata. Our results identify a new decidable subclass of multirate hybrid automata.

Original languageEnglish (US)
Title of host publicationFormal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Proceedings
EditorsSriram Sankaranarayanan, Enrico Vicario
PublisherSpringer
Pages256-269
Number of pages14
ISBN (Print)9783319229744
DOIs
StatePublished - 2015
Event13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015 - Madrid, Spain
Duration: Sep 2 2015Sep 4 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9268
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015
Country/TerritorySpain
CityMadrid
Period9/2/159/4/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Deciding concurrent planar monotonic linear hybrid systems'. Together they form a unique fingerprint.

Cite this