State Space Reduction of Linear Processes using Control Flow Reconstruction

    Research output: Book/ReportReportAcademic

    12 Citations (Scopus)
    50 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 languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages25
    Publication statusPublished - 23 Jun 2009

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-09-24
    ISSN (Print)1381-3625

    Keywords

    • State space reduction
    • EWI-15471
    • Dead variable analysis
    • IR-67478
    • Control flow reconstruction
    • Process Algebra
    • METIS-263893

    Cite this

    van de Pol, J. C., & Timmer, M. (2009). State Space Reduction of Linear Processes using Control Flow Reconstruction. (CTIT Technical Report Series; No. TR-CTIT-09-24). Enschede: Centre for Telematics and Information Technology (CTIT).
    van de Pol, Jan Cornelis ; Timmer, Mark. / State Space Reduction of Linear Processes using Control Flow Reconstruction. Enschede : Centre for Telematics and Information Technology (CTIT), 2009. 25 p. (CTIT Technical Report Series; TR-CTIT-09-24).
    @book{0dba8b03b56a46dcaf2ec93349fecb36,
    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 = "State space reduction, EWI-15471, Dead variable analysis, IR-67478, Control flow reconstruction, Process Algebra, METIS-263893",
    author = "{van de Pol}, {Jan Cornelis} and Mark Timmer",
    year = "2009",
    month = "6",
    day = "23",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "TR-CTIT-09-24",
    address = "Netherlands",

    }

    van de Pol, JC & Timmer, M 2009, State Space Reduction of Linear Processes using Control Flow Reconstruction. CTIT Technical Report Series, no. TR-CTIT-09-24, Centre for Telematics and Information Technology (CTIT), Enschede.

    State Space Reduction of Linear Processes using Control Flow Reconstruction. / van de Pol, Jan Cornelis; Timmer, Mark.

    Enschede : Centre for Telematics and Information Technology (CTIT), 2009. 25 p. (CTIT Technical Report Series; No. TR-CTIT-09-24).

    Research output: Book/ReportReportAcademic

    TY - BOOK

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

    AU - van de Pol, Jan Cornelis

    AU - Timmer, Mark

    PY - 2009/6/23

    Y1 - 2009/6/23

    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 - State space reduction

    KW - EWI-15471

    KW - Dead variable analysis

    KW - IR-67478

    KW - Control flow reconstruction

    KW - Process Algebra

    KW - METIS-263893

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - State Space Reduction of Linear Processes using Control Flow Reconstruction

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    van de Pol JC, Timmer M. State Space Reduction of Linear Processes using Control Flow Reconstruction. Enschede: Centre for Telematics and Information Technology (CTIT), 2009. 25 p. (CTIT Technical Report Series; TR-CTIT-09-24).