The sweep-line state space exploration method

DOI10.1016/J.TCS.2011.12.036MaRDI QIDQ418783zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Kurt Jensen, Thomas Mailund, Lars M. Kristensen

Publication date 30 May 2012

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

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

zbMATH Keywords

verificationmodel checkingcoloured Petri netsconcurrent systemsexplicit state space explorationstate explosionsweep-line method

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

• scientific article; zbMATH DE number 2090157
• scientific article; zbMATH DE number 1973992
• scientific article; zbMATH DE number 1701774
• scientific article; zbMATH DE number 2088669
• A sweep-line method for Büchi automata-based model checking

Cites work

• scientific article; zbMATH DE number 1696471 (Why is no real title available?)
• scientific article; zbMATH DE number 1701774 (Why is no real title available?)
• scientific article; zbMATH DE number 2088662 (Why is no real title available?)
• scientific article; zbMATH DE number 2088669 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3885321 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 177511 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1973992 (Why is no real title available?)
• scientific article; zbMATH DE number 2090157 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A theory of timed automata
• An improvement of McMillan's unfolding algorithm
• Coloured Petri Nets
• Formal Methods in Computer-Aided Design
• Lectures on Concurrency and Petri Nets
• Lectures on Petri nets. 1: Basic models. Advances in Petri nets
• Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking
• State space reduction using partial order techniques
• The ComBack Method – Extending Hash Compaction with Backtracking
• To store or not to store.
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(7)

• scientific article; zbMATH DE number 1701774 (Why is no real title available?)
• scientific article; zbMATH DE number 2088669 (Why is no real title available?)
• scientific article; zbMATH DE number 1973992 (Why is no real title available?)
• scientific article; zbMATH DE number 2090157 (Why is no real title available?)
• Tools and Algorithms for the Construction and Analysis of Systems
• A sweep-line method for Büchi automata-based model checking
• Hybrid on-the-fly LTL model checking with the sweep-line method

Describes a project that uses

Uses Software

• CPN/Tools
• Design/CPN
• SPIN
• DiVinE
• LoLA
• Murphi

This page was built for publication: The sweep-line state space exploration method

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