Formal analysis of the Schulz matrix inversion algorithm: A paradigm towards computer aided verification of general matrix flow solvers

Vassilios A. Tsachouridis; Georgios Giantamidis; Stylianos Basagiannis; Kostas Kouramas

doi:10.3934/naco.2019047

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

Vassilios A. Tsachouridis ^, , Georgios Giantamidis ^**, , Stylianos Basagiannis and Kostas Kouramas

United Technologies Research Center Ltd., 2nd Floor Penrose Wharf Business Centre, Penrose Quay, Cork, T23 XN53, Ireland

^* Corresponding author: Vassilios A. Tsachouridis (tsachov@utrc.utc.com)

^** Also with Aalto University, Finland

Received January 2019 Revised July 2019 Published September 2019

Fund Project: This work was supported by the Irish Development Agency (IDA) under the program "Network of Excellence in Aerospace Cyber-Physical Systems", 2015-2019

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 & 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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[8]	A. Ben-Israel and T. N. E. Greville, Generalized Inverses Theory and Applications, Springer, 2003, ISBN 978-0-387-00293-4. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[14]	X. Chen, Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models, PhD Thesis in RWTH Aachen University, Germany, 2015. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[19]	B. Datta, Numerical Methods for Linear Control Systems, Elsevier Academic Press, 2004. Google Scholar
[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. Google Scholar
[21]	A. Donze, Breach, a toolbox for verification and parameter synthesis of hybrid systems, Proc. of Computer Aided Verification, (2010), 167–170. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[28]	M. Gameiro and P. Manolios, Formally verifying an algorithm based on interval arithmetic for checking transversality, Workshop on ACL2 Prover and Applications, 2004. Google Scholar
[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. Google Scholar
[30]	C. Le Guernic, Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics, PhD Thesis in Universit Joseph-Fourier-Grenoble I, France, 2009. Google Scholar
[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. Google Scholar
[32]	T. Henzinger, The theory of hybrid automata, Symposium on Logic in Computer Science, (1996), 278–292. doi: 10.1109/LICS.1996.561342. Google Scholar
[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. Google Scholar
[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. Google Scholar
[35]	S. Kong, S. Gao and W. Chen, Reachability analysis for hybrid systems, Proc. of TACAS15, LNCS, Springer, 9035 (2015), 200–205. Google Scholar
[36]	M. Konstantinov, D. Gu, V. Mehrmann and P. Petkov, Perturbation Theory for Matrix Equations, 2$^{nd}$ edition, Elsevier, Amsterdam, 2003, ISBN-9780444513151. Google Scholar
[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. Google Scholar
[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. Google Scholar
[39]	LAPACK-Linear Algebra PACKage, 2019. Available from: http://www.netlib.org/lapack/. Google Scholar
[40]	W. Levine, The Control Handbook, IEEE Press, 1996. Google Scholar
[41]	C. Livadas and N. Lynch, A new class of decidable hybrid systems, Hybrid Systems: Computation and Control, LNCS, 1386 (1998), 253-272. Google Scholar
[42]	Matlab-Mathworks, 2019. Available from: https://www.mathworks.com Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[46]	R. E. Moore, Methods and Applications of Interval Analysis, SIAM Studies in Applied and Numerical Mathematics, Philadelphia, 1987, ISBN-10: 0898711614. Google Scholar
[47]	R. E. Moore, R. B. Kearfott and M. J. Cloud, Introduction to Interval Analysis, SIAM, 2009. doi: 10.1137/1.9780898717716. Google Scholar
[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. Google Scholar
[49]	T. Nahhal and T. Dang, Test coverage for continuous and hybrid systems, Int. Conf. on Computer Aided Verification, LNCS, 4590 (2007), 449-462. Google Scholar
[50]	I. Pasca, Formal Verifcation for Numerical Methods, PhD Thesis in Universit Nice Sophia Antipolis, France, 2010. Google Scholar
[51]	P. Petkov, M. Konstantinov and N. Christov, Computational Methods for Linear Control Systems, 2$^{nd}$ edition, Prentice- Hall, Hemel Hempstead, 1991, ISBN-9780444513151. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[57]	A. Puri, Theory of Hybrid Systems and Discrete Event Systems, PhD Thesis in University of California, Berkeley, 1995. Google Scholar
[58]	PyInterval - Interval arithmetic in Python, 2019. Available from: https://github.com/taschini/pyinterval Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[62]	RTCA Formal Methods Supplement to DO-178C and DO-278A, RTCA DO-333, December 13, 2011. Google Scholar
[63]	RTCA, Software Considerations in Airborne Systems and Equipment Certification, RTCA DO-178C, December 13, 2011. Google Scholar
[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. Google Scholar
[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. Google Scholar
[66]	B. I. Silva and B. H. Krogh, Formal verification of hybrid systems using CheckMate: A case study, American Control Conference, (2000), 1679–1683. Google Scholar
[67]	G. Stewart and J. Sun, Matrix Perturbation Theory, Academic Press, New York, 1990. Google Scholar
[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. Google Scholar
[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. Google Scholar
[70]	V. A. Tsachouridis, Numerical analysis of $H_{\infty} $ filter for system parameter identification, Int. J. Modelling, Identification and Control, 30 (2018), 163-183. Google Scholar
[71]	University of Florida Sparse Matrix Collection, 2019. Available from: https://www.cise.ufl.edu/research/sparse/matrices/list_by_id.html Google Scholar
[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. Google Scholar
[73]	Y. Wei, P. Stanimirovic and M. Petkovic, Numerical and Symbolic Computations of Generalized Inverses, World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2018. Google Scholar
[74]	J. Wilkinson, Rounding Errors in Algebraic Processes, Prentice Hall, Englewood Cliff, NJ, 1963. Google Scholar
[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. Google Scholar
[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. Google Scholar

show all references

References:

[1]	AAFLIB - An Affine Arithmetic C++, 2019. Available from: http://aaflib.sourceforge.net. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[8]	A. Ben-Israel and T. N. E. Greville, Generalized Inverses Theory and Applications, Springer, 2003, ISBN 978-0-387-00293-4. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[14]	X. Chen, Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models, PhD Thesis in RWTH Aachen University, Germany, 2015. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[19]	B. Datta, Numerical Methods for Linear Control Systems, Elsevier Academic Press, 2004. Google Scholar
[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. Google Scholar
[21]	A. Donze, Breach, a toolbox for verification and parameter synthesis of hybrid systems, Proc. of Computer Aided Verification, (2010), 167–170. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[28]	M. Gameiro and P. Manolios, Formally verifying an algorithm based on interval arithmetic for checking transversality, Workshop on ACL2 Prover and Applications, 2004. Google Scholar
[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. Google Scholar
[30]	C. Le Guernic, Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics, PhD Thesis in Universit Joseph-Fourier-Grenoble I, France, 2009. Google Scholar
[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. Google Scholar
[32]	T. Henzinger, The theory of hybrid automata, Symposium on Logic in Computer Science, (1996), 278–292. doi: 10.1109/LICS.1996.561342. Google Scholar
[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. Google Scholar
[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. Google Scholar
[35]	S. Kong, S. Gao and W. Chen, Reachability analysis for hybrid systems, Proc. of TACAS15, LNCS, Springer, 9035 (2015), 200–205. Google Scholar
[36]	M. Konstantinov, D. Gu, V. Mehrmann and P. Petkov, Perturbation Theory for Matrix Equations, 2$^{nd}$ edition, Elsevier, Amsterdam, 2003, ISBN-9780444513151. Google Scholar
[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. Google Scholar
[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. Google Scholar
[39]	LAPACK-Linear Algebra PACKage, 2019. Available from: http://www.netlib.org/lapack/. Google Scholar
[40]	W. Levine, The Control Handbook, IEEE Press, 1996. Google Scholar
[41]	C. Livadas and N. Lynch, A new class of decidable hybrid systems, Hybrid Systems: Computation and Control, LNCS, 1386 (1998), 253-272. Google Scholar
[42]	Matlab-Mathworks, 2019. Available from: https://www.mathworks.com Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[46]	R. E. Moore, Methods and Applications of Interval Analysis, SIAM Studies in Applied and Numerical Mathematics, Philadelphia, 1987, ISBN-10: 0898711614. Google Scholar
[47]	R. E. Moore, R. B. Kearfott and M. J. Cloud, Introduction to Interval Analysis, SIAM, 2009. doi: 10.1137/1.9780898717716. Google Scholar
[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. Google Scholar
[49]	T. Nahhal and T. Dang, Test coverage for continuous and hybrid systems, Int. Conf. on Computer Aided Verification, LNCS, 4590 (2007), 449-462. Google Scholar
[50]	I. Pasca, Formal Verifcation for Numerical Methods, PhD Thesis in Universit Nice Sophia Antipolis, France, 2010. Google Scholar
[51]	P. Petkov, M. Konstantinov and N. Christov, Computational Methods for Linear Control Systems, 2$^{nd}$ edition, Prentice- Hall, Hemel Hempstead, 1991, ISBN-9780444513151. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[57]	A. Puri, Theory of Hybrid Systems and Discrete Event Systems, PhD Thesis in University of California, Berkeley, 1995. Google Scholar
[58]	PyInterval - Interval arithmetic in Python, 2019. Available from: https://github.com/taschini/pyinterval Google Scholar
[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. Google Scholar
[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. Google Scholar
[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. Google Scholar
[62]	RTCA Formal Methods Supplement to DO-178C and DO-278A, RTCA DO-333, December 13, 2011. Google Scholar
[63]	RTCA, Software Considerations in Airborne Systems and Equipment Certification, RTCA DO-178C, December 13, 2011. Google Scholar
[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. Google Scholar
[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. Google Scholar
[66]	B. I. Silva and B. H. Krogh, Formal verification of hybrid systems using CheckMate: A case study, American Control Conference, (2000), 1679–1683. Google Scholar
[67]	G. Stewart and J. Sun, Matrix Perturbation Theory, Academic Press, New York, 1990. Google Scholar
[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. Google Scholar
[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. Google Scholar
[70]	V. A. Tsachouridis, Numerical analysis of $H_{\infty} $ filter for system parameter identification, Int. J. Modelling, Identification and Control, 30 (2018), 163-183. Google Scholar
[71]	University of Florida Sparse Matrix Collection, 2019. Available from: https://www.cise.ufl.edu/research/sparse/matrices/list_by_id.html Google Scholar
[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. Google Scholar
[73]	Y. Wei, P. Stanimirovic and M. Petkovic, Numerical and Symbolic Computations of Generalized Inverses, World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2018. Google Scholar
[74]	J. Wilkinson, Rounding Errors in Algebraic Processes, Prentice Hall, Englewood Cliff, NJ, 1963. Google Scholar
[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. Google Scholar
[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. Google Scholar

Figure 1. Hybrid automaton for a $ 1 \times 2 $ matrix $ A $

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 2. Hybrid automaton for a $ 2 \times 2 $ matrix $ A $

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 3. Hybrid automaton for a $ 2 \times 3 $ matrix $ A $

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 4. Affine arithmetic approach for bound convergence expression (34) for a $ 2 \times 2 $ interval matrix

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 5. Affine arithmetic approach for bound convergence expression (34) for a $ 2 \times 3 $ interval matrix

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 6. Variation of condition number of $ A $ as function of $ {A_{11}} $

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 7. $ 43 \times 68 $ matrix lpkb2 University of Florida sparse matrix collection

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 8. $ 43 \times 68 $ matrix example in Breach

Figure Options

Download full-size image

Download as PowerPoint slide

Figure 9. Computational reliability monitor for $ 43 \times 68 $ matrix Example 6

Figure Options

Download full-size image

Download as PowerPoint slide

[1]	Ningyu Sha, Lei Shi, Ming Yan. Fast algorithms for robust principal component analysis with an upper bound on the rank. Inverse Problems & Imaging, 2021, 15 (1) : 109-128. doi: 10.3934/ipi.2020067
[2]	Jing Qin, Shuang Li, Deanna Needell, Anna Ma, Rachel Grotheer, Chenxi Huang, Natalie Durgin. Stochastic greedy algorithms for multiple measurement vectors. Inverse Problems & Imaging, 2021, 15 (1) : 79-107. doi: 10.3934/ipi.2020066
[3]	Peizhao Yu, Guoshan Zhang, Yi Zhang. Decoupling of cubic polynomial matrix systems. Numerical Algebra, Control & Optimization, 2021, 11 (1) : 13-26. doi: 10.3934/naco.2020012
[4]	Shengxin Zhu, Tongxiang Gu, Xingping Liu. AIMS: Average information matrix splitting. Mathematical Foundations of Computing, 2020, 3 (4) : 301-308. doi: 10.3934/mfc.2020012
[5]	Ye Zhang, Bernd Hofmann. Two new non-negativity preserving iterative regularization methods for ill-posed inverse problems. Inverse Problems & Imaging, 2021, 15 (2) : 229-256. doi: 10.3934/ipi.2020062
[6]	Nicola Pace, Angelo Sonnino. On the existence of PD-sets: Algorithms arising from automorphism groups of codes. Advances in Mathematics of Communications, 2021, 15 (2) : 267-277. doi: 10.3934/amc.2020065
[7]	Wolfgang Riedl, Robert Baier, Matthias Gerdts. Optimization-based subdivision algorithm for reachable sets. Journal of Computational Dynamics, 2021, 8 (1) : 99-130. doi: 10.3934/jcd.2021005
[8]	Masoud Rabbani, Nastaran Oladzad-Abbasabady, Niloofar Akbarian-Saravi. Ambulance routing in disaster response considering variable patient condition: NSGA-II and MOPSO algorithms. Journal of Industrial & Management Optimization, 2021 doi: 10.3934/jimo.2021007
[9]	Parikshit Upadhyaya, Elias Jarlebring, Emanuel H. Rubensson. A density matrix approach to the convergence of the self-consistent field iteration. Numerical Algebra, Control & Optimization, 2021, 11 (1) : 99-115. doi: 10.3934/naco.2020018
[10]	George W. Patrick. The geometry of convergence in numerical analysis. Journal of Computational Dynamics, 2021, 8 (1) : 33-58. doi: 10.3934/jcd.2021003
[11]	Mohammed Abdulrazaq Kahya, Suhaib Abduljabbar Altamir, Zakariya Yahya Algamal. Improving whale optimization algorithm for feature selection with a time-varying transfer function. Numerical Algebra, Control & Optimization, 2021, 11 (1) : 87-98. doi: 10.3934/naco.2020017
[12]	Cheng Peng, Zhaohui Tang, Weihua Gui, Qing Chen, Jing He. A bidirectional weighted boundary distance algorithm for time series similarity computation based on optimized sliding window size. Journal of Industrial & Management Optimization, 2021, 17 (1) : 205-220. doi: 10.3934/jimo.2019107
[13]	Editorial Office. Retraction: Honggang Yu, An efficient face recognition algorithm using the improved convolutional neural network. Discrete & Continuous Dynamical Systems - S, 2019, 12 (4&5) : 901-901. doi: 10.3934/dcdss.2019060
[14]	Editorial Office. Retraction: Xiaohong Zhu, Zili Yang and Tabharit Zoubir, Research on the matching algorithm for heterologous image after deformation in the same scene. Discrete & Continuous Dynamical Systems - S, 2019, 12 (4&5) : 1281-1281. doi: 10.3934/dcdss.2019088
[15]	Zi Xu, Siwen Wang, Jinjin Huang. An efficient low complexity algorithm for box-constrained weighted maximin dispersion problem. Journal of Industrial & Management Optimization, 2021, 17 (2) : 971-979. doi: 10.3934/jimo.2020007
[16]	Guo Zhou, Yongquan Zhou, Ruxin Zhao. Hybrid social spider optimization algorithm with differential mutation operator for the job-shop scheduling problem. Journal of Industrial & Management Optimization, 2021, 17 (2) : 533-548. doi: 10.3934/jimo.2019122
[17]	Min Chen, Olivier Goubet, Shenghao Li. Mathematical analysis of bump to bucket problem. Communications on Pure & Applied Analysis, 2020, 19 (12) : 5567-5580. doi: 10.3934/cpaa.2020251
[18]	S. Sadeghi, H. Jafari, S. Nemati. Solving fractional Advection-diffusion equation using Genocchi operational matrix based on Atangana-Baleanu derivative. Discrete & Continuous Dynamical Systems - S, 2020 doi: 10.3934/dcdss.2020435
[19]	Yuri Fedorov, Božidar Jovanović. Continuous and discrete Neumann systems on Stiefel varieties as matrix generalizations of the Jacobi–Mumford systems. Discrete & Continuous Dynamical Systems - A, 2020 doi: 10.3934/dcds.2020375
[20]	Sihem Guerarra. Maximum and minimum ranks and inertias of the Hermitian parts of the least rank solution of the matrix equation AXB = C. Numerical Algebra, Control & Optimization, 2021, 11 (1) : 75-86. doi: 10.3934/naco.2020016

Impact Factor:

Tools

Metrics

Tools

Article outline

Figures and Tables

Impact Factor:

Tools

Figures and Tables

Impact Factor:

American Institute of Mathematical Sciences

Formal analysis of the Schulz matrix inversion algorithm: A paradigm towards computer aided verification of general matrix flow solvers

References:

References:

Tools

Metrics

Other articles
by authors

Tools

Tools

Tools

Metrics

Other articles
by authors

American Institute of Mathematical Sciences

Formal analysis of the Schulz matrix inversion algorithm: A paradigm towards computer aided verification of general matrix flow solvers

References:

References:

Tools

Metrics

Other articlesby authors

Tools

Tools

Tools

Metrics

Other articlesby authors

Other articles
by authors

Other articles
by authors