Symmetry reduction for stochastic hybrid systems

L.M. Bujorianu; Joost P. Katoen

doi:10.1109/CDC.2008.4739086

Symmetry reduction for stochastic hybrid systems

L.M. Bujorianu, Joost P. Katoen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

182 Downloads (Pure)

Abstract

This paper is focused on adapting symmetry reduction, a technique that is highly successful in traditional model checking, to stochastic hybrid systems. We first show that performability analysis of stochastic hybrid systems can be reduced to a stochastic reachability analysis (SRA). Then, we generalize the notion of symmetry reduction as recently proposed for probabilistic model checking, to continuous probabilistic systems. We provide a rigorous mathematical foundation for the reduction technique in the continuous case and also investigate its observability perspective. For stochastic hybrid systems, characterizations for this reduction technique are provided, in terms of their infinitesimal generator.

Original language	Undefined
Title of host publication	47th IEEE Conference on Decision and Control, CDC 2008
Place of Publication	Los Alamitos
Publisher	IEEE
Pages	233-238
Number of pages	6
ISBN (Print)	978-1-4244-3123-6
DOIs	https://doi.org/10.1109/CDC.2008.4739086
Publication status	Published - 6 Jan 2009
Event	47th IEEE Conference on Decision and Control, CDC 2008 - Cancun, Mexico Duration: 9 Dec 2008 → 11 Dec 2008 Conference number: 47

Publication series

Name
Publisher	IEEE Computer Society Press
ISSN (Print)	0191-2216

Conference

Conference	47th IEEE Conference on Decision and Control, CDC 2008
Abbreviated title	CDC
Country/Territory	Mexico
City	Cancun
Period	9/12/08 → 11/12/08

Keywords

EWI-15275
abstractions
Reachability
Symmetries
transformation group
METIS-263807
IR-62797
Markov models
Markov Processes
Probability
probabilistic model checking

Access to Document

10.1109/CDC.2008.4739086

Cite this

@inproceedings{387721b7d3d94960a1dce7c6581deb74,

title = "Symmetry reduction for stochastic hybrid systems",

abstract = "This paper is focused on adapting symmetry reduction, a technique that is highly successful in traditional model checking, to stochastic hybrid systems. We first show that performability analysis of stochastic hybrid systems can be reduced to a stochastic reachability analysis (SRA). Then, we generalize the notion of symmetry reduction as recently proposed for probabilistic model checking, to continuous probabilistic systems. We provide a rigorous mathematical foundation for the reduction technique in the continuous case and also investigate its observability perspective. For stochastic hybrid systems, characterizations for this reduction technique are provided, in terms of their infinitesimal generator.",

keywords = "EWI-15275, abstractions, Reachability, Symmetries, transformation group, METIS-263807, IR-62797, Markov models, Markov Processes, Probability, probabilistic model checking",

author = "L.M. Bujorianu and Katoen, {Joost P.}",

note = "10.1109/CDC.2008.4739086 ; 47th IEEE Conference on Decision and Control, CDC 2008 ; Conference date: 09-12-2008 Through 11-12-2008",

year = "2009",

month = jan,

day = "6",

doi = "10.1109/CDC.2008.4739086",

language = "Undefined",

isbn = "978-1-4244-3123-6",

publisher = "IEEE",

pages = "233--238",

booktitle = "47th IEEE Conference on Decision and Control, CDC 2008",

address = "United States",

}

TY - GEN

T1 - Symmetry reduction for stochastic hybrid systems

AU - Bujorianu, L.M.

AU - Katoen, Joost P.

N1 - Conference code: 47

PY - 2009/1/6

Y1 - 2009/1/6

N2 - This paper is focused on adapting symmetry reduction, a technique that is highly successful in traditional model checking, to stochastic hybrid systems. We first show that performability analysis of stochastic hybrid systems can be reduced to a stochastic reachability analysis (SRA). Then, we generalize the notion of symmetry reduction as recently proposed for probabilistic model checking, to continuous probabilistic systems. We provide a rigorous mathematical foundation for the reduction technique in the continuous case and also investigate its observability perspective. For stochastic hybrid systems, characterizations for this reduction technique are provided, in terms of their infinitesimal generator.

AB - This paper is focused on adapting symmetry reduction, a technique that is highly successful in traditional model checking, to stochastic hybrid systems. We first show that performability analysis of stochastic hybrid systems can be reduced to a stochastic reachability analysis (SRA). Then, we generalize the notion of symmetry reduction as recently proposed for probabilistic model checking, to continuous probabilistic systems. We provide a rigorous mathematical foundation for the reduction technique in the continuous case and also investigate its observability perspective. For stochastic hybrid systems, characterizations for this reduction technique are provided, in terms of their infinitesimal generator.

KW - EWI-15275

KW - abstractions

KW - Reachability

KW - Symmetries

KW - transformation group

KW - METIS-263807

KW - IR-62797

KW - Markov models

KW - Markov Processes

KW - Probability

KW - probabilistic model checking

U2 - 10.1109/CDC.2008.4739086

DO - 10.1109/CDC.2008.4739086

M3 - Conference contribution

SN - 978-1-4244-3123-6

SP - 233

EP - 238

BT - 47th IEEE Conference on Decision and Control, CDC 2008

PB - IEEE

CY - Los Alamitos

T2 - 47th IEEE Conference on Decision and Control, CDC 2008

Y2 - 9 December 2008 through 11 December 2008

ER -