Formal analysis of piecewise affine systems through formula-guided refinement

DOI10.1016/J.AUTOMATICA.2012.09.027MaRDI QIDQ1939637zbMATH OpenFDO

Authors Boyan Yordanov, Jana Tůmová, I. Černá, J. Barnat, Calin Belta

Publication date 4 March 2013

Published in Automatica (Search for Journal in Brave)

zbMATH Keywords

verificationtemporal logicbiotechnologypiecewise linear analysis

Mathematics Subject Classification ID

Biochemistry, molecular biology (92C40) System identification (93B30)

Recommendations

• Formal Analysis of Discrete-Time Piecewise Affine Systems
• Reachability analysis of continuous-time piecewise affine systems
• On the complexity of bounded time and precision reachability for piecewise affine systems
• Efficient Conversion of Mixed Logical Dynamical Systems Into an Equivalent Piecewise Affine Form
• Hybrid Systems: Computation and Control
• An implicit representation for the analysis of piecewise affine discrete-time systems
• On the complexity of bounded time reachability for piecewise affine systems
• Formal methods for analysis of discrete systems using a specification language
• Canonical Forms of Generic Piecewise Linear Continuous Systems

Cited in

(6)

• \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems
• Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis
• Augmented finite transition systems as abstractions for control synthesis
• Distributed \(H_\infty\)-consensus filtering for piecewise discrete-time linear systems
• Compositional abstraction refinement for control synthesis
• Automated generation of dynamics-based runtime certificates for high-level control

Describes a project that uses

Uses Software

• FaPAS
• NuSMV

This page was built for publication: Formal analysis of piecewise affine systems through formula-guided refinement

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