We gratefully acknowledge support from
the Simons Foundation and member institutions.

Logic in Computer Science

New submissions

[ total of 4 entries: 1-4 ]
[ showing up to 2000 entries per page: fewer | more ]

New submissions for Thu, 25 Nov 21

[1]  arXiv:2111.12274 [pdf, other]
Title: Formalization of Bond Graph using Higher-order-logic Theorem Proving
Comments: ISA Transactions, Elsevier
Subjects: Logic in Computer Science (cs.LO)

Bond graph is a unified graphical approach for describing the dynamics of complex engineering and physical systems and is widely adopted in a variety of domains, such as, electrical, mechanical, medical, thermal and fluid mechanics. Traditionally, these dynamics are analyzed using paper-and-pencil proof methods and computer-based techniques. However, both of these techniques suffer from their inherent limitations, such as human-error proneness, approximations of results and enormous computational requirements. Thus, these techniques cannot be trusted for performing the bond graph based dynamical analysis of systems from the safety-critical domains like robotics and medicine. Formal methods, in particular, higher-order-logic theorem proving, can overcome the shortcomings of these traditional methods and provide an accurate analysis of these systems. It has been widely used for analyzing the dynamics of engineering and physical systems. In this paper, we propose to use higher-order-logic theorem proving for performing the bond graph based analysis of the physical systems. In particular, we provide formalization of bond graph, which mainly includes functions that allow conversion of a bond graph to its corresponding mathematical model (state-space model) and the verification of its various properties, such as, stability. To illustrate the practical effectiveness of our proposed approach, we present the formal stability analysis of a prosthetic mechatronic hand using HOL Light theorem prover. Moreover, to help non-experts in HOL, we encode our formally verified stability theorems in MATLAB to perform the stability analysis of an anthropomorphic prosthetic mechatronic hand.

Replacements for Thu, 25 Nov 21

[2]  arXiv:2012.13806 (replaced) [pdf, other]
Title: Time-Fluid Field-Based Coordination through Programmable Distributed Schedulers
Subjects: Logic in Computer Science (cs.LO); Distributed, Parallel, and Cluster Computing (cs.DC)
[3]  arXiv:2002.09827 (replaced) [pdf, ps, other]
Title: A Formal Treatment of Contract Signature
Comments: This paper has been accepted to IEEE Transactions on Services Computing. Revisions to the previous version include expanded material on smart contracts in Section 9
Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Multiagent Systems (cs.MA)
[4]  arXiv:2105.10362 (replaced) [pdf, other]
Title: Functionals in the Clouds: An abstract architecture of serverless Cloud-Native Apps
Comments: improved version submitted to CCGrid_2022
Subjects: Computation and Language (cs.CL); Logic in Computer Science (cs.LO)
[ total of 4 entries: 1-4 ]
[ showing up to 2000 entries per page: fewer | more ]

Disable MathJax (What is MathJax?)

Links to: arXiv, form interface, find, cs, recent, 2111, contact, help  (Access key information)