[發(fā)明專利]一種基于共形幾何代數(shù)的機(jī)械臂運(yùn)動(dòng)規(guī)劃的形式化分析方法及系統(tǒng)

無(wú)效

• 申請(qǐng)?zhí)枺?/td>: 201610055938.2
• 申請(qǐng)日: 2016-01-27
• 公開（公告）號(hào): CN105760576A
• 公開（公告）日: 2016-07-13
• 發(fā)明（設(shè)計(jì)）人: 施智平;馬莎;關(guān)永;邵振洲;張倩穎;王瑞;李曉娟;李黎明
• 申請(qǐng)（專利權(quán)）人: 首都師范大學(xué)
• 主分類號(hào): G06F17/50
• 分類號(hào): G06F17/50
• 代理公司: 北京慧泉知識(shí)產(chǎn)權(quán)代理有限公司 11232
• 代理人: 王順榮;唐愛華

【技術(shù)領(lǐng)域】

本發(fā)明涉及一種基于共形幾何代數(shù)的機(jī)械臂運(yùn)動(dòng)規(guī)劃的形式化分析方法及系統(tǒng)，屬于計(jì)算機(jī)科學(xué)技術(shù)領(lǐng)域。

【背景技術(shù)】

共形幾何代數(shù)(CGA)作為一種先進(jìn)的幾何表示和計(jì)算系統(tǒng)，它為經(jīng)典幾何提供了簡(jiǎn)潔、直觀和統(tǒng)一的齊性代數(shù)框架。CGA通過(guò)引入兩個(gè)額外維度基準(zhǔn)原點(diǎn)(e₀)和無(wú)窮遠(yuǎn)點(diǎn)(e_∞)，使得歐氏空間嵌入到共形空間中，并賦予其閔氏內(nèi)積結(jié)構(gòu)，不僅保留了齊次空間中外積的Grassmann結(jié)構(gòu)、更使得內(nèi)積具備了表征距離、角度等基本度量的明確幾何意義。CGA不僅成功的解決了運(yùn)用幾何語(yǔ)言完成幾何計(jì)算，基于CGA的新方法和新算法層出不窮,還在許多高科技領(lǐng)域中如工程學(xué)和計(jì)算機(jī)科學(xué)的幾何問題的解決起了關(guān)鍵性的作用。在機(jī)器人學(xué)中，CGA與以往的代數(shù)不同，它的運(yùn)算對(duì)象不是數(shù)字，而是幾何體。而機(jī)器人研究對(duì)象是于基本幾何體建立的系統(tǒng)所形成的幾何關(guān)系。因此，共形幾何代數(shù)在機(jī)器人研究中具有獨(dú)特性。

目前利用CGA為數(shù)學(xué)工具進(jìn)行建模和計(jì)算分析傳統(tǒng)上使用基于計(jì)算機(jī)的數(shù)值計(jì)算分析和計(jì)算機(jī)代數(shù)系統(tǒng)(CASs)如Maple、CLUCalc、Gaalop等，然而這兩種方法均不能完全保證結(jié)果的正確性和精確性，由于計(jì)算的迭代次數(shù)受限于計(jì)算機(jī)內(nèi)存和浮點(diǎn)數(shù)限制，數(shù)值方法并不能完全保證結(jié)果的精確性，而CASs提供的符號(hào)方法雖然利用核心算法可以精確推導(dǎo)出符號(hào)表達(dá)式的解在一定程度上避免了數(shù)值計(jì)算解不精確的問題，但是對(duì)龐大的符號(hào)集進(jìn)行運(yùn)算的算法并沒有經(jīng)過(guò)驗(yàn)證，并且在邊界條件的處理上存在短板，所得到的結(jié)果仍然可能存在問題。為避免這些問題在系統(tǒng)早期設(shè)計(jì)時(shí)就產(chǎn)生，對(duì)CGA理論進(jìn)行形式化分析是一種理想的解決辦法。近幾十年來(lái)，形式化方法在很多領(lǐng)域中都取得了巨大進(jìn)步，基礎(chǔ)研究的進(jìn)展加上技術(shù)進(jìn)步的推動(dòng)，使新方法和新工具不斷出現(xiàn)并逐步完善成為一種成熟的高可靠驗(yàn)證技術(shù)。它的主要思想是根據(jù)數(shù)學(xué)理論來(lái)證明所設(shè)計(jì)的系統(tǒng)滿足系統(tǒng)的規(guī)范或具有所期望的性質(zhì)。與人為筆紙分析和上述傳統(tǒng)方法相比，形式化方法可根據(jù)數(shù)學(xué)邏輯的嚴(yán)密性提高發(fā)現(xiàn)微小而關(guān)鍵的早期設(shè)計(jì)錯(cuò)誤的機(jī)率。

【發(fā)明內(nèi)容】

有鑒于此，本發(fā)明的目的在于提供一種基于共形幾何代數(shù)的機(jī)械臂運(yùn)動(dòng)規(guī)劃的形式化分析方法及系統(tǒng)，主要是在高階邏輯證明工具HOL-Light中建立CGA系統(tǒng)的形式化模型，并基于建立的共形幾何邏輯模型對(duì)機(jī)器人的運(yùn)動(dòng)規(guī)劃進(jìn)行形式化建模與驗(yàn)證，以解決現(xiàn)有技術(shù)中計(jì)算復(fù)雜、結(jié)果不太精確的問題。

下面將本發(fā)明的技術(shù)方案詳述如下：

本發(fā)明一方面提供了一種基于共形幾何代數(shù)的機(jī)械臂運(yùn)動(dòng)規(guī)劃的形式化分析方法，其包括：

基于共形幾何代數(shù)理論對(duì)機(jī)器人的基本構(gòu)件、運(yùn)動(dòng)規(guī)劃約束構(gòu)建對(duì)應(yīng)的幾何模型，再用高階邏輯語(yǔ)言描述所建立的幾何模型，形成機(jī)器人的基本幾何邏輯模型系統(tǒng)；

確定機(jī)器人的具體結(jié)構(gòu)參數(shù)和運(yùn)動(dòng)規(guī)劃參數(shù)；

基于基本幾何邏輯模型系統(tǒng)對(duì)具體機(jī)器人運(yùn)動(dòng)過(guò)程的形式化建模，得到具體機(jī)器人運(yùn)動(dòng)過(guò)程的幾何關(guān)系邏輯模型；

用邏輯公式描述需要驗(yàn)證的機(jī)器人運(yùn)動(dòng)過(guò)程的約束或?qū)傩裕?/p>

將具體機(jī)器人運(yùn)動(dòng)過(guò)程的所述幾何關(guān)系邏輯模型和待驗(yàn)證的運(yùn)動(dòng)過(guò)程的約束或?qū)傩越M成一個(gè)邏輯命題；

利用邏輯推理引擎證明所述邏輯命題是否成立，成立表明所述模型滿足所述的約束或者具備所述的屬性，不成立表明所述模型不滿足所述的約束或者不具備所述的屬性。

其中，所構(gòu)建的幾何模型包括：機(jī)器人關(guān)節(jié)抽象化成點(diǎn)模型、機(jī)器人關(guān)節(jié)末端可達(dá)范圍抽象化為球模型、機(jī)器人關(guān)節(jié)所在輔助面抽象為面模型、機(jī)器人關(guān)節(jié)點(diǎn)連接構(gòu)成的線模型、將機(jī)器人基本構(gòu)件的約束關(guān)系抽象化為幾何體求交模型、機(jī)器人基本構(gòu)件旋轉(zhuǎn)運(yùn)動(dòng)抽象化為幾何體純旋轉(zhuǎn)模型、機(jī)器人基本構(gòu)件平移運(yùn)動(dòng)抽象化為幾何體純平移模型、機(jī)器人關(guān)節(jié)末端到達(dá)期望位置抽象化為幾何體剛體運(yùn)動(dòng)模型、機(jī)器人基本構(gòu)件度量關(guān)系抽象化為幾何體間距離模型、機(jī)器人基本構(gòu)件夾角抽象化為幾何體夾角模型。

其中，所述機(jī)器人關(guān)節(jié)抽象化成點(diǎn)模型如下表示：

e_∞＝e_-+e₊