Data structures for symbolic multi-valued model-checking

DOI10.1007/S10703-006-0016-ZMaRDI QIDQ862857zbMATH OpenOpenAlexFDO

Authors Marsha Chechik, Arie Gurfinkel, Benet Devereux, Albert Lai, Steve Easterbrook

Publication date 24 January 2007

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-006-0016-z

zbMATH Keywords

Decision diagramsSymbolic model-checkingMulti-valued logic

Mathematics Subject Classification ID

Data structures (68P05) Many-valued logic (03B50) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in artificial intelligence (68T27)

Recommendations

• scientific article; zbMATH DE number 1701772
• scientific article; zbMATH DE number 1863178
• Automata, Languages and Programming
• scientific article; zbMATH DE number 1693429
• Multi-valued model checking via classical model checking.

Cites work

• scientific article; zbMATH DE number 1670794 (Why is no real title available?)
• scientific article; zbMATH DE number 1693429 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 1701772 (Why is no real title available?)
• scientific article; zbMATH DE number 1330907 (Why is no real title available?)
• scientific article; zbMATH DE number 1487861 (Why is no real title available?)
• scientific article; zbMATH DE number 1487864 (Why is no real title available?)
• scientific article; zbMATH DE number 1538049 (Why is no real title available?)
• scientific article; zbMATH DE number 1759610 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 194916 (Why is no real title available?)
• scientific article; zbMATH DE number 201040 (Why is no real title available?)
• scientific article; zbMATH DE number 1863178 (Why is no real title available?)
• scientific article; zbMATH DE number 1903350 (Why is no real title available?)
• scientific article; zbMATH DE number 1905120 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• scientific article; zbMATH DE number 1390338 (Why is no real title available?)
• scientific article; zbMATH DE number 1446599 (Why is no real title available?)
• scientific article; zbMATH DE number 3245483 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A comparative study of various model-theoretic treatments of negation: A history of formal negation
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Binary Decision Diagrams
• Branching Programs and Binary Decision Diagrams
• Computer Aided Verification
• Computer Aided Verification
• Data structures for symbolic multi-valued model-checking
• Efficient detection of vacuity in temporal model checking
• Graph-Based Algorithms for Boolean Function Manipulation
• Model checking lattices: using and reasoning about information orders for abstraction
• Multi-valued model checking via classical model checking.
• SCTL-MUS: A formal methodology for software development of distributed systems. A case study
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(22)

• Computation tree logic model checking based on multi-valued possibility measures
• Fuzzy Halpern and Shoham's interval temporal logics
• Simulation for lattice-valued doubly labeled transition systems
• Model checking of linear-time properties in multi-valued systems
• Abstraction and approximation in fuzzy temporal logics and models
• Multi-valued model checking games
• scientific article; zbMATH DE number 1701772 (Why is no real title available?)
• Data structures for symbolic multi-valued model-checking
• scientific article; zbMATH DE number 1863178 (Why is no real title available?)
• Statistical Model Checking for Variability-Intensive Systems
• Multi-robot LTL planning under uncertainty
• Abstraction and abstraction refinement
• Model checking computation tree logic over finite lattices
• Integrating topological proofs with model checking to instrument iterative design
• Statistical model checking for variability-intensive systems: applications to bug detection and minimization
• A verification-driven framework for iterative design of controllers
• A Direct Algorithm for Multi-valued Bounded Model Checking
• Quantitative \(\mu\)-calculus and CTL defined over constraint semirings
• TOrPEDO : witnessing model correctness with topological proofs
• Symbolic checking of fuzzy CTL on fuzzy program graph
• Quantitative model checking of linear-time properties based on generalized possibility measures
• Model checking fuzzy computation tree logic

Describes a project that uses

Uses Software

• NuSMV
• SLAM
• SCTL-MUS

This page was built for publication: Data structures for symbolic multi-valued model-checking

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