A bounded model checking technique for discrete-time nonlinear systems

DOI10.1007/978-3-031-43835-6_5MaRDI QIDQ6546447zbMATH OpenFDO

Authors YoungMin Kwon, Eun-Hee Kim, Gul A. Agha

Publication date 29 May 2024

Full work available at URL https://doi.org/10.1007/978-3-031-43835-6_5

Mathematics Subject Classification ID

System identification (93B30) Nonlinear systems in control theory (93C10) Discrete-time control/observation systems (93C55)

Recommendations

• scientific article; zbMATH DE number 1903367
• scientific article; zbMATH DE number 1956650
• Formal Methods for Control of Nonlinear Systems
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• Automated Technology for Verification and Analysis

Cites work

• A design of GPU-based quantitative model checking
• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• A theory of timed automata
• Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems
• Bounded Model Checking of Hybrid Systems for Control
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• Generalized predictive control. I: The basic algorithm
• scientific article; zbMATH DE number 439900 (Why is no real title available?)
• scientific article; zbMATH DE number 3709074 (Why is no real title available?)
• scientific article; zbMATH DE number 53595 (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 5585443 (Why is no real title available?)
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Linear Time Logic Control of Discrete-Time Linear Systems
• STL model checking of continuous and hybrid systems
• Synthesis of Reactive Switching Protocols From Temporal Logic Specifications
• Uppaal in a nutshell

This page was built for publication: A bounded model checking technique for discrete-time nonlinear systems

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