A design of GPU-based quantitative model checking

DOI10.1007/978-3-030-67067-2_20MaRDI QIDQ2234091zbMATHOpenAlexFDO

Authors YoungMin Kwon, Eun-Hee Kim

Publication date 18 October 2021

Full work available at URL https://doi.org/10.1007/978-3-030-67067-2_20

zbMATH Keywords

GPU programmingLTLCquantitative model checking

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• CUDA accelerated LTL model checking -- revisited
• Model checking probabilistic systems
• Quantitative Model Checking for a Controller Design
• LTL Generalized Model Checking Revisited
• Quantitative approach for linear temporal logic based on DTMC

Cites work

• scientific article; zbMATH DE number 3770836 (Why is no real title available?)
• scientific article; zbMATH DE number 2005717 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 3997612 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• A new polynomial-time algorithm for linear programming
• A theory of timed automata
• Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems
• BFS-based model checking of linear-time properties with an application on GPUs
• Bounded Model Checking of Hybrid Systems for Control
• Constrained receding-horizon predictive control
• Generalized predictive control. II: Extensions and interpretations
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• LTLC: Linear Temporal Logic for Control
• Synthesis of Reactive Switching Protocols From Temporal Logic Specifications
• Uppaal in a nutshell

Cited in

(4)

• Quantitative Model Checking for a Controller Design
• CUDA accelerated LTL model checking -- revisited
• A bounded model checking technique for discrete-time nonlinear systems
• Implementing a CTL model checker with \(\mu \mathcal{G}\), a language for programming graph neural networks

This page was built for publication: A design of GPU-based quantitative model checking

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