State Space Reduction of Linear Processes Using Control Flow Reconstruction

Jan Cornelis van de Pol; Mark Timmer

doi:10.1007/978-3-642-04761-9_5

State Space Reduction of Linear Processes Using Control Flow Reconstruction

Jan Cornelis van de Pol, Mark Timmer

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

32 Downloads (Pure)

Abstract

We present a new method for fighting the state space explosion of process algebraic specifications, by performing static analysis on an intermediate format: linear process equations (LPEs). Our method consists of two steps: (1) we reconstruct the LPE's control flow, detecting control flow parameters that were introduced by linearisation as well as those already encoded in the original specification; (2) we reset parameters found to be irrelevant based on data flow analysis techniques similar to traditional liveness analysis, modified to take into account the parallel nature of the specifications. Our transformation is correct with respect to strong bisimilarity, and never increases the state space. Case studies show that impressive reductions occur in practice, which could not be obtained automatically without reconstructing the control flow.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings
Editors	Zhiming Liu, Anders P. Ravn
Place of Publication	Berlin
Publisher	Springer
Pages	54-68
Number of pages	15
ISBN (Electronic)	978-3-642-04761-9
ISBN (Print)	978-3-642-04760-2
DOIs	https://doi.org/10.1007/978-3-642-04761-9_5
Publication status	Published - 13 Oct 2009
Event	7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009 - Macao, China Duration: 14 Oct 2009 → 16 Oct 2009 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	5799
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009
Abbreviated title	ATVA
Country/Territory	China
City	Macao
Period	14/10/09 → 16/10/09

Keywords

IR-68161
METIS-264067
Dead variable analysis
EWI-16155
Process Algebra
Control flow reconstruction
State space reduction

Access to Document

10.1007/978-3-642-04761-9_5

State Space ReductionAccepted author version, 221 KB

Cite this

van de Pol, J. C., & Timmer, M. (2009). State Space Reduction of Linear Processes Using Control Flow Reconstruction. In Z. Liu, & A. P. Ravn (Eds.), Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings (pp. 54-68). (Lecture Notes in Computer Science; Vol. 5799). Springer. https://doi.org/10.1007/978-3-642-04761-9_5

van de Pol, Jan Cornelis ; Timmer, Mark. / State Space Reduction of Linear Processes Using Control Flow Reconstruction. Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. editor / Zhiming Liu ; Anders P. Ravn. Berlin : Springer, 2009. pp. 54-68 (Lecture Notes in Computer Science).

@inproceedings{aa1e09badac24b6d8d4e76ac766e1d75,

title = "State Space Reduction of Linear Processes Using Control Flow Reconstruction",

abstract = "We present a new method for fighting the state space explosion of process algebraic specifications, by performing static analysis on an intermediate format: linear process equations (LPEs). Our method consists of two steps: (1) we reconstruct the LPE's control flow, detecting control flow parameters that were introduced by linearisation as well as those already encoded in the original specification; (2) we reset parameters found to be irrelevant based on data flow analysis techniques similar to traditional liveness analysis, modified to take into account the parallel nature of the specifications. Our transformation is correct with respect to strong bisimilarity, and never increases the state space. Case studies show that impressive reductions occur in practice, which could not be obtained automatically without reconstructing the control flow.",

keywords = "IR-68161, METIS-264067, Dead variable analysis, EWI-16155, Process Algebra, Control flow reconstruction, State space reduction",

author = "{van de Pol}, {Jan Cornelis} and Mark Timmer",

note = "10.1007/978-3-642-04761-9_5 ; 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, ATVA ; Conference date: 14-10-2009 Through 16-10-2009",

year = "2009",

month = oct,

day = "13",

doi = "10.1007/978-3-642-04761-9_5",

language = "English",

isbn = "978-3-642-04760-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "54--68",

editor = "Zhiming Liu and Ravn, {Anders P.}",

booktitle = "Automated Technology for Verification and Analysis",

}

van de Pol, JC & Timmer, M 2009, State Space Reduction of Linear Processes Using Control Flow Reconstruction. in Z Liu & AP Ravn (eds), Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5799, Springer, Berlin, pp. 54-68, 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, Macao, China, 14/10/09. https://doi.org/10.1007/978-3-642-04761-9_5

State Space Reduction of Linear Processes Using Control Flow Reconstruction. / van de Pol, Jan Cornelis ; Timmer, Mark.
Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. ed. / Zhiming Liu; Anders P. Ravn. Berlin: Springer, 2009. p. 54-68 (Lecture Notes in Computer Science; Vol. 5799).

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

TY - GEN

T1 - State Space Reduction of Linear Processes Using Control Flow Reconstruction

AU - van de Pol, Jan Cornelis

AU - Timmer, Mark

N1 - Conference code: 7

PY - 2009/10/13

Y1 - 2009/10/13

N2 - We present a new method for fighting the state space explosion of process algebraic specifications, by performing static analysis on an intermediate format: linear process equations (LPEs). Our method consists of two steps: (1) we reconstruct the LPE's control flow, detecting control flow parameters that were introduced by linearisation as well as those already encoded in the original specification; (2) we reset parameters found to be irrelevant based on data flow analysis techniques similar to traditional liveness analysis, modified to take into account the parallel nature of the specifications. Our transformation is correct with respect to strong bisimilarity, and never increases the state space. Case studies show that impressive reductions occur in practice, which could not be obtained automatically without reconstructing the control flow.

AB - We present a new method for fighting the state space explosion of process algebraic specifications, by performing static analysis on an intermediate format: linear process equations (LPEs). Our method consists of two steps: (1) we reconstruct the LPE's control flow, detecting control flow parameters that were introduced by linearisation as well as those already encoded in the original specification; (2) we reset parameters found to be irrelevant based on data flow analysis techniques similar to traditional liveness analysis, modified to take into account the parallel nature of the specifications. Our transformation is correct with respect to strong bisimilarity, and never increases the state space. Case studies show that impressive reductions occur in practice, which could not be obtained automatically without reconstructing the control flow.

KW - IR-68161

KW - METIS-264067

KW - Dead variable analysis

KW - EWI-16155

KW - Process Algebra

KW - Control flow reconstruction

KW - State space reduction

U2 - 10.1007/978-3-642-04761-9_5

DO - 10.1007/978-3-642-04761-9_5

M3 - Conference contribution

SN - 978-3-642-04760-2

T3 - Lecture Notes in Computer Science

SP - 54

EP - 68

BT - Automated Technology for Verification and Analysis

A2 - Liu, Zhiming

A2 - Ravn, Anders P.

PB - Springer

CY - Berlin

T2 - 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009

Y2 - 14 October 2009 through 16 October 2009

ER -

van de Pol JC , Timmer M. State Space Reduction of Linear Processes Using Control Flow Reconstruction. In Liu Z, Ravn AP, editors, Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. Berlin: Springer. 2009. p. 54-68. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-04761-9_5

State Space Reduction of Linear Processes Using Control Flow Reconstruction

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this