Model checking linear dynamical systems under floating-point rounding

DOI10.1007/978-3-031-30823-9_3MaRDI QIDQ6535340zbMATH OpenFDO

Authors Engel Lefaucheux, Joël Ouaknine, David Purser, Mohammadamin Sharifi

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

dynamical systemsmodel checkingfloating-point arithmetic

Mathematics Subject Classification ID

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

Recommendations

• What's decidable about discrete linear dynamical systems?
• Correct probabilistic model checking with floating-point arithmetic
• Reachability in Linear Dynamical Systems
• On the linear ranking problem for simple floating-point loops
• Reflections on termination of linear loops

Cites work

• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• scientific article; zbMATH DE number 7724207 (Why is no real title available?)
• A two-phase approach for conditional floating-point verification
• Algebraic model checking for discrete linear dynamical systems
• Combining tools for optimization and analysis of floating-point computations
• Computer Aided Verification
• Deductive verification of floating-point Java programs in KeY
• On robustness for the Skolem and positivity problems
• On the complexity of the orbit problem
• Parameter synthesis for parametric probabilistic dynamical systems and prefix-independent specifications
• Polynomial-time algorithm for the orbit problem
• Positivity problems for low-order linear recurrence sequences
• Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday
• Reachability problems for Markov chains
• Skolem meets schanuel
• Symbolic decision procedure for termination of linear programs
• Termination of Integer Linear Programs
• The pseudo-reachability problem for diagonalisable linear dynamical systems
• Wielandt's proof of the exponent inequality for primitive nonnegative matrices

Cited in

(2)

• New tools for localization of limit cycles in recursive block floating point systems
• Model verification in dynamics through strict upper error bounds

This page was built for publication: Model checking linear dynamical systems under floating-point rounding

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