State space reduction for process algebra specifications

DOI10.1016/J.TCS.2005.09.064MaRDI QIDQ820124zbMATH OpenOpenAlexFDO

Authors Hubert Garavel, Wendelin Serwe

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

model checkingcompositional verificationprocess algebraCADPformal specificationlabeled transition systemdata-flow analysisLOTOSCÆ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)

Recommendations

• Algebraic Methodology and Software Technology
• State space reduction of linear processes using control flow reconstruction
• Static analysis for state-space reductions preserving temporal logics
• State space reduction based on live variables analysis.
• scientific article; zbMATH DE number 1487855

Cites work

• scientific article; zbMATH DE number 1487855 (Why is no real title available?)
• scientific article; zbMATH DE number 1418459 (Why is no real title available?)
• Algebraic Methodology and Software Technology
• State space reduction based on live variables analysis.
• Static analysis for state-space reductions preserving temporal logics

Cited in

(13)

• Nested-unit Petri nets
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• Translating FSP into LOTOS and networks of automata
• Static analysis of IMC
• scientific article; zbMATH DE number 1905121 (Why is no real title available?)
• Reflections on the future of concurrency theory in general and process calculi in particular
• State space reduction of linear processes using control flow reconstruction
• Nested-unit Petri nets: a structural means to increase efficiency and scalability of verification on elementary nets
• CAESAR
• Automatic decomposition of Petri nets into automata networks -- a synthetic account
• On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP
• Efficient algorithms for three reachability problems in safe Petri nets
• Algebraic Methodology and Software Technology

Describes a project that uses

Uses Software

• SPIN
• Murphi

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q820124)