State space reduction for process algebra specifications

DOI10.1016/j.tcs.2005.09.064zbMath1086.68091OpenAlexW1982254742MaRDI QIDQ820124

Wendelin Serwe, Hubert Garavel

Publication date: 6 April 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.09.064

zbMATH Keywords

process algebraformal specificationmodel checkingdata-flow analysiscompositional verificationCADPlabeled transition systemLOTOSCÆSAR

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (10)

Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets ⋮ Translating FSP into LOTOS and networks of automata ⋮ Automatic Decomposition of Petri Nets into Automata Networks – A Synthetic Account ⋮ Nested-unit Petri nets ⋮ CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes ⋮ On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP ⋮ CAESAR ⋮ State Space Reduction of Linear Processes Using Control Flow Reconstruction ⋮ Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular ⋮ Efficient algorithms for three reachability problems in safe Petri nets

Uses Software

• SPIN
• Murphi

Cites Work

• State space reduction based on live variables analysis.
• Static analysis for state-space reductions preserving temporal logics
• Algebraic Methodology and Software Technology
• Unnamed Item
• Unnamed Item

This page was built for publication: State space reduction for process algebra specifications