-
Previous Article
Optimal control of an HIV model with CTL cells and latently infected cells
- NACO Home
- This Issue
-
Next Article
Quadratic optimization with two ball constraints
June
2020, 10(2): 177-206.
doi: 10.3934/naco.2019047
Formal analysis of the Schulz matrix inversion algorithm: A paradigm towards computer aided verification of general matrix flow solvers
United Technologies Research Center Ltd., 2nd Floor Penrose Wharf Business Centre, Penrose Quay, Cork, T23 XN53, Ireland |
This paper pilots Schulz generalised matrix inverse algorithm as a paradigm in demonstrating how computer aided reachability analysis and theoretical numerical analysis can be combined effectively in developing verification methodologies and tools for matrix iterative solvers. It is illustrated how algorithmic convergence to computed solutions with required accuracy is mathematically quantified and used within computer aided reachability analysis tools to formally verify convergence over predefined sets of multiple problem data. In addition, some numerical analysis results are used to form computational reliability monitors to escort the algorithm on-line and monitor the numerical performance, accuracy and stability of the entire computational process. For making the paper self-contained, formal verification preliminaries and background on tools and approaches are reported together with the detailed numerical analysis in basic mathematical language. For demonstration purposes, a custom made reachability analysis program based on affine arithmetic is applied to numerical examples.
Keywords:
Matrix iterative algorithms,
Schulz algorithm,
Reachability analysis,
Formal verification.
Mathematics Subject Classification:
Primary: 65F20, 65F30; Secondary: 68Q45.
Citation:
Vassilios A. Tsachouridis, Georgios Giantamidis, Stylianos Basagiannis, Kostas Kouramas. Formal analysis of the Schulz matrix inversion algorithm: A paradigm towards computer aided verification of general matrix flow solvers. Numerical Algebra, Control and Optimization,
2020, 10
(2)
: 177-206.
doi: 10.3934/naco.2019047
![]()
References:
| [1] |
AAFLIB - An Affine Arithmetic C++, 2019. Available from: http://aaflib.sourceforge.net. |
| [2] |
R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine,
The algorithmic analysis of hybrid systems, Theoretical Computer Science, 138 (1995), 3-34.
doi: 10.1016/0304-3975(94)00202-T. |
| [3] |
R. Alur, T. A. Henzinger, G. Lafferriere and G. Pappas,
Discrete abstractions of hybrid systems, Proceedings of the IEEE 88, 7 (2000), 971-984.
|
| [4] |
R. Alur, T. Dang and F. Ivancic,
Counter example-guided predicate abstraction of hybrid systems, Theoretical Computer Science, 354 (2006), 250-271.
doi: 10.1016/j.tcs.2005.11.026. |
| [5] |
Y. Annapureddy, C. Liu, G. Fainekos and S. Sankaranarayanan, S-TaLiRo: A tool for temporal logic falsification for hybrid systems, Proc. of Tools and Algorithms for the Construction and Analysis of Systems, (2011), 254–257. |
| [6] |
E. Asarin, T. Dang and O. Maler, The d/dt tool for verification of hybrid systems, Int. Conf. on Computer Aided Verification, LNCS, Springer-Verlag, (2002), 365–350. |
| [7] |
A. Ben-Israel and D. Cohen,
On iterative computation of generalized inverses and associated projections, SIAM J. Numer. Anal., 3 (1966), 410-419.
doi: 10.1137/0703035. |
| [8] |
A. Ben-Israel and T. N. E. Greville, Generalized Inverses Theory and Applications, Springer, 2003, ISBN 978-0-387-00293-4. |
| [9] |
A. Bhatia and E. Frazzoli, Incremental search methods for reachability analysis of continuous and hybrid systems, Hybrid Systems: Computation and Control, LNCS, Springer-Verlag, 2993 (2004), 142–156. |
| [10] |
O. Botchkarev and S. Tripakis, Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations, Hybrid Systems: Computation and Control, LNCS, Springer-Verlag, 1790 (2000), 73–78. |
| [11] |
M. S. Branicky, M. M. Curtiss, J. Levine and S. Morgan,
Sampling-based planning, control, and verification of hybrid systems, Control Theory and Applications, 153 (2006), 575-590.
|
| [12] |
C. Bu, X. Zhang, J. Zhou, W. Wang and Y. Wei,
The inverse, rank and product of tensors, Linear Algebra and Its Applications, 446 (2014), 269-280.
doi: 10.1016/j.laa.2013.12.015. |
| [13] |
X. Chen, E. Abraham and S. Sankaranarayanan, Flow* An analyzer for non-linear hybrid systems, Proc. of CAV13, LNCS, Springer, 8044 (2013), 258–263.
doi: 10.1007/978-3-642-39799-8_18. |
| [14] |
X. Chen, Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models, PhD Thesis in RWTH Aachen University, Germany, 2015. |
| [15] |
C. Chutinan and B. H. Krogh,
Computational techniques for hybrid system verification, IEEE Transactions on Automatic Control, 48 (2003), 64-75.
doi: 10.1109/TAC.2002.806655. |
| [16] |
E. M Clarke, W. Klieber, M. Novcek and P. Zuliani, Model checking and the state explosion problem, Tools for Practical Software Verification, Springer, (2012), 1–30. |
| [17] |
E. M. Clarke, Th. A. Henzinger, H. Veith and R. Bloem, Handbook of Model Checking, Springer International Publishing, 2018.
doi: 10.1007/978-3-319-10575-8. |
| [18] |
J-J. Climent, N. Thome and Y. Wei,
A geometrical approach on generalized inverses by Neumann-type series, Linear Algebra and Its Applications, 1 (2001), 533-540.
doi: 10.1016/S0024-3795(01)00309-3. |
| [19] |
B. Datta, Numerical Methods for Linear Control Systems, Elsevier Academic Press, 2004.
|
| [20] |
M. Daumas, D. Lester and C. Muoz,
Verified real number calculations, A library for interval arithmetic, IEEE Transactions on Computers, 58 (2009), 226-237.
doi: 10.1109/TC.2008.213. |
| [21] |
A. Donze, Breach, a toolbox for verification and parameter synthesis of hybrid systems, Proc. of Computer Aided Verification, (2010), 167–170. |
| [22] |
P. Duggirala, S. Mitra, M. Viswanathan and M. Potok, C2E2 A verification tool for Stateflow models, Proc. of TACAS15, LNCS, Springer, 9035 (2015), 68–82. |
| [23] |
J. M. Esposito, J. Kim and V. Kumar, Adaptive RRTs for validating hybrid robotic control systems, Workshop on Algorithmic Foundations of Robotics, Zeist, Netherlands, (2004), 107–132. |
| [24] |
J. Kim, J. M. Esposito and V. Kumar, An RRT-based algorithm for testing and validating multi-robot controllers, Robotics: Science and Systems, Boston, MA, (2005), 249–256. |
| [25] |
L. H. de Figueiredo and J. Stolfi,
Affine arithmetic: concepts and applications, Numerical Algorithms, 37 (2004), 147-158.
doi: 10.1023/B:NUMA.0000049462.70970.b6. |
| [26] |
G. Frehse, C. L. Guernic, A. Donz, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang and O. Maler, SpaceEx Scalable verification of hybrid systems, Proc. of CAV11, LNCS, Springer, 6806 (2011), 379–395.
doi: 10.1007/978-3-642-22110-1_30. |
| [27] |
G. Frehse, R. Kateja and C. Le Guernic,
Flowpipe approximation and clustering in space-time, Proc. of HSCC13, 9035 (2013), 203-212.
doi: 10.1145/2461328.2461361. |
| [28] |
M. Gameiro and P. Manolios, Formally verifying an algorithm based on interval arithmetic for checking transversality, Workshop on ACL2 Prover and Applications, 2004. |
| [29] |
N. Giorgetti, G.J. Pappas and A. Bemporad, Bounded model checking for hybrid dynamical systems, IEEE Conference on Decision and Control, Seville, Spain, (2005), 672–677. |
| [30] |
C. Le Guernic, Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics, PhD Thesis in Universit Joseph-Fourier-Grenoble I, France, 2009. |
| [31] |
T. Henzinger, P. Kopke, A. Puri and P. Varaiya, What's decidable about hybrid automata?, ACM Symposium on Theory of Computing, (1995), 273–282.
doi: 10.1016/0895-7177(96)00072-6. |
| [32] |
T. Henzinger, The theory of hybrid automata, Symposium on Logic in Computer Science, (1996), 278–292.
doi: 10.1109/LICS.1996.561342. |
| [33] |
F. Immler, Tool presentation Isabelle/hol for reachability analysis of continuous systems, in ARCH14-15, 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems (eds. M. Frehse and M. Althoff), Academic Press, (1971), 33–75. EPiC Series in Computer Science, 34 (2015), 180–187. |
| [34] |
A. A. A. Julius, G. E. Fainekos, M. Anand, I. Lee and G. J. Pappas, IRobust test generation and coverage for hybrid systems, Hybrid Systems: Computation and Control, LNCS, Springer-Verlag, 4416 (2007), 329–342. |
| [35] |
S. Kong, S. Gao and W. Chen, Reachability analysis for hybrid systems, Proc. of TACAS15, LNCS, Springer, 9035 (2015), 200–205. |
| [36] |
M. Konstantinov, D. Gu, V. Mehrmann and P. Petkov, Perturbation Theory for Matrix Equations, 2$^{nd}$ edition, Elsevier, Amsterdam, 2003, ISBN-9780444513151. |
| [37] |
G. A. Kumar, T. V. Subbareddy, B. M. Redd, N. Raju and V. Elamaran,
An approach to design a matrix inversion hardware module using FPGA, Int. Conf. on Control, Instrumentation, Comm. and Comput. Technologies, 230 (2014), 87-90.
|
| [38] |
G. Lafferriere, G. Pappas and S. Yovine,
A new class of decidable hybrid systems, Hybrid Systems: Computation and Control, LNCS, 1569 (1999), 137-151.
|
| [39] |
LAPACK-Linear Algebra PACKage, 2019. Available from: http://www.netlib.org/lapack/. |
| [40] |
W. Levine, The Control Handbook, IEEE Press, 1996. |
| [41] |
C. Livadas and N. Lynch,
A new class of decidable hybrid systems, Hybrid Systems: Computation and Control, LNCS, 1386 (1998), 253-272.
|
| [42] |
Matlab-Mathworks, 2019. Available from: https://www.mathworks.com |
| [43] |
F. Messine and A. Touhami,
A general reliable quadratic form: an extension of affine arithmetic, Reliable Computing, 12 (2006), 171-192.
doi: 10.1007/s11155-006-7217-4. |
| [44] |
D. Monniaux, Toward verifiably correct control implementations, The impact of control technology Part 2: Challenges for control research, Report of IEEE Control Systems Society, 2nd Ed, 2011. Available from: http://ieeecss.org/general/IoCT2-report. |
| [45] |
D. Monniaux and A. Mine, Verification of control system software, the impact of control technology, Part 1: Success stories for control, Report of IEEE Control Systems Society, 2nd Ed, 2011. Available from: http://ieeecss.org/general/IoCT2-report. |
| [46] |
R. E. Moore, Methods and Applications of Interval Analysis, SIAM Studies in Applied and Numerical Mathematics, Philadelphia, 1987, ISBN-10: 0898711614. |
| [47] |
R. E. Moore, R. B. Kearfott and M. J. Cloud, Introduction to Interval Analysis, SIAM, 2009.
doi: 10.1137/1.9780898717716. |
| [48] |
C. Munoz and D. Lester, Real number calculations and theorem proving, 18th Int. Conf. on Theorem Proving in Higher Order Logics, England, (2005), 239–254.
doi: 10.1007/11541868_13. |
| [49] |
T. Nahhal and T. Dang,
Test coverage for continuous and hybrid systems, Int. Conf. on Computer Aided Verification, LNCS, 4590 (2007), 449-462.
|
| [50] |
I. Pasca, Formal Verifcation for Numerical Methods, PhD Thesis in Universit Nice Sophia Antipolis, France, 2010. |
| [51] |
P. Petkov, M. Konstantinov and N. Christov, Computational Methods for Linear Control Systems, 2$^{nd}$ edition, Prentice- Hall, Hemel Hempstead, 1991, ISBN-9780444513151. |
| [52] |
M. D. Petkovic and P. S. Stanimirovic,
Generalized matrix inversion is not harder than matrix multiplication, J. Comput. and Applied Math., 230 (2009), 270-282.
doi: 10.1016/j.cam.2008.11.012. |
| [53] |
M. D. Petkovic and P. S. Stanimirovic,
Iterative method for computing Moore-Penrose inverse based on Penrose equations, J. Comput. and Applied Math., 235 (2011), 1604-1613.
doi: 10.1016/j.cam.2010.08.042. |
| [54] |
M. S. Petkovic,
Iterative methods for bounding the inverse of a matrix (a survey), FILOMAT Nis, Algebra Logic & Discrete Mathematics, 9 (1995), 543-577.
|
| [55] |
E. Plaku, L. Kavraki and M. Vardi,
Hybrid systems: from verification to falsification by combining motion planning and discrete search, Formal Methods in System Design, 34 (2009), 157-182.
|
| [56] |
A. Platzer and J-D Quesel, KeYmaera a hybrid theorem prover for hybrid systems (system description), Automated Reasoning, IJCAR 2008, Lecture Notes in Computer Science (eds. M. Frehse and M. AlthoffArmando A., Baumgartner P., Dowek G.), Springer Berlin Heidelberg, 5195 (2008), 163–183.
doi: 10.1007/978-3-540-71070-7_15. |
| [57] |
A. Puri, Theory of Hybrid Systems and Discrete Event Systems, PhD Thesis in University of California, Berkeley, 1995. |
| [58] |
PyInterval - Interval arithmetic in Python, 2019. Available from: https://github.com/taschini/pyinterval |
| [59] |
S. Qiao, X. Wang and Y. Wei,
Two finite-time convergent Zhang neural network models for time-varying complex matrix Drazin inverse, Linear Algebra and Its Applications, 542 (2018), 101-117.
doi: 10.1016/j.laa.2017.03.014. |
| [60] |
Y. Rahman, A. Xie and S. Bernstein, Retrospective cost adaptive control: pole placement, frequency response, and connections with LQG control, IEEE Control System Magazine, (2017), 28–69.
doi: 10.1109/MCS.2017.2718825. |
| [61] |
S. Ratschan and Z. She, Safety verification of hybrid systems by constraint propagation based abstraction refinement, ACM Transactions on Embedded Computing Systems, 6 (2007), Article No. 8.
doi: 10.1145/1210268.1210276. |
| [62] |
RTCA Formal Methods Supplement to DO-178C and DO-278A, RTCA DO-333, December 13, 2011. |
| [63] |
RTCA, Software Considerations in Airborne Systems and Equipment Certification, RTCA DO-178C, December 13, 2011. |
| [64] |
S. Schupp, E. Abraham, X. Chen, I. B. Makhlouf, G. Frehse, S. Sankaranarayanan and S. Kowalewski, Current challenges in the verification of hybrid systems, Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, (2015), 8–24. |
| [65] |
S. Schupp and E. Abraham, Efficient dynamic error reduction for hybrid systems reachability analysis, Proc. of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS18, LNCS, Springer, 2018. |
| [66] |
B. I. Silva and B. H. Krogh, Formal verification of hybrid systems using CheckMate: A case study, American Control Conference, (2000), 1679–1683. |
| [67] |
G. Stewart and J. Sun, Matrix Perturbation Theory, Academic Press, New York, 1990. |
| [68] |
O. Stursberg and B. H. Krogh,
Efficient representation and computation of reachable sets for hybrid systems, Hybrid Systems: Computation and Control, LNCS, 2623 (2003), 482-497.
|
| [69] |
C. J. Tomlin, I. Mitchell, A. Bayen and M. Oishi, Computational techniques for the verification and control of hybrid systems, Proceedings of the IEEE 91, Springer-Verlag, 7 (2003), 986–1001. |
| [70] |
V. A. Tsachouridis,
Numerical analysis of $H_{\infty} $ filter for system parameter identification, Int. J. Modelling, Identification and Control, 30 (2018), 163-183.
|
| [71] |
University of Florida Sparse Matrix Collection, 2019. Available from: https://www.cise.ufl.edu/research/sparse/matrices/list_by_id.html |
| [72] |
G. Wang, Y. Wei and S. Qiao, Generalized Inverses: Theory and Computations, Springer, Singapore: Science Press Beijing, Beijing, 2018.
doi: 10.1007/978-981-13-0146-9. |
| [73] |
Y. Wei, P. Stanimirovic and M. Petkovic, Numerical and Symbolic Computations of Generalized Inverses, World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2018. |
| [74] |
J. Wilkinson, Rounding Errors in Algebraic Processes, Prentice Hall, Englewood Cliff, NJ, 1963. |
| [75] |
H. Wolkovicz and G. P. H. Stayan,
Bounds for eigenvalues using traces, Linear Algebra and Its Applications, 29 (1980), 471-506.
doi: 10.1016/0024-3795(80)90258-X. |
| [76] |
P. Xie, H. Xiang and Y. Wei, Randomized algorithms for total least squares problems, Numerical Linear Algebra with Applications, 26 (2019), e2219, Available from: https://doi.org/10.1002/nla.2219
doi: 10.1002/nla.2219. |
show all references
References:
| [1] |
AAFLIB - An Affine Arithmetic C++, 2019. Available from: http://aaflib.sourceforge.net. |
| [2] |
R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine,
The algorithmic analysis of hybrid systems, Theoretical Computer Science, 138 (1995), 3-34.
doi: 10.1016/0304-3975(94)00202-T. |
| [3] |
R. Alur, T. A. Henzinger, G. Lafferriere and G. Pappas,
Discrete abstractions of hybrid systems, Proceedings of the IEEE 88, 7 (2000), 971-984.
|
| [4] |
R. Alur, T. Dang and F. Ivancic,
Counter example-guided predicate abstraction of hybrid systems, Theoretical Computer Science, 354 (2006), 250-271.
doi: 10.1016/j.tcs.2005.11.026. |
| [5] |
Y. Annapureddy, C. Liu, G. Fainekos and S. Sankaranarayanan, S-TaLiRo: A tool for temporal logic falsification for hybrid systems, Proc. of Tools and Algorithms for the Construction and Analysis of Systems, (2011), 254–257. |
| [6] |
E. Asarin, T. Dang and O. Maler, The d/dt tool for verification of hybrid systems, Int. Conf. on Computer Aided Verification, LNCS, Springer-Verlag, (2002), 365–350. |
| [7] |
A. Ben-Israel and D. Cohen,
On iterative computation of generalized inverses and associated projections, SIAM J. Numer. Anal., 3 (1966), 410-419.
doi: 10.1137/0703035. |
| [8] |
A. Ben-Israel and T. N. E. Greville, Generalized Inverses Theory and Applications, Springer, 2003, ISBN 978-0-387-00293-4. |
| [9] |
A. Bhatia and E. Frazzoli, Incremental search methods for reachability analysis of continuous and hybrid systems, Hybrid Systems: Computation and Control, LNCS, Springer-Verlag, 2993 (2004), 142–156. |
| [10] |
O. Botchkarev and S. Tripakis, Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations, Hybrid Systems: Computation and Control, LNCS, Springer-Verlag, 1790 (2000), 73–78. |
| [11] |
M. S. Branicky, M. M. Curtiss, J. Levine and S. Morgan,
Sampling-based planning, control, and verification of hybrid systems, Control Theory and Applications, 153 (2006), 575-590.
|
| [12] |
C. Bu, X. Zhang, J. Zhou, W. Wang and Y. Wei,
The inverse, rank and product of tensors, Linear Algebra and Its Applications, 446 (2014), 269-280.
doi: 10.1016/j.laa.2013.12.015. |
| [13] |
X. Chen, E. Abraham and S. Sankaranarayanan, Flow* An analyzer for non-linear hybrid systems, Proc. of CAV13, LNCS, Springer, 8044 (2013), 258–263.
doi: 10.1007/978-3-642-39799-8_18. |
| [14] |
X. Chen, Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models, PhD Thesis in RWTH Aachen University, Germany, 2015. |
| [15] |
C. Chutinan and B. H. Krogh,
Computational techniques for hybrid system verification, IEEE Transactions on Automatic Control, 48 (2003), 64-75.
doi: 10.1109/TAC.2002.806655. |
| [16] |
E. M Clarke, W. Klieber, M. Novcek and P. Zuliani, Model checking and the state explosion problem, Tools for Practical Software Verification, Springer, (2012), 1–30. |
| [17] |
E. M. Clarke, Th. A. Henzinger, H. Veith and R. Bloem, Handbook of Model Checking, Springer International Publishing, 2018.
doi: 10.1007/978-3-319-10575-8. |
| [18] |
J-J. Climent, N. Thome and Y. Wei,
A geometrical approach on generalized inverses by Neumann-type series, Linear Algebra and Its Applications, 1 (2001), 533-540.
doi: 10.1016/S0024-3795(01)00309-3. |
| [19] |
B. Datta, Numerical Methods for Linear Control Systems, Elsevier Academic Press, 2004.
|
| [20] |
M. Daumas, D. Lester and C. Muoz,
Verified real number calculations, A library for interval arithmetic, IEEE Transactions on Computers, 58 (2009), 226-237.
doi: 10.1109/TC.2008.213. |
| [21] |
A. Donze, Breach, a toolbox for verification and parameter synthesis of hybrid systems, Proc. of Computer Aided Verification, (2010), 167–170. |
| [22] |
P. Duggirala, S. Mitra, M. Viswanathan and M. Potok, C2E2 A verification tool for Stateflow models, Proc. of TACAS15, LNCS, Springer, 9035 (2015), 68–82. |
| [23] |
J. M. Esposito, J. Kim and V. Kumar, Adaptive RRTs for validating hybrid robotic control systems, Workshop on Algorithmic Foundations of Robotics, Zeist, Netherlands, (2004), 107–132. |
| [24] |
J. Kim, J. M. Esposito and V. Kumar, An RRT-based algorithm for testing and validating multi-robot controllers, Robotics: Science and Systems, Boston, MA, (2005), 249–256. |
| [25] |
L. H. de Figueiredo and J. Stolfi,
Affine arithmetic: concepts and applications, Numerical Algorithms, 37 (2004), 147-158.
doi: 10.1023/B:NUMA.0000049462.70970.b6. |
| [26] |
G. Frehse, C. L. Guernic, A. Donz, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang and O. Maler, SpaceEx Scalable verification of hybrid systems, Proc. of CAV11, LNCS, Springer, 6806 (2011), 379–395.
doi: 10.1007/978-3-642-22110-1_30. |
| [27] |
G. Frehse, R. Kateja and C. Le Guernic,
Flowpipe approximation and clustering in space-time, Proc. of HSCC13, 9035 (2013), 203-212.
doi: 10.1145/2461328.2461361. |
| [28] |
M. Gameiro and P. Manolios, Formally verifying an algorithm based on interval arithmetic for checking transversality, Workshop on ACL2 Prover and Applications, 2004. |
| [29] |
N. Giorgetti, G.J. Pappas and A. Bemporad, Bounded model checking for hybrid dynamical systems, IEEE Conference on Decision and Control, Seville, Spain, (2005), 672–677. |
| [30] |
C. Le Guernic, Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics, PhD Thesis in Universit Joseph-Fourier-Grenoble I, France, 2009. |
| [31] |
T. Henzinger, P. Kopke, A. Puri and P. Varaiya, What's decidable about hybrid automata?, ACM Symposium on Theory of Computing, (1995), 273–282.
doi: 10.1016/0895-7177(96)00072-6. |
| [32] |
T. Henzinger, The theory of hybrid automata, Symposium on Logic in Computer Science, (1996), 278–292.
doi: 10.1109/LICS.1996.561342. |
| [33] |
F. Immler, Tool presentation Isabelle/hol for reachability analysis of continuous systems, in ARCH14-15, 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems (eds. M. Frehse and M. Althoff), Academic Press, (1971), 33–75. EPiC Series in Computer Science, 34 (2015), 180–187. |
| [34] |
A. A. A. Julius, G. E. Fainekos, M. Anand, I. Lee and G. J. Pappas, IRobust test generation and coverage for hybrid systems, Hybrid Systems: Computation and Control, LNCS, Springer-Verlag, 4416 (2007), 329–342. |
| [35] |
S. Kong, S. Gao and W. Chen, Reachability analysis for hybrid systems, Proc. of TACAS15, LNCS, Springer, 9035 (2015), 200–205. |
| [36] |
M. Konstantinov, D. Gu, V. Mehrmann and P. Petkov, Perturbation Theory for Matrix Equations, 2$^{nd}$ edition, Elsevier, Amsterdam, 2003, ISBN-9780444513151. |
| [37] |
G. A. Kumar, T. V. Subbareddy, B. M. Redd, N. Raju and V. Elamaran,
An approach to design a matrix inversion hardware module using FPGA, Int. Conf. on Control, Instrumentation, Comm. and Comput. Technologies, 230 (2014), 87-90.
|
| [38] |
G. Lafferriere, G. Pappas and S. Yovine,
A new class of decidable hybrid systems, Hybrid Systems: Computation and Control, LNCS, 1569 (1999), 137-151.
|
| [39] |
LAPACK-Linear Algebra PACKage, 2019. Available from: http://www.netlib.org/lapack/. |
| [40] |
W. Levine, The Control Handbook, IEEE Press, 1996. |
| [41] |
C. Livadas and N. Lynch,
A new class of decidable hybrid systems, Hybrid Systems: Computation and Control, LNCS, 1386 (1998), 253-272.
|
| [42] |
Matlab-Mathworks, 2019. Available from: https://www.mathworks.com |
| [43] |
F. Messine and A. Touhami,
A general reliable quadratic form: an extension of affine arithmetic, Reliable Computing, 12 (2006), 171-192.
doi: 10.1007/s11155-006-7217-4. |
| [44] |
D. Monniaux, Toward verifiably correct control implementations, The impact of control technology Part 2: Challenges for control research, Report of IEEE Control Systems Society, 2nd Ed, 2011. Available from: http://ieeecss.org/general/IoCT2-report. |
| [45] |
D. Monniaux and A. Mine, Verification of control system software, the impact of control technology, Part 1: Success stories for control, Report of IEEE Control Systems Society, 2nd Ed, 2011. Available from: http://ieeecss.org/general/IoCT2-report. |
| [46] |
R. E. Moore, Methods and Applications of Interval Analysis, SIAM Studies in Applied and Numerical Mathematics, Philadelphia, 1987, ISBN-10: 0898711614. |
| [47] |
R. E. Moore, R. B. Kearfott and M. J. Cloud, Introduction to Interval Analysis, SIAM, 2009.
doi: 10.1137/1.9780898717716. |
| [48] |
C. Munoz and D. Lester, Real number calculations and theorem proving, 18th Int. Conf. on Theorem Proving in Higher Order Logics, England, (2005), 239–254.
doi: 10.1007/11541868_13. |
| [49] |
T. Nahhal and T. Dang,
Test coverage for continuous and hybrid systems, Int. Conf. on Computer Aided Verification, LNCS, 4590 (2007), 449-462.
|
| [50] |
I. Pasca, Formal Verifcation for Numerical Methods, PhD Thesis in Universit Nice Sophia Antipolis, France, 2010. |
| [51] |
P. Petkov, M. Konstantinov and N. Christov, Computational Methods for Linear Control Systems, 2$^{nd}$ edition, Prentice- Hall, Hemel Hempstead, 1991, ISBN-9780444513151. |
| [52] |
M. D. Petkovic and P. S. Stanimirovic,
Generalized matrix inversion is not harder than matrix multiplication, J. Comput. and Applied Math., 230 (2009), 270-282.
doi: 10.1016/j.cam.2008.11.012. |
| [53] |
M. D. Petkovic and P. S. Stanimirovic,
Iterative method for computing Moore-Penrose inverse based on Penrose equations, J. Comput. and Applied Math., 235 (2011), 1604-1613.
doi: 10.1016/j.cam.2010.08.042. |
| [54] |
M. S. Petkovic,
Iterative methods for bounding the inverse of a matrix (a survey), FILOMAT Nis, Algebra Logic & Discrete Mathematics, 9 (1995), 543-577.
|
| [55] |
E. Plaku, L. Kavraki and M. Vardi,
Hybrid systems: from verification to falsification by combining motion planning and discrete search, Formal Methods in System Design, 34 (2009), 157-182.
|
| [56] |
A. Platzer and J-D Quesel, KeYmaera a hybrid theorem prover for hybrid systems (system description), Automated Reasoning, IJCAR 2008, Lecture Notes in Computer Science (eds. M. Frehse and M. AlthoffArmando A., Baumgartner P., Dowek G.), Springer Berlin Heidelberg, 5195 (2008), 163–183.
doi: 10.1007/978-3-540-71070-7_15. |
| [57] |
A. Puri, Theory of Hybrid Systems and Discrete Event Systems, PhD Thesis in University of California, Berkeley, 1995. |
| [58] |
PyInterval - Interval arithmetic in Python, 2019. Available from: https://github.com/taschini/pyinterval |
| [59] |
S. Qiao, X. Wang and Y. Wei,
Two finite-time convergent Zhang neural network models for time-varying complex matrix Drazin inverse, Linear Algebra and Its Applications, 542 (2018), 101-117.
doi: 10.1016/j.laa.2017.03.014. |
| [60] |
Y. Rahman, A. Xie and S. Bernstein, Retrospective cost adaptive control: pole placement, frequency response, and connections with LQG control, IEEE Control System Magazine, (2017), 28–69.
doi: 10.1109/MCS.2017.2718825. |
| [61] |
S. Ratschan and Z. She, Safety verification of hybrid systems by constraint propagation based abstraction refinement, ACM Transactions on Embedded Computing Systems, 6 (2007), Article No. 8.
doi: 10.1145/1210268.1210276. |
| [62] |
RTCA Formal Methods Supplement to DO-178C and DO-278A, RTCA DO-333, December 13, 2011. |
| [63] |
RTCA, Software Considerations in Airborne Systems and Equipment Certification, RTCA DO-178C, December 13, 2011. |
| [64] |
S. Schupp, E. Abraham, X. Chen, I. B. Makhlouf, G. Frehse, S. Sankaranarayanan and S. Kowalewski, Current challenges in the verification of hybrid systems, Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, (2015), 8–24. |
| [65] |
S. Schupp and E. Abraham, Efficient dynamic error reduction for hybrid systems reachability analysis, Proc. of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS18, LNCS, Springer, 2018. |
| [66] |
B. I. Silva and B. H. Krogh, Formal verification of hybrid systems using CheckMate: A case study, American Control Conference, (2000), 1679–1683. |
| [67] |
G. Stewart and J. Sun, Matrix Perturbation Theory, Academic Press, New York, 1990. |
| [68] |
O. Stursberg and B. H. Krogh,
Efficient representation and computation of reachable sets for hybrid systems, Hybrid Systems: Computation and Control, LNCS, 2623 (2003), 482-497.
|
| [69] |
C. J. Tomlin, I. Mitchell, A. Bayen and M. Oishi, Computational techniques for the verification and control of hybrid systems, Proceedings of the IEEE 91, Springer-Verlag, 7 (2003), 986–1001. |
| [70] |
V. A. Tsachouridis,
Numerical analysis of $H_{\infty} $ filter for system parameter identification, Int. J. Modelling, Identification and Control, 30 (2018), 163-183.
|
| [71] |
University of Florida Sparse Matrix Collection, 2019. Available from: https://www.cise.ufl.edu/research/sparse/matrices/list_by_id.html |
| [72] |
G. Wang, Y. Wei and S. Qiao, Generalized Inverses: Theory and Computations, Springer, Singapore: Science Press Beijing, Beijing, 2018.
doi: 10.1007/978-981-13-0146-9. |
| [73] |
Y. Wei, P. Stanimirovic and M. Petkovic, Numerical and Symbolic Computations of Generalized Inverses, World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2018. |
| [74] |
J. Wilkinson, Rounding Errors in Algebraic Processes, Prentice Hall, Englewood Cliff, NJ, 1963. |
| [75] |
H. Wolkovicz and G. P. H. Stayan,
Bounds for eigenvalues using traces, Linear Algebra and Its Applications, 29 (1980), 471-506.
doi: 10.1016/0024-3795(80)90258-X. |
| [76] |
P. Xie, H. Xiang and Y. Wei, Randomized algorithms for total least squares problems, Numerical Linear Algebra with Applications, 26 (2019), e2219, Available from: https://doi.org/10.1002/nla.2219
doi: 10.1002/nla.2219. |
Figure 4.
Affine arithmetic approach for bound convergence expression (34) for a $ 2 \times 2 $ interval matrix
Figure 5.
Affine arithmetic approach for bound convergence expression (34) for a $ 2 \times 3 $ interval matrix
Figure 7.
$ 43 \times 68 $ matrix lpkb2 University of Florida sparse matrix collection
Figure 8.
$ 43 \times 68 $ matrix example in Breach
Figure 9.
Computational reliability monitor for $ 43 \times 68 $ matrix Example 6
| [1] |
Lingling Lv, Zhe Zhang, Lei Zhang, Weishu Wang. An iterative algorithm for periodic sylvester matrix equations. Journal of Industrial and Management Optimization, 2018, 14 (1) : 413-425. doi: 10.3934/jimo.2017053 |
| [2] |
Ai-Guo Wu, Ying Zhang, Hui-Jie Sun. Parametric Smith iterative algorithms for discrete Lyapunov matrix equations. Journal of Industrial and Management Optimization, 2020, 16 (6) : 3047-3063. doi: 10.3934/jimo.2019093 |
| [3] |
Yan Tang. Convergence analysis of a new iterative algorithm for solving split variational inclusion problems. Journal of Industrial and Management Optimization, 2020, 16 (2) : 945-964. doi: 10.3934/jimo.2018187 |
| [4] |
Mikhail Gusev. On reachability analysis for nonlinear control systems with state constraints. Conference Publications, 2015, 2015 (special) : 579-587. doi: 10.3934/proc.2015.0579 |
| [5] |
Henry Adams, Lara Kassab, Deanna Needell. An adaptation for iterative structured matrix completion. Foundations of Data Science, 2021, 3 (4) : 769-791. doi: 10.3934/fods.2021028 |
| [6] |
Simai He, Min Li, Shuzhong Zhang, Zhi-Quan Luo. A nonconvergent example for the iterative water-filling algorithm. Numerical Algebra, Control and Optimization, 2011, 1 (1) : 147-150. doi: 10.3934/naco.2011.1.147 |
| [7] |
Fabián Crocce, Ernesto Mordecki. A non-iterative algorithm for generalized pig games. Journal of Dynamics and Games, 2018, 5 (4) : 331-341. doi: 10.3934/jdg.2018020 |
| [8] |
Matthew M. Dunlop, Andrew M. Stuart. The Bayesian formulation of EIT: Analysis and algorithms. Inverse Problems and Imaging, 2016, 10 (4) : 1007-1036. doi: 10.3934/ipi.2016030 |
| [9] |
Victor Kozyakin. Iterative building of Barabanov norms and computation of the joint spectral radius for matrix sets. Discrete and Continuous Dynamical Systems - B, 2010, 14 (1) : 143-158. doi: 10.3934/dcdsb.2010.14.143 |
| [10] |
Sanming Liu, Zhijie Wang, Chongyang Liu. Proximal iterative Gaussian smoothing algorithm for a class of nonsmooth convex minimization problems. Numerical Algebra, Control and Optimization, 2015, 5 (1) : 79-89. doi: 10.3934/naco.2015.5.79 |
| [11] |
Justyna Jarczyk, Witold Jarczyk. Gaussian iterative algorithm and integrated automorphism equation for random means. Discrete and Continuous Dynamical Systems, 2020, 40 (12) : 6837-6844. doi: 10.3934/dcds.2020135 |
| [12] |
Xin Li, Ziguan Cui, Linhui Sun, Guanming Lu, Debnath Narayan. Research on iterative repair algorithm of Hyperchaotic image based on support vector machine. Discrete and Continuous Dynamical Systems - S, 2019, 12 (4&5) : 1199-1218. doi: 10.3934/dcdss.2019083 |
| [13] |
Xin Du, M. Monir Uddin, A. Mostakim Fony, Md. Tanzim Hossain, Md. Nazmul Islam Shuzan. Iterative Rational Krylov Algorithms for model reduction of a class of constrained structural dynamic system with Engineering applications. Numerical Algebra, Control and Optimization, 2021 doi: 10.3934/naco.2021016 |
| [14] |
Patrick Ballard, Bernadette Miara. Formal asymptotic analysis of elastic beams and thin-walled beams: A derivation of the Vlassov equations and their generalization to the anisotropic heterogeneous case. Discrete and Continuous Dynamical Systems - S, 2019, 12 (6) : 1547-1588. doi: 10.3934/dcdss.2019107 |
| [15] |
Yitong Guo, Bingo Wing-Kuen Ling. Principal component analysis with drop rank covariance matrix. Journal of Industrial and Management Optimization, 2021, 17 (5) : 2345-2366. doi: 10.3934/jimo.2020072 |
| [16] |
Ningyu Sha, Lei Shi, Ming Yan. Fast algorithms for robust principal component analysis with an upper bound on the rank. Inverse Problems and Imaging, 2021, 15 (1) : 109-128. doi: 10.3934/ipi.2020067 |
| [17] |
Sie Long Kek, Mohd Ismail Abd Aziz, Kok Lay Teo, Rohanin Ahmad. An iterative algorithm based on model-reality differences for discrete-time nonlinear stochastic optimal control problems. Numerical Algebra, Control and Optimization, 2013, 3 (1) : 109-125. doi: 10.3934/naco.2013.3.109 |
| [18] |
Kazeem Olalekan Aremu, Chinedu Izuchukwu, Grace Nnenanya Ogwo, Oluwatosin Temitope Mewomo. Multi-step iterative algorithm for minimization and fixed point problems in p-uniformly convex metric spaces. Journal of Industrial and Management Optimization, 2021, 17 (4) : 2161-2180. doi: 10.3934/jimo.2020063 |
| [19] |
Heping Dong, Deyue Zhang, Yukun Guo. A reference ball based iterative algorithm for imaging acoustic obstacle from phaseless far-field data. Inverse Problems and Imaging, 2019, 13 (1) : 177-195. doi: 10.3934/ipi.2019010 |
| [20] |
Ya-Zheng Dang, Zhong-Hui Xue, Yan Gao, Jun-Xiang Li. Fast self-adaptive regularization iterative algorithm for solving split feasibility problem. Journal of Industrial and Management Optimization, 2020, 16 (4) : 1555-1569. doi: 10.3934/jimo.2019017 |
Impact Factor:
Tools
Metrics
Other articles
by authors
[Back to Top]