Model checking linear dynamical systems under floating-point rounding

DOI10.1007/978-3-031-30823-9_3zbMATH Open1543.68222MaRDI QIDQ6535340FDOQ6535340

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

Publication date: 13 December 2023

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

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)

Cites Work

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

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)