A design of GPU-based quantitative model checking

DOI10.1007/978-3-030-67067-2_20zbMath1472.68091OpenAlexW3119058056MaRDI QIDQ2234091

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

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

Cites Work

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

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