Flow faster: efficient decision algorithms for probabilistic simulations

Lijun Zhang; H. Hermanns; Friedrich Eisenbrand; D.N. Jansen

doi:10.1007/978-3-540-71209-1_14

Flow faster: efficient decision algorithms for probabilistic simulations

Lijun Zhang, H. Hermanns, Friedrich Eisenbrand, D.N. Jansen

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

13 Citations (Scopus)

Abstract

Abstraction techniques based on simulation relations have become an important and effective proof technique to avoid the infamous state space explosion problem. In the context of Markov chains, strong and weak simulation relations have been proposed, together with corresponding decision algorithms, but it is as yet unclear whether they can be use as effectively as their non-stochastic counterparts. This paper presents drastically improved algorithms to decide whether one (discrete- or continuous-time) Markov chain strongly or weeakly simulaties another. The key innovation is the use of parametric maximum flow techniques to amortize computations.

Original language	Undefined
Title of host publication	Tools and algorithms for the construction and analysis of systems
Editors	O. Grumberg, M. Huth
Place of Publication	Berlin
Publisher	Springer
Pages	155-169
Number of pages	15
ISBN (Print)	978-3-540-71208-4
DOIs	https://doi.org/10.1007/978-3-540-71209-1_14
Publication status	Published - 2007
Event	13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007 - Braga, Portugal Duration: 24 Mar 2007 → 1 Apr 2007 Conference number: 13

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Number	2
Volume	4424

Conference

Conference	13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007
Abbreviated title	TACAS
Country/Territory	Portugal
City	Braga
Period	24/03/07 → 1/04/07

Access to Document

10.1007/978-3-540-71209-1_14

Cite this

Zhang, L., Hermanns, H., Eisenbrand, F., & Jansen, D. N. (2007). Flow faster: efficient decision algorithms for probabilistic simulations. In O. Grumberg, & M. Huth (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 155-169). [10.1007/978-3-540-71209-1_14] (Lecture notes in computer science; Vol. 4424, No. 2). Springer. https://doi.org/10.1007/978-3-540-71209-1_14

@inproceedings{b0d06948012e4cdb9bf81255087116dd,

title = "Flow faster: efficient decision algorithms for probabilistic simulations",

abstract = "Abstraction techniques based on simulation relations have become an important and effective proof technique to avoid the infamous state space explosion problem. In the context of Markov chains, strong and weak simulation relations have been proposed, together with corresponding decision algorithms, but it is as yet unclear whether they can be use as effectively as their non-stochastic counterparts. This paper presents drastically improved algorithms to decide whether one (discrete- or continuous-time) Markov chain strongly or weeakly simulaties another. The key innovation is the use of parametric maximum flow techniques to amortize computations.",

author = "Lijun Zhang and H. Hermanns and Friedrich Eisenbrand and D.N. Jansen",

note = "10.1007/978-3-540-71209-1_14 ; 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007 ; Conference date: 24-03-2007 Through 01-04-2007",

year = "2007",

doi = "10.1007/978-3-540-71209-1_14",

language = "Undefined",

isbn = "978-3-540-71208-4",

series = "Lecture notes in computer science",

publisher = "Springer",

number = "2",

pages = "155--169",

editor = "O. Grumberg and M. Huth",

booktitle = "Tools and algorithms for the construction and analysis of systems",

}

Zhang, L, Hermanns, H, Eisenbrand, F & Jansen, DN 2007, Flow faster: efficient decision algorithms for probabilistic simulations. in O Grumberg & M Huth (eds), Tools and algorithms for the construction and analysis of systems., 10.1007/978-3-540-71209-1_14, Lecture notes in computer science, no. 2, vol. 4424, Springer, Berlin, pp. 155-169, 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007, Braga, Portugal, 24/03/07. https://doi.org/10.1007/978-3-540-71209-1_14

Flow faster: efficient decision algorithms for probabilistic simulations. / Zhang, Lijun; Hermanns, H.; Eisenbrand, Friedrich et al.
Tools and algorithms for the construction and analysis of systems. ed. / O. Grumberg; M. Huth. Berlin: Springer, 2007. p. 155-169 10.1007/978-3-540-71209-1_14 (Lecture notes in computer science; Vol. 4424, No. 2).

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

TY - GEN

T1 - Flow faster: efficient decision algorithms for probabilistic simulations

AU - Zhang, Lijun

AU - Hermanns, H.

AU - Eisenbrand, Friedrich

AU - Jansen, D.N.

N1 - Conference code: 13

PY - 2007

Y1 - 2007

N2 - Abstraction techniques based on simulation relations have become an important and effective proof technique to avoid the infamous state space explosion problem. In the context of Markov chains, strong and weak simulation relations have been proposed, together with corresponding decision algorithms, but it is as yet unclear whether they can be use as effectively as their non-stochastic counterparts. This paper presents drastically improved algorithms to decide whether one (discrete- or continuous-time) Markov chain strongly or weeakly simulaties another. The key innovation is the use of parametric maximum flow techniques to amortize computations.

AB - Abstraction techniques based on simulation relations have become an important and effective proof technique to avoid the infamous state space explosion problem. In the context of Markov chains, strong and weak simulation relations have been proposed, together with corresponding decision algorithms, but it is as yet unclear whether they can be use as effectively as their non-stochastic counterparts. This paper presents drastically improved algorithms to decide whether one (discrete- or continuous-time) Markov chain strongly or weeakly simulaties another. The key innovation is the use of parametric maximum flow techniques to amortize computations.

U2 - 10.1007/978-3-540-71209-1_14

DO - 10.1007/978-3-540-71209-1_14

M3 - Conference contribution

SN - 978-3-540-71208-4

T3 - Lecture notes in computer science

SP - 155

EP - 169

BT - Tools and algorithms for the construction and analysis of systems

A2 - Grumberg, O.

A2 - Huth, M.

PB - Springer

CY - Berlin

T2 - 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007

Y2 - 24 March 2007 through 1 April 2007

ER -