Specifications for decidable hybrid games

Vladimeros Vladimerou; Pavithra Prabhakar; Mahesh Viswanathan; Geir Dullerud

doi:10.1016/j.tcs.2011.08.036

Specifications for decidable hybrid games

Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir Dullerud

Department of Automatic Control

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

Abstract

We introduce STORMED hybrid games (SHG), a generalization of STORMED hybrid systems, Vladimerou et al. (2008) [33], which have natural specifications that allow rich continuous dynamics and various decidable properties. We solve the control problem for SHG using a reduction to bisimulation on finite game graphs. This generalizes to a greater family of games, which includes o-minimal hybrid games, Bouyer et al. (2006)161. We also solve the optimal-cost reachability problem for Weighted SHG and prove decidability of WCTL for Weighted STORMED hybrid systems. (C) 2011 Elsevier B.V. All rights reserved.

Original language	English
Pages (from-to)	6770-6785
Journal	Theoretical Computer Science
Volume	412
Issue number	48
DOIs	https://doi.org/10.1016/j.tcs.2011.08.036
Publication status	Published - 2011

Bibliographical note

key=vlad_etal2011
month=November

Subject classification (UKÄ)

Control Engineering

Free keywords

Hybrid systems
Hybrid games
Weighted CTL
Control
Verification

Access to Document

10.1016/j.tcs.2011.08.036

Cite this

@article{6cd7c20fa29c47b292e9ff829fdb1258,

title = "Specifications for decidable hybrid games",

abstract = "We introduce STORMED hybrid games (SHG), a generalization of STORMED hybrid systems, Vladimerou et al. (2008) [33], which have natural specifications that allow rich continuous dynamics and various decidable properties. We solve the control problem for SHG using a reduction to bisimulation on finite game graphs. This generalizes to a greater family of games, which includes o-minimal hybrid games, Bouyer et al. (2006)161. We also solve the optimal-cost reachability problem for Weighted SHG and prove decidability of WCTL for Weighted STORMED hybrid systems. (C) 2011 Elsevier B.V. All rights reserved.",

keywords = "Hybrid systems, Hybrid games, Weighted CTL, Control, Verification",

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

note = "key=vlad_etal2011 month=November",

year = "2011",

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

language = "English",

volume = "412",

pages = "6770--6785",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

number = "48",

}

TY - JOUR

T1 - Specifications for decidable hybrid games

AU - Vladimerou, Vladimeros

AU - Prabhakar, Pavithra

AU - Viswanathan, Mahesh

AU - Dullerud, Geir

N1 - key=vlad_etal2011 month=November

PY - 2011

Y1 - 2011

N2 - We introduce STORMED hybrid games (SHG), a generalization of STORMED hybrid systems, Vladimerou et al. (2008) [33], which have natural specifications that allow rich continuous dynamics and various decidable properties. We solve the control problem for SHG using a reduction to bisimulation on finite game graphs. This generalizes to a greater family of games, which includes o-minimal hybrid games, Bouyer et al. (2006)161. We also solve the optimal-cost reachability problem for Weighted SHG and prove decidability of WCTL for Weighted STORMED hybrid systems. (C) 2011 Elsevier B.V. All rights reserved.

AB - We introduce STORMED hybrid games (SHG), a generalization of STORMED hybrid systems, Vladimerou et al. (2008) [33], which have natural specifications that allow rich continuous dynamics and various decidable properties. We solve the control problem for SHG using a reduction to bisimulation on finite game graphs. This generalizes to a greater family of games, which includes o-minimal hybrid games, Bouyer et al. (2006)161. We also solve the optimal-cost reachability problem for Weighted SHG and prove decidability of WCTL for Weighted STORMED hybrid systems. (C) 2011 Elsevier B.V. All rights reserved.

KW - Hybrid systems

KW - Hybrid games

KW - Weighted CTL

KW - Control

KW - Verification

U2 - 10.1016/j.tcs.2011.08.036

DO - 10.1016/j.tcs.2011.08.036

M3 - Article

SN - 0304-3975

VL - 412

SP - 6770

EP - 6785

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 48

ER -

Specifications for decidable hybrid games

Abstract

Bibliographical note

Subject classification (UKÄ)

Free keywords

Access to Document

Fingerprint

Cite this