State Space Reduction of Linear Processes using Control Flow Reconstruction

Research output: Book/ReportReportAcademic

12 Citations (Scopus)
40 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).