Extended beam search for non-exhaustive state space analysis

DOI10.1016/J.JLAP.2011.06.002zbMATH Open1269.68048OpenAlexW2123777643MaRDI QIDQ652163FDOQ652163

Authors: M. Dashti, Anton Wijs 

Publication date: 19 December 2011

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2011.06.002

Recommendations

• Pruning State Spaces with Extended Beam Search
• Distributed Extended Beam Search for Quantitative Model Checking
• Extended breadth-first search algorithm in practice
• Incremental beam search
• Abstract reduction in directed model checking CCS processes

zbMATH Keywords

heuristicsmodel checkingformal analysisguided traversalstate space generation

Mathematics Subject Classification ID

Searching and sorting (68P10) Nonnumerical algorithms (68W05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Formal Methods for the Design of Real-Time Systems
• Title not available (Why is that?)
• A note on two problems in connexion with graphs
• Heuristic search viewed as path finding in a graph
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Multi-objective Model Checking of Markov Decision Processes
• KBFS: K-Best-First Search
• Job shop scheduling with beam search
• Beam search algorithms for the single machine total weighted tardiness scheduling problem with sequence-dependent setups
• A Recovering Beam Search algorithm for the one-machine dynamic total completion time scheduling problem
• The Single Machine Early/Tardy Problem
• State-Space Search
• Improved lower bounds for the early/tardy scheduling problem with no idle time
• Depth-first iterative-deepening: An optimal admissible tree search
• Efficient on-the-fly model-checking for regular alternation-free \(\mu\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal Modeling and Analysis of Timed Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Foundations of Software Science and Computational Structures
• Title not available (Why is that?)
• Survey on Directed Model Checking
• Title not available (Why is that?)
• Linear-space best-first search
• Pruning State Spaces with Extended Beam Search
• Hierarchical Adaptive State Space Caching Based on Level Sampling
• Falsification of LTL Safety Properties in Hybrid Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Distributed Extended Beam Search for Quantitative Model Checking
• Model Checking Software
• Lectures on Formal methods and performance analysis. 1st EEF/Euro summer school on trends in computer science, Berg en Dal, the Netherlands, July 3--7, 2000. Revised lectures

Cited In (5)

• Extended breadth-first search algorithm in practice
• Pruning State Spaces with Extended Beam Search
• Title not available (Why is that?)
• Distributed Extended Beam Search for Quantitative Model Checking
• Incremental beam search

Uses Software

• mCRL2
• SPIN
• Uppaal
• LTSmin
• mCRL

This page was built for publication: Extended beam search for non-exhaustive state space analysis

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