Model checking linear dynamical systems under floating-point rounding
type: Item
instance of: scholarly article
title: Model checking linear dynamical systems under floating-point rounding
zbMATH Open document ID: 1543.68222
DOI: 10.1007/978-3-031-30823-9_3
author: Engel Lefaucheux
author: Joël Ouaknine
author: David Purser
author: Mohammadamin Sharifi
publication date: 2023-12-13T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N30
zbMATH DE Number: 7777298
zbMATH Keywords: model checking
zbMATH Keywords: floating-point arithmetic
zbMATH Keywords: dynamical systems
MaRDI profile type: Publication
cites work: Deductive verification of floating-point Java programs in KeY
cites work: Reachability problems for Markov chains
cites work: On robustness for the Skolem and positivity problems
cites work: Parameter synthesis for parametric probabilistic dynamical systems and prefix-independent specifications
cites work: Combining tools for optimization and analysis of floating-point computations
cites work: Skolem meets schanuel
cites work: Termination of Integer Linear Programs
cites work: On the Complexity of the Orbit Problem
cites work: Q6168448
cites work: The pseudo-reachability problem for diagonalisable linear dynamical systems
cites work: Polynomial-time algorithm for the orbit problem
cites work: Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday
cites work: A two-phase approach for conditional floating-point verification
cites work: Algebraic model checking for discrete linear dynamical systems
cites work: Q5590814
cites work: Positivity Problems for Low-Order Linear Recurrence Sequences
cites work: Wielandt's proof of the exponent inequality for primitive nonnegative matrices
cites work: Computer Aided Verification
cites work: Symbolic decision procedure for termination of linear programs
description: scientific article; zbMATH DE number 7777298