A decidable class of planar linear hybrid systems

Pavithra Prabhakar; Vladimeros Vladimerou; Mahesh Viswanathan; Geir Dullerud

doi:10.1016/j.tcs.2014.11.018

A decidable class of planar linear hybrid systems

Pavithra Prabhakar
, Vladimeros Vladimerou
, Mahesh Viswanathan
, Geir Dullerud

Research output: Contribution to journal › Article › peer-review

2 Scopus citations

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 language	English (US)
Pages (from-to)	1-17
Number of pages	17
Journal	Theoretical Computer Science
Volume	574
DOIs	https://doi.org/10.1016/j.tcs.2014.11.018
State	Published - Apr 1 2015
Externally published	Yes

Bibliographical note

Publisher Copyright:
© 2014 Elsevier B.V.

Keywords

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

Publisher link

10.1016/j.tcs.2014.11.018

Find It

Find It at U of M Libraries

Cite this

@article{781ebc844b474901b4668abc4180f5ee,

title = "A decidable class of planar linear hybrid systems",

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.",

keywords = "Bisimulations, Decidability, Hybrid systems, Piecewise constant derivatives, Planar systems, Reachability, Safety, Verification",

author = "Pavithra Prabhakar and Vladimeros Vladimerou and Mahesh Viswanathan and Geir Dullerud",

note = "Publisher Copyright: {\textcopyright} 2014 Elsevier B.V.",

year = "2015",

month = apr,

day = "1",

doi = "10.1016/j.tcs.2014.11.018",

language = "English (US)",

volume = "574",

pages = "1--17",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - A decidable class of planar linear hybrid systems

AU - Prabhakar, Pavithra

AU - Vladimerou, Vladimeros

AU - Viswanathan, Mahesh

AU - Dullerud, Geir

PY - 2015/4/1

Y1 - 2015/4/1

N2 - 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.

AB - 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.

KW - Bisimulations

KW - Decidability

KW - Hybrid systems

KW - Piecewise constant derivatives

KW - Planar systems

KW - Reachability

KW - Safety

KW - Verification

UR - https://www.scopus.com/pages/publications/84944678928

UR - https://www.scopus.com/pages/publications/84944678928#tab=citedBy

U2 - 10.1016/j.tcs.2014.11.018

DO - 10.1016/j.tcs.2014.11.018

M3 - Article

AN - SCOPUS:84944678928

SN - 0304-3975

VL - 574

SP - 1

EP - 17

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

A decidable class of planar linear hybrid systems

Abstract

Bibliographical note

Keywords

Publisher link

Find It

Other files and links

Fingerprint

Cite this