A design of GPU-based quantitative model checking

DOI10.1007/978-3-030-67067-2_20zbMATH Open1472.68091OpenAlexW3119058056MaRDI QIDQ2234091FDOQ2234091

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

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

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)

Cites Work

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

Cited In (4)

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

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)