State Space Reduction of Linear Processes Using Control Flow Reconstruction

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    15 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 languageEnglish
    Title of host publicationAutomated Technology for Verification and Analysis
    Subtitle of host publication7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings
    EditorsZhiming Liu, Anders P. Ravn
    Place of PublicationBerlin
    PublisherSpringer
    Pages54-68
    Number of pages15
    ISBN (Electronic)978-3-642-04761-9
    ISBN (Print)978-3-642-04760-2
    DOIs
    Publication statusPublished - 13 Oct 2009
    Event7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009 - Macao, China
    Duration: 14 Oct 200916 Oct 2009
    Conference number: 7

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume5799
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009
    Abbreviated titleATVA
    CountryChina
    CityMacao
    Period14/10/0916/10/09

    Fingerprint

    Flow control
    Process control
    Specifications
    Data flow analysis
    Static analysis
    Linearization
    Explosions

    Keywords

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

    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). Berlin: 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",
    year = "2009",
    month = "10",
    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 proceedingConference contributionAcademicpeer-review

    TY - GEN

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

    AU - van de Pol, Jan Cornelis

    AU - Timmer, Mark

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

    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

    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). https://doi.org/10.1007/978-3-642-04761-9_5